%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV764-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:22 PM UTC 2026
% Result : Unsatisfiable 125.37s 35.78s
% Output : Refutation 125.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 31
% Syntax : Number of formulae : 96 ( 30 unt; 6 def)
% Number of atoms : 196 ( 35 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 194 ( 94 ~; 94 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 7 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 19 con; 0-4 aty)
% Number of variables : 140 ( 0 sgn 140 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f212,axiom,
! [X2,X0,X1] : hBOOL(c_in(X0,c_Set_Oinsert(X0,X1,X2),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__iff_1) ).
fof(f349,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(X0,X1),X2,tc_Event_Oevent)) = c_Set_Oinsert(X1,c_Event_Oknows(c_Message_Oagent_OSpy,X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_knows__Spy__Notes_0) ).
fof(f403,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(X0,c_List_Oset(X3,X2),X2))
| c_List_Olist__inter(c_List_Olist_OCons(X0,X1,X2),X3,X2) = c_List_Olist_OCons(X0,c_List_Olist__inter(X1,X3,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list__inter_Osimps_I2_J_0) ).
fof(f404,axiom,
! [X2,X3,X0,X1] :
( hBOOL(c_in(X0,c_List_Oset(X3,X2),X2))
| c_List_Olist__inter(c_List_Olist_OCons(X0,X1,X2),X3,X2) = c_List_Olist__inter(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list__inter_Osimps_I2_J_1) ).
fof(f418,axiom,
! [X0,X1] :
( ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Spy__see__shrK_0) ).
fof(f426,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(X2,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Crypt__Spy__analz__bad_0) ).
fof(f469,axiom,
! [X2,X0,X1] : X0 != c_List_Olist_OCons(X1,X0,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f470,plain,
! [X2,X0,X1] : c_List_Olist_OCons(X1,X0,X2) != X0,
inference(reorient_equations,[],[f469]) ).
fof(f472,axiom,
~ hBOOL(c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Server__not__bad_0) ).
fof(f475,axiom,
! [X2,X0,X1] :
( c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(X0,X1),X2,tc_Event_Oevent)) = c_Event_Oknows(c_Message_Oagent_OSpy,X2)
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_knows__Spy__Notes_1) ).
fof(f476,plain,
! [X2,X0,X1] :
( hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| c_Event_Oknows(c_Message_Oagent_OSpy,X2) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(X0,X1),X2,tc_Event_Oevent)) ),
inference(reorient_equations,[],[f475]) ).
fof(f531,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(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))
| ~ hBOOL(c_in(X3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(X1,c_Event_Obad,tc_Message_Oagent))
| hBOOL(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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_B__trusts__NS3_0) ).
fof(f555,axiom,
! [X0] : c_Message_Oanalz(c_Message_Oanalz(X0)) = c_Message_Oanalz(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_analz__idem_0) ).
fof(f556,plain,
! [X0] : c_Message_Oanalz(X0) = c_Message_Oanalz(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f555]) ).
fof(f558,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X2),c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_analz_OFst_0) ).
fof(f570,axiom,
! [X0,X1] :
( hBOOL(c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_parts_OInj_0) ).
fof(f571,axiom,
! [X0,X1] :
( hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_analz_OInj_0) ).
fof(f573,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Says__imp__spies_0) ).
fof(f591,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Says__imp__analz__Spy_0) ).
fof(f593,axiom,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(X7,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X8),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X9))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X6))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_unique__session__keys_0) ).
fof(f595,axiom,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X7,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X7),c_Message_Omsg_OMPair(X8,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X9))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X6))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_unique__session__keys_2) ).
fof(f625,axiom,
! [X2,X3,X0,X1,X6,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)))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(X5,c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Says__Server__message__form_1) ).
fof(f626,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(X5,c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(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 ),
inference(reorient_equations,[],[f625]) ).
fof(f636,negated_conjecture,
hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f639,negated_conjecture,
hBOOL(c_in(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f640,negated_conjecture,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f641,negated_conjecture,
hBOOL(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_evs4,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f642,negated_conjecture,
v_K = v_Ka,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f643,plain,
v_Ka = v_K,
inference(reorient_equations,[],[f642]) ).
fof(f646,negated_conjecture,
! [X0] : ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,v_B,v_X),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f689,plain,
hBOOL(c_in(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
inference(definition_unfolding,[],[f639,f643]) ).
fof(f749,definition,
( spl0_1
<=> hBOOL(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_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f750,plain,
( hBOOL(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_evs4,tc_Event_Oevent),tc_Event_Oevent))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f770,plain,
spl0_1,
inference(avatar_split_clause,[],[f641,f749]) ).
fof(f1645,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X2),X1,tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
inference(resolution,[],[f558,f571]) ).
fof(f2990,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa))),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),
inference(resolution,[],[f573,f689]) ).
fof(f3246,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(resolution,[],[f591,f689]) ).
fof(f3597,plain,
! [X0,X1] : c_List_Olist__inter(c_List_Olist_OCons(c_Event_Oevent_OSays(X0,v_B,v_X),X1,tc_Event_Oevent),v_evs4,tc_Event_Oevent) = c_List_Olist__inter(X1,v_evs4,tc_Event_Oevent),
inference(resolution,[],[f404,f646]) ).
fof(f4734,plain,
! [X0] : c_List_Olist__inter(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))),X0,tc_Event_Oevent),v_evs4,tc_Event_Oevent) = c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))),c_List_Olist__inter(X0,v_evs4,tc_Event_Oevent),tc_Event_Oevent),
inference(resolution,[],[f403,f689]) ).
fof(f5153,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg)) ),
inference(resolution,[],[f418,f570]) ).
fof(f5313,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))
| c_Event_Oknows(c_Message_Oagent_OSpy,X3) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(X2,X4),X3,tc_Event_Oevent)) ),
inference(resolution,[],[f426,f476]) ).
fof(f5928,plain,
( ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A)))
| ~ spl0_1 ),
inference(resolution,[],[f626,f750]) ).
fof(f5936,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_1 ),
inference(forward_subsumption_resolution,[],[f5928,f636]) ).
fof(f6076,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(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,v_K),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_A = X0 )
| ~ spl0_1 ),
inference(resolution,[],[f593,f750]) ).
fof(f6084,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(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,v_K),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_A = X0 )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f6076,f636]) ).
fof(f6094,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(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,v_K),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_B = X2 )
| ~ spl0_1 ),
inference(resolution,[],[f595,f750]) ).
fof(f6102,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(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,v_K),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_B = X2 )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f6094,f636]) ).
fof(f6229,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X3),c_Message_Omsg_OAgent(X2))),c_Event_Oknows(c_Message_Oagent_OSpy,X0),tc_Message_Omsg))
| hBOOL(c_in(X1,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X2,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X2,X1,X3,X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X3),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X3),c_Message_Omsg_OAgent(X2)))))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(resolution,[],[f531,f570]) ).
fof(f6477,definition,
( spl0_70
<=> hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_K,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f6479,plain,
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_K,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f6477]) ).
fof(f6481,definition,
( spl0_71
<=> hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f6483,plain,
( hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f6481]) ).
fof(f6504,definition,
( spl0_72
<=> hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f6506,plain,
( hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f6504]) ).
fof(f72670,plain,
! [X0] :
( ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolution,[],[f5153,f636]) ).
fof(f207506,plain,
! [X0,X1] :
( hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))
| c_Event_Oknows(c_Message_Oagent_OSpy,X0) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(v_Ba,X1),X0,tc_Event_Oevent)) ),
inference(resolution,[],[f5313,f3246]) ).
fof(f207545,definition,
( spl0_387
<=> ! [X0,X1] : c_Event_Oknows(c_Message_Oagent_OSpy,X0) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(v_Ba,X1),X0,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl0_387])],[avatar_definition]) ).
fof(f207546,plain,
( ! [X0,X1] : c_Event_Oknows(c_Message_Oagent_OSpy,X0) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(v_Ba,X1),X0,tc_Event_Oevent))
| ~ spl0_387 ),
inference(avatar_component_clause,[],[f207545]) ).
fof(f207547,plain,
( spl0_387
| spl0_72 ),
inference(avatar_split_clause,[],[f207506,f6504,f207545]) ).
fof(f271355,plain,
( hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_K,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(resolution,[],[f6229,f2990]) ).
fof(f271396,plain,
( hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_K,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(forward_subsumption_resolution,[],[f271355,f636]) ).
fof(f271398,plain,
( spl0_70
| spl0_71 ),
inference(avatar_split_clause,[],[f271396,f6481,f6477]) ).
fof(f277124,plain,
( hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg))
| ~ spl0_72 ),
inference(resolution,[],[f6506,f1645]) ).
fof(f277183,plain,
( hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))
| ~ spl0_72 ),
inference(forward_demodulation,[],[f277124,f556]) ).
fof(f277189,plain,
( $false
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f277183,f640]) ).
fof(f277190,plain,
~ spl0_72,
inference(avatar_contradiction_clause,[],[f277189]) ).
fof(f296897,plain,
( ! [X0,X1] : c_Set_Oinsert(X0,c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(v_Ba,X0),X1,tc_Event_Oevent))
| ~ spl0_71 ),
inference(resolution,[],[f6483,f349]) ).
fof(f296918,plain,
( ! [X0,X1] : c_Event_Oknows(c_Message_Oagent_OSpy,X1) = c_Set_Oinsert(X0,c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg)
| ~ spl0_71
| ~ spl0_387 ),
inference(forward_demodulation,[],[f296897,f207546]) ).
fof(f312377,definition,
( spl0_757
<=> ! [X0] : hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[spl0_757])],[avatar_definition]) ).
fof(f312378,plain,
( ! [X0] : hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ spl0_757 ),
inference(avatar_component_clause,[],[f312377]) ).
fof(f312395,plain,
( $false
| ~ spl0_757 ),
inference(backward_subsumption_resolution,[],[f472,f312378]) ).
fof(f312431,plain,
~ spl0_757,
inference(avatar_contradiction_clause,[],[f312395]) ).
fof(f452483,plain,
( v_Ba = v_B
| ~ spl0_1
| ~ spl0_70 ),
inference(resolution,[],[f6479,f6102]) ).
fof(f452485,plain,
( v_A = v_Aa
| ~ spl0_1
| ~ spl0_70 ),
inference(resolution,[],[f6479,f6084]) ).
fof(f452828,plain,
( ! [X0] : c_List_Olist__inter(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A)))),X0,tc_Event_Oevent),v_evs4,tc_Event_Oevent) = c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A)))),c_List_Olist__inter(X0,v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| ~ spl0_1
| ~ spl0_70 ),
inference(superposition,[],[f4734,f452485]) ).
fof(f453085,plain,
( ! [X0] : c_List_Olist__inter(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_B,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)))),X0,tc_Event_Oevent),v_evs4,tc_Event_Oevent) = c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_B,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_List_Olist__inter(X0,v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| ~ spl0_1
| ~ spl0_70 ),
inference(forward_demodulation,[],[f452828,f452483]) ).
fof(f453215,plain,
( ! [X0] : c_List_Olist__inter(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_B,v_X),X0,tc_Event_Oevent),v_evs4,tc_Event_Oevent) = c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_B,v_X),c_List_Olist__inter(X0,v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| ~ spl0_1
| ~ spl0_70 ),
inference(forward_demodulation,[],[f453085,f5936]) ).
fof(f453233,plain,
( ! [X0] : c_List_Olist__inter(X0,v_evs4,tc_Event_Oevent) = c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,v_B,v_X),c_List_Olist__inter(X0,v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| ~ spl0_1
| ~ spl0_70 ),
inference(forward_demodulation,[],[f453215,f3597]) ).
fof(f453238,plain,
( $false
| ~ spl0_1
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f453233,f470]) ).
fof(f453239,plain,
( ~ spl0_1
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f453238]) ).
fof(f563371,plain,
( ! [X0,X1] : hBOOL(c_in(X1,c_Event_Oknows(c_Message_Oagent_OSpy,X0),tc_Message_Omsg))
| ~ spl0_71
| ~ spl0_387 ),
inference(superposition,[],[f212,f296918]) ).
fof(f567636,plain,
( ! [X0] : hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ spl0_71
| ~ spl0_387 ),
inference(backward_subsumption_resolution,[],[f72670,f563371]) ).
fof(f567783,plain,
( spl0_757
| ~ spl0_71
| ~ spl0_387 ),
inference(avatar_split_clause,[],[f567636,f207545,f6481,f312377]) ).
cnf(s3,plain,
spl0_1,
inference(sat_conversion,[],[f770]) ).
cnf(s630,plain,
( spl0_72
| spl0_387 ),
inference(sat_conversion,[],[f207547]) ).
cnf(s790,plain,
( spl0_70
| spl0_71 ),
inference(sat_conversion,[],[f271398]) ).
cnf(s799,plain,
~ spl0_72,
inference(sat_conversion,[],[f277190]) ).
cnf(s1058,plain,
~ spl0_757,
inference(sat_conversion,[],[f312431]) ).
cnf(s1908,plain,
( ~ spl0_1
| ~ spl0_70 ),
inference(sat_conversion,[],[f453239]) ).
cnf(s2844,plain,
( ~ spl0_71
| ~ spl0_387
| spl0_757 ),
inference(sat_conversion,[],[f567783]) ).
cnf(s3004,plain,
spl0_387,
inference(rat,[],[s630,s799]) ).
cnf(s3005,plain,
~ spl0_71,
inference(rat,[],[s2844,s1058,s3004]) ).
cnf(s3007,plain,
spl0_70,
inference(rat,[],[s790,s3005]) ).
cnf(s3008,plain,
~ spl0_1,
inference(rat,[],[s1908,s3007]) ).
cnf(s3072,plain,
$false,
inference(rat,[],[s3,s3008]) ).
fof(f567793,plain,
$false,
inference(avatar_sat_refutation,[],[s3072]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV764-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 12:33:21 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.43/1.79 % (2597584)Will run a generic schedule for satisfiability detection.
% 9.43/1.79 % (2597592)dis+10_1_sil=32000:sp=arity:random_seed=2611130534:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 9.43/1.79 % (2597590)% WARNING: option uhcvi not known.
% 9.43/1.79 % (2597589)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3940161664_2999 on theBenchmark for (2999ds/0Mi)
% 9.43/1.79 % (2597590)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1175875743:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 9.43/1.79 % (2597591)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2443317203:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 9.43/1.79 % (2597593)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3464545164:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 9.43/1.79 % (2597594)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=586396868:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 9.43/1.79 % (2597595)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4212289815:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 9.43/1.79 % (2597592)Instruction limit reached!
% 9.43/1.79 % (2597592)------------------------------
% 9.43/1.79 % (2597592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.43/1.79 % (2597592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.43/1.79 % (2597592)CaDiCaL version: 2.1.3
% 9.43/1.79 % (2597592)Termination reason: Instruction limit
% 9.43/1.79 % (2597592)Termination phase: Saturation
% 9.43/1.79 % (2597592)Time elapsed: 0.036 s
% 9.43/1.79 % (2597592)Peak memory usage: 13 MB
% 9.43/1.79 % (2597592)Instructions burned: 105 (million)
% 9.43/1.79 % (2597603)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2782057837:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 9.43/1.79 % (2597593)Instruction limit reached!
% 9.43/1.79 % (2597593)------------------------------
% 9.43/1.79 % (2597593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.43/1.79 % (2597593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.43/1.79 % (2597593)CaDiCaL version: 2.1.3
% 9.43/1.79 % (2597593)Termination reason: Instruction limit
% 9.43/1.79 % (2597593)Termination phase: Saturation
% 9.43/1.79 % (2597593)Time elapsed: 0.069 s
% 9.43/1.79 % (2597593)Peak memory usage: 13 MB
% 9.43/1.79 % (2597593)Instructions burned: 116 (million)
% 9.43/1.79 % (2597594)Instruction limit reached!
% 9.43/1.79 % (2597594)------------------------------
% 9.43/1.79 % (2597594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.43/1.79 % (2597594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.43/1.79 % (2597594)CaDiCaL version: 2.1.3
% 9.43/1.79 % (2597594)Termination reason: Instruction limit
% 9.43/1.79 % (2597594)Termination phase: Saturation
% 9.43/1.79 % (2597594)Time elapsed: 0.081 s
% 9.43/1.79 % (2597594)Peak memory usage: 13 MB
% 9.43/1.79 % (2597594)Instructions burned: 131 (million)
% 9.43/1.79 % (2597605)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4003889477:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 9.43/1.79 % (2597595)Instruction limit reached!
% 9.43/1.79 % (2597595)------------------------------
% 9.43/1.79 % (2597595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.43/1.79 % (2597595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.43/1.79 % (2597595)CaDiCaL version: 2.1.3
% 9.43/1.79 % (2597595)Termination reason: Instruction limit
% 9.43/1.79 % (2597595)Termination phase: Saturation
% 9.43/1.79 % (2597595)Time elapsed: 0.096 s
% 9.43/1.79 % (2597595)Peak memory usage: 13 MB
% 9.43/1.79 % (2597595)Instructions burned: 160 (million)
% 9.43/1.79 % (2597606)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=1557596075:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.43/1.79 % (2597608)ott-21_1_sil=16000:fs=off:random_seed=1456463524:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.43/1.79 % TRYING [1]
% 9.43/1.79 % TRYING [2]
% 9.43/1.79 % (2597605)Instruction limit reached!
% 9.43/1.79 % (2597605)------------------------------
% 9.43/1.79 % (2597605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.43/1.79 % (2597605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/5.47 % (2597605)CaDiCaL version: 2.1.3
% 36.56/5.47 % (2597605)Termination reason: Instruction limit
% 36.56/5.47 % (2597605)Termination phase: Saturation
% 36.56/5.47 % (2597605)Time elapsed: 0.080 s
% 36.56/5.47 % (2597605)Peak memory usage: 14 MB
% 36.56/5.47 % (2597605)Instructions burned: 131 (million)
% 36.56/5.47 % (2597608)Instruction limit reached!
% 36.56/5.47 % (2597608)------------------------------
% 36.56/5.47 % (2597608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.56/5.47 % (2597608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/5.47 % (2597608)CaDiCaL version: 2.1.3
% 36.56/5.47 % (2597608)Termination reason: Instruction limit
% 36.56/5.47 % (2597608)Termination phase: Saturation
% 36.56/5.47 % (2597608)Time elapsed: 0.067 s
% 36.56/5.47 % (2597608)Peak memory usage: 12 MB
% 36.56/5.47 % (2597608)Instructions burned: 180 (million)
% 36.56/5.47 % TRYING [3]
% 36.56/5.47 % (2597611)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=570778870:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 36.56/5.47 % TRYING [1]
% 36.56/5.47 % TRYING [2]
% 36.56/5.47 % (2597612)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=642767788:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 36.56/5.47 % (2597603)Instruction limit reached!
% 36.56/5.47 % (2597603)------------------------------
% 36.56/5.47 % (2597603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.56/5.47 % (2597603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/5.47 % (2597603)CaDiCaL version: 2.1.3
% 36.56/5.47 % (2597603)Termination reason: Instruction limit
% 36.56/5.47 % (2597603)Termination phase: Finite model building constraint generation
% 36.56/5.47 % (2597603)Time elapsed: 0.167 s
% 36.56/5.47 % (2597603)Peak memory usage: 28 MB
% 36.56/5.47 % (2597603)Instructions burned: 715 (million)
% 36.56/5.47 % (2597615)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1602170363:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 36.56/5.47 % TRYING [3]
% 36.56/5.47 % TRYING [1]
% 36.56/5.47 % TRYING [2]
% 36.56/5.47 % (2597611)Instruction limit reached!
% 36.56/5.47 % (2597611)------------------------------
% 36.56/5.47 % (2597611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.56/5.47 % (2597611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/5.47 % (2597611)CaDiCaL version: 2.1.3
% 36.56/5.47 % (2597611)Termination reason: Instruction limit
% 36.56/5.47 % (2597611)Termination phase: Saturation
% 36.56/5.47 % (2597611)Time elapsed: 0.294 s
% 36.56/5.47 % (2597611)Peak memory usage: 15 MB
% 36.56/5.47 % (2597611)Instructions burned: 478 (million)
% 36.56/5.47 % (2597617)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2940122924:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 36.56/5.47 % (2597606)Instruction limit reached!
% 36.56/5.47 % (2597606)------------------------------
% 36.56/5.47 % (2597606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.56/5.47 % (2597606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/5.47 % (2597606)CaDiCaL version: 2.1.3
% 36.56/5.47 % (2597606)Termination reason: Instruction limit
% 36.56/5.47 % (2597606)Termination phase: Saturation
% 36.56/5.47 % (2597606)Time elapsed: 0.413 s
% 36.56/5.47 % (2597606)Peak memory usage: 18 MB
% 36.56/5.47 % (2597606)Instructions burned: 685 (million)
% 36.56/5.47 % (2597619)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=1610967334: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)
% 36.56/5.47 % (2597615)Instruction limit reached!
% 36.56/5.47 % (2597615)------------------------------
% 36.56/5.47 % (2597615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.56/5.47 % (2597615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/5.47 % (2597615)CaDiCaL version: 2.1.3
% 36.56/5.47 % (2597615)Termination reason: Instruction limit
% 36.56/5.47 % (2597615)Termination phase: Saturation
% 36.56/5.47 % (2597615)Time elapsed: 0.390 s
% 36.56/5.47 % (2597615)Peak memory usage: 24 MB
% 36.56/5.47 % (2597615)Instructions burned: 1181 (million)
% 36.56/5.47 % (2597621)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1665230307:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 36.56/5.47 % (2597612)Instruction limit reached!
% 36.56/5.47 % (2597612)------------------------------
% 36.56/5.47 % (2597612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.07/14.22 % (2597612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.07/14.22 % (2597612)CaDiCaL version: 2.1.3
% 99.07/14.22 % (2597612)Termination reason: Instruction limit
% 99.07/14.22 % (2597612)Termination phase: Finite model building SAT solving
% 99.07/14.22 % (2597612)Time elapsed: 0.419 s
% 99.07/14.22 % (2597612)Peak memory usage: 31 MB
% 99.07/14.22 % (2597612)Instructions burned: 867 (million)
% 99.07/14.22 % (2597623)fmb+10_1_sil=64000:random_seed=4134596002:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 99.07/14.22 % TRYING [1]
% 99.07/14.22 % TRYING [4]
% 99.07/14.22 % TRYING [2]
% 99.07/14.22 % (2597621)Instruction limit reached!
% 99.07/14.22 % (2597621)------------------------------
% 99.07/14.22 % (2597621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.07/14.22 % (2597621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.07/14.22 % (2597621)CaDiCaL version: 2.1.3
% 99.07/14.22 % (2597621)Termination reason: Instruction limit
% 99.07/14.22 % (2597621)Termination phase: Saturation
% 99.07/14.22 % (2597621)Time elapsed: 0.264 s
% 99.07/14.22 % (2597621)Peak memory usage: 19 MB
% 99.07/14.22 % (2597621)Instructions burned: 882 (million)
% 99.07/14.22 % (2597625)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2027375094:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 99.07/14.22 % (2597617)Instruction limit reached!
% 99.07/14.22 % (2597617)------------------------------
% 99.07/14.22 % (2597617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.07/14.22 % (2597617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.07/14.22 % (2597617)CaDiCaL version: 2.1.3
% 99.07/14.22 % (2597617)Termination reason: Instruction limit
% 99.07/14.22 % (2597617)Termination phase: Finite model building constraint generation
% 99.07/14.22 % (2597617)Time elapsed: 0.432 s
% 99.07/14.22 % (2597617)Peak memory usage: 81 MB
% 99.07/14.22 % (2597617)Instructions burned: 890 (million)
% 99.07/14.22 % (2597627)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1966364517:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 99.07/14.22 % (2597619)Instruction limit reached!
% 99.07/14.22 % (2597619)------------------------------
% 99.07/14.22 % (2597619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.07/14.22 % (2597619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.07/14.22 % (2597619)CaDiCaL version: 2.1.3
% 99.07/14.22 % (2597619)Termination reason: Instruction limit
% 99.07/14.22 % (2597619)Termination phase: Saturation
% 99.07/14.22 % (2597619)Time elapsed: 0.439 s
% 99.07/14.22 % (2597619)Peak memory usage: 19 MB
% 99.07/14.22 % (2597619)Instructions burned: 692 (million)
% 99.07/14.22 % (2597629)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2015287304:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 99.07/14.22 % (2597625)Cannot represent all propositional literals internally
% 99.07/14.22 % (2597625)Refutation not found, incomplete strategy
% 99.07/14.22 % (2597625)------------------------------
% 99.07/14.22 % (2597625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.07/14.22 % (2597625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.07/14.22 % (2597625)CaDiCaL version: 2.1.3
% 99.07/14.22 % (2597625)Termination reason: Refutation not found, incomplete strategy
% 99.07/14.22 % (2597625)Time elapsed: 0.102 s
% 99.07/14.22 % (2597625)Peak memory usage: 17 MB
% 99.07/14.22 % (2597625)Instructions burned: 389 (million)
% 99.07/14.22 % (2597625)------------------------------
% 99.07/14.22 % (2597625)------------------------------
% 99.07/14.22 % (2597631)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3212799534:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 99.07/14.22 % TRYING [8]
% 99.07/14.22 % TRYING [3]
% 99.07/14.22 % (2597627)Instruction limit reached!
% 99.07/14.22 % (2597627)------------------------------
% 99.07/14.22 % (2597627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.07/14.22 % (2597627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.07/14.22 % (2597627)CaDiCaL version: 2.1.3
% 99.07/14.22 % (2597627)Termination reason: Instruction limit
% 99.07/14.22 % (2597627)Termination phase: Finite model building constraint generation
% 99.07/14.22 % (2597627)Time elapsed: 0.374 s
% 99.07/14.22 % (2597627)Peak memory usage: 54 MB
% 99.07/14.22 % (2597627)Instructions burned: 920 (million)
% 99.07/14.22 % (2597633)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1521259907:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 99.07/14.22 % (2597631)Instruction limit reached!
% 125.37/35.78 % (2597631)------------------------------
% 125.37/35.78 % (2597631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597631)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597631)Termination reason: Instruction limit
% 125.37/35.78 % (2597631)Termination phase: Saturation
% 125.37/35.78 % (2597631)Time elapsed: 0.489 s
% 125.37/35.78 % (2597631)Peak memory usage: 32 MB
% 125.37/35.78 % (2597631)Instructions burned: 1472 (million)
% 125.37/35.78 % (2597635)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2290063761:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi)
% 125.37/35.78 % (2597633)Cannot represent all propositional literals internally
% 125.37/35.78 % (2597633)Refutation not found, incomplete strategy
% 125.37/35.78 % (2597633)------------------------------
% 125.37/35.78 % (2597633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597633)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597633)Termination reason: Refutation not found, incomplete strategy
% 125.37/35.78 % (2597633)Time elapsed: 0.197 s
% 125.37/35.78 % (2597633)Peak memory usage: 17 MB
% 125.37/35.78 % (2597633)Instructions burned: 394 (million)
% 125.37/35.78 % (2597633)------------------------------
% 125.37/35.78 % (2597633)------------------------------
% 125.37/35.78 % (2597637)ott-2_1_sil=16000:newcnf=on:random_seed=1689338828:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 125.37/35.78 % (2597637)Instruction limit reached!
% 125.37/35.78 % (2597637)------------------------------
% 125.37/35.78 % (2597637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597637)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597637)Termination reason: Instruction limit
% 125.37/35.78 % (2597637)Termination phase: Saturation
% 125.37/35.78 % (2597637)Time elapsed: 0.323 s
% 125.37/35.78 % (2597637)Peak memory usage: 15 MB
% 125.37/35.78 % (2597637)Instructions burned: 871 (million)
% 125.37/35.78 % (2597635)Cannot represent all propositional literals internally
% 125.37/35.78 % (2597635)Refutation not found, incomplete strategy
% 125.37/35.78 % (2597635)------------------------------
% 125.37/35.78 % (2597635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597635)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597635)Termination reason: Refutation not found, incomplete strategy
% 125.37/35.78 % (2597635)Time elapsed: 0.392 s
% 125.37/35.78 % (2597635)Peak memory usage: 26 MB
% 125.37/35.78 % (2597635)Instructions burned: 1523 (million)
% 125.37/35.78 % (2597635)------------------------------
% 125.37/35.78 % (2597635)------------------------------
% 125.37/35.78 % (2597639)ott+10_1_sil=32000:tgt=ground:random_seed=4253295253:i=5114:av=off_2980 on theBenchmark for (2980ds/5114Mi)
% 125.37/35.78 % (2597640)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=346171448:i=54282_2980 on theBenchmark for (2980ds/54282Mi)
% 125.37/35.78 % TRYING [1]
% 125.37/35.78 % TRYING [2]
% 125.37/35.78 % TRYING [3]
% 125.37/35.78 % TRYING [4]
% 125.37/35.78 % TRYING [4]
% 125.37/35.78 % TRYING [5]
% 125.37/35.78 % TRYING [5]
% 125.37/35.78 % (2597629)Instruction limit reached!
% 125.37/35.78 % (2597629)------------------------------
% 125.37/35.78 % (2597629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597629)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597629)Termination reason: Instruction limit
% 125.37/35.78 % (2597629)Termination phase: Saturation
% 125.37/35.78 % (2597629)Time elapsed: 3.019 s
% 125.37/35.78 % (2597629)Peak memory usage: 46 MB
% 125.37/35.78 % (2597629)Instructions burned: 5133 (million)
% 125.37/35.78 % (2597643)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3458205900:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 125.37/35.78 % (2597639)Instruction limit reached!
% 125.37/35.78 % (2597639)------------------------------
% 125.37/35.78 % (2597639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597639)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597639)Termination reason: Instruction limit
% 125.37/35.78 % (2597639)Termination phase: Saturation
% 125.37/35.78 % (2597639)Time elapsed: 3.257 s
% 125.37/35.78 % (2597639)Peak memory usage: 52 MB
% 125.37/35.78 % (2597639)Instructions burned: 5114 (million)
% 125.37/35.78 % (2597645)dis+21_1_sil=32000:sas=cadical:random_seed=1764038525:i=3773:amm=off_2947 on theBenchmark for (2947ds/3773Mi)
% 125.37/35.78 % (2597643)Instruction limit reached!
% 125.37/35.78 % (2597643)------------------------------
% 125.37/35.78 % (2597643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597643)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597643)Termination reason: Instruction limit
% 125.37/35.78 % (2597643)Termination phase: Saturation
% 125.37/35.78 % (2597643)Time elapsed: 2.109 s
% 125.37/35.78 % (2597643)Peak memory usage: 39 MB
% 125.37/35.78 % (2597643)Instructions burned: 3512 (million)
% 125.37/35.78 % (2597647)ott+11_1_sil=16000:gs=on:random_seed=282907394:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 125.37/35.78 % (2597645)Instruction limit reached!
% 125.37/35.78 % (2597645)------------------------------
% 125.37/35.78 % (2597645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597645)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597645)Termination reason: Instruction limit
% 125.37/35.78 % (2597645)Termination phase: Saturation
% 125.37/35.78 % (2597645)Time elapsed: 2.239 s
% 125.37/35.78 % (2597645)Peak memory usage: 36 MB
% 125.37/35.78 % (2597645)Instructions burned: 3773 (million)
% 125.37/35.78 % (2597649)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=63491876:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi)
% 125.37/35.78 % (2597647)Instruction limit reached!
% 125.37/35.78 % (2597647)------------------------------
% 125.37/35.78 % (2597647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597647)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597647)Termination reason: Instruction limit
% 125.37/35.78 % (2597647)Termination phase: Saturation
% 125.37/35.78 % (2597647)Time elapsed: 1.307 s
% 125.37/35.78 % (2597647)Peak memory usage: 26 MB
% 125.37/35.78 % (2597647)Instructions burned: 2252 (million)
% 125.37/35.78 % (2597651)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1366306940:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2924 on theBenchmark for (2924ds/4591Mi)
% 125.37/35.78 % TRYING [7]
% 125.37/35.78 % (2597623)Instruction limit reached!
% 125.37/35.78 % (2597623)------------------------------
% 125.37/35.78 % (2597623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597623)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597623)Termination reason: Instruction limit
% 125.37/35.78 % (2597623)Termination phase: Finite model building SAT solving
% 125.37/35.78 % (2597623)Time elapsed: 8.838 s
% 125.37/35.78 % (2597623)Peak memory usage: 312 MB
% 125.37/35.78 % (2597623)Instructions burned: 22063 (million)
% 125.37/35.78 % (2597769)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4200011085:i=29340_2904 on theBenchmark for (2904ds/29340Mi)
% 125.37/35.78 % (2597651)Instruction limit reached!
% 125.37/35.78 % (2597651)------------------------------
% 125.37/35.78 % (2597651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597651)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597651)Termination reason: Instruction limit
% 125.37/35.78 % (2597651)Termination phase: Saturation
% 125.37/35.78 % (2597651)Time elapsed: 2.084 s
% 125.37/35.78 % (2597651)Peak memory usage: 37 MB
% 125.37/35.78 % (2597651)Instructions burned: 4591 (million)
% 125.37/35.78 % (2597771)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=592198802:i=5211_2903 on theBenchmark for (2903ds/5211Mi)
% 125.37/35.78 % (2597771)Instruction limit reached!
% 125.37/35.78 % (2597771)------------------------------
% 125.37/35.78 % (2597771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597771)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597771)Termination reason: Instruction limit
% 125.37/35.78 % (2597771)Termination phase: Saturation
% 125.37/35.78 % (2597771)Time elapsed: 4.325 s
% 125.37/35.78 % (2597771)Peak memory usage: 51 MB
% 125.37/35.78 % (2597771)Instructions burned: 5211 (million)
% 125.37/35.78 % (2597948)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3855336824:i=5497:nm=2_2860 on theBenchmark for (2860ds/5497Mi)
% 125.37/35.78 % TRYING [17]
% 125.37/35.78 % TRYING [6]
% 125.37/35.78 % TRYING [6]
% 125.37/35.78 % (2597948)Instruction limit reached!
% 125.37/35.78 % (2597948)------------------------------
% 125.37/35.78 % (2597948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597948)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597948)Termination reason: Instruction limit
% 125.37/35.78 % (2597948)Termination phase: Finite model building constraint generation
% 125.37/35.78 % (2597948)Time elapsed: 3.970 s
% 125.37/35.78 % (2597948)Peak memory usage: 367 MB
% 125.37/35.78 % (2597948)Instructions burned: 5497 (million)
% 125.37/35.78 % (2597960)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1632892848:fmbsr=2:i=46332_2819 on theBenchmark for (2819ds/46332Mi)
% 125.37/35.78 % TRYING [15]
% 125.37/35.78 % (2597640)Instruction limit reached!
% 125.37/35.78 % (2597640)------------------------------
% 125.37/35.78 % (2597640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597640)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597640)Termination reason: Instruction limit
% 125.37/35.78 % (2597640)Termination phase: Finite model building constraint generation
% 125.37/35.78 % (2597640)Time elapsed: 20.224 s
% 125.37/35.78 % (2597640)Peak memory usage: 1515 MB
% 125.37/35.78 % (2597640)Instructions burned: 54284 (million)
% 125.37/35.78 % (2597966)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2768433889:i=14071_2775 on theBenchmark for (2775ds/14071Mi)
% 125.37/35.78 % TRYING [12]
% 125.37/35.78 % (2597966)Instruction limit reached!
% 125.37/35.78 % (2597966)------------------------------
% 125.37/35.78 % (2597966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597966)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597966)Termination reason: Instruction limit
% 125.37/35.78 % (2597966)Termination phase: Finite model building constraint generation
% 125.37/35.78 % (2597966)Time elapsed: 5.083 s
% 125.37/35.78 % (2597966)Peak memory usage: 1029 MB
% 125.37/35.78 % (2597966)Instructions burned: 14073 (million)
% 125.37/35.78 % (2597974)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=850253791:i=22565:add=on:rawr=on_2722 on theBenchmark for (2722ds/22565Mi)
% 125.37/35.78 % (2597769)Instruction limit reached!
% 125.37/35.78 % (2597769)------------------------------
% 125.37/35.78 % (2597769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597769)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597769)Termination reason: Instruction limit
% 125.37/35.78 % (2597769)Termination phase: Saturation
% 125.37/35.78 % (2597769)Time elapsed: 25.193 s
% 125.37/35.78 % (2597769)Peak memory usage: 267 MB
% 125.37/35.78 % (2597769)Instructions burned: 29340 (million)
% 125.37/35.78 % (2597982)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2139866932:i=8173:av=off_2651 on theBenchmark for (2651ds/8173Mi)
% 125.37/35.78 % (2597590) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2597584-2597590"...
% 125.37/35.78 % (2597590)...printing done.
% 125.37/35.78 % (2597590)Refutation found. Thanks to Tanya!
% 125.37/35.78 % SZS status Unsatisfiable for theBenchmark
% 125.37/35.78 % SZS output start Proof for theBenchmark
% See solution above
% 125.37/35.78 % (2597590)------------------------------
% 125.37/35.78 % (2597590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.37/35.78 % (2597590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.37/35.78 % (2597590)CaDiCaL version: 2.1.3
% 125.37/35.78 % (2597590)Termination reason: Refutation
% 125.37/35.78 % (2597590)Time elapsed: 34.909 s
% 125.37/35.78 % (2597590)Peak memory usage: 248 MB
% 125.37/35.78 % (2597590)Instructions burned: 42962 (million)
% 125.37/35.78 % (2597584)Success in time 35.546 s
% 125.37/35.78 % Vampire exiting
%------------------------------------------------------------------------------