%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV757-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 : n002.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:21 PM UTC 2026
% Result : Unsatisfiable 70.30s 15.99s
% Output : Refutation 70.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of formulae : 81 ( 24 unt; 7 def)
% Number of atoms : 164 ( 28 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 158 ( 75 ~; 76 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 8 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 19 con; 0-4 aty)
% Number of variables : 93 ( 0 sgn 93 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f328,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(f394,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(f412,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(f461,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(f462,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,[],[f461]) ).
fof(f516,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(X3,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(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))
| hBOOL(c_in(X1,c_Event_Obad,tc_Message_Oagent))
| ~ 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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_B__trusts__NS3_0) ).
fof(f540,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(f541,plain,
! [X0] : c_Message_Oanalz(X0) = c_Message_Oanalz(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f540]) ).
fof(f543,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(f556,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(f557,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_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Says__imp__parts__knows__Spy_0) ).
fof(f575,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(f577,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(f579,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(f617,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(f620,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(f621,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(f622,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(f623,negated_conjecture,
v_K = v_Ka,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f624,plain,
v_Ka = v_K,
inference(reorient_equations,[],[f623]) ).
fof(f628,negated_conjecture,
( v_A != v_Aa
| v_B != v_Ba ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_9) ).
fof(f629,plain,
( v_A != v_Aa
| v_Ba != v_B ),
inference(reorient_equations,[],[f628]) ).
fof(f673,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,[],[f620,f624]) ).
fof(f743,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(f744,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,[],[f743]) ).
fof(f756,definition,
( spl0_4
<=> v_Ba = v_B ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f758,plain,
( v_Ba != v_B
| spl0_4 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f760,definition,
( spl0_5
<=> v_A = v_Aa ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f763,plain,
( ~ spl0_4
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f629,f760,f756]) ).
fof(f765,plain,
spl0_1,
inference(avatar_split_clause,[],[f622,f743]) ).
fof(f991,plain,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),
inference(resolution,[],[f556,f621]) ).
fof(f2047,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,[],[f543,f556]) ).
fof(f3689,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_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(resolution,[],[f557,f673]) ).
fof(f3695,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,[],[f575,f673]) ).
fof(f6144,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,[],[f412,f462]) ).
fof(f6900,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,[],[f577,f744]) ).
fof(f6905,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,[],[f6900,f617]) ).
fof(f7031,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,[],[f579,f744]) ).
fof(f7036,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,[],[f7031,f617]) ).
fof(f7215,plain,
! [X2,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,v_evs4)),tc_Message_Omsg))
| 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,v_evs4),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(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(resolution,[],[f516,f617]) ).
fof(f7737,definition,
( spl0_114
<=> 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_114])],[avatar_definition]) ).
fof(f7739,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_114 ),
inference(avatar_component_clause,[],[f7737]) ).
fof(f8129,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(resolution,[],[f7215,f3689]) ).
fof(f8133,definition,
( spl0_126
<=> 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_126])],[avatar_definition]) ).
fof(f8135,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_126 ),
inference(avatar_component_clause,[],[f8133]) ).
fof(f8137,definition,
( spl0_127
<=> hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f8139,plain,
( hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f8137]) ).
fof(f8140,plain,
( spl0_126
| spl0_127 ),
inference(avatar_split_clause,[],[f8129,f8137,f8133]) ).
fof(f278672,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,[],[f6144,f3695]) ).
fof(f278706,definition,
( spl0_701
<=> ! [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_701])],[avatar_definition]) ).
fof(f278707,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_701 ),
inference(avatar_component_clause,[],[f278706]) ).
fof(f278708,plain,
( spl0_701
| spl0_114 ),
inference(avatar_split_clause,[],[f278672,f7737,f278706]) ).
fof(f606597,plain,
( v_Ba = v_B
| ~ spl0_1
| ~ spl0_126 ),
inference(resolution,[],[f8135,f7036]) ).
fof(f606599,plain,
( v_A = v_Aa
| ~ spl0_1
| ~ spl0_126 ),
inference(resolution,[],[f8135,f6905]) ).
fof(f606632,plain,
( spl0_5
| ~ spl0_1
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f606599,f8133,f743,f760]) ).
fof(f606633,plain,
( $false
| ~ spl0_1
| spl0_4
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f606597,f758]) ).
fof(f606634,plain,
( ~ spl0_1
| spl0_4
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f606633]) ).
fof(f606636,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_127 ),
inference(resolution,[],[f8139,f328]) ).
fof(f606655,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_127
| ~ spl0_701 ),
inference(forward_demodulation,[],[f606636,f278707]) ).
fof(f721067,plain,
( ! [X0,X1] : hBOOL(c_in(X1,c_Event_Oknows(c_Message_Oagent_OSpy,X0),tc_Message_Omsg))
| ~ spl0_127
| ~ spl0_701 ),
inference(superposition,[],[f394,f606655]) ).
fof(f722316,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_114 ),
inference(resolution,[],[f7739,f2047]) ).
fof(f722374,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_114 ),
inference(forward_demodulation,[],[f722316,f541]) ).
fof(f722380,plain,
( $false
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f722374,f621]) ).
fof(f722381,plain,
~ spl0_114,
inference(avatar_contradiction_clause,[],[f722380]) ).
fof(f722587,plain,
( $false
| ~ spl0_127
| ~ spl0_701 ),
inference(backward_subsumption_resolution,[],[f991,f721067]) ).
fof(f722691,plain,
( ~ spl0_127
| ~ spl0_701 ),
inference(avatar_contradiction_clause,[],[f722587]) ).
cnf(s2,plain,
( ~ spl0_4
| ~ spl0_5 ),
inference(sat_conversion,[],[f763]) ).
cnf(s4,plain,
spl0_1,
inference(sat_conversion,[],[f765]) ).
cnf(s164,plain,
( spl0_126
| spl0_127 ),
inference(sat_conversion,[],[f8140]) ).
cnf(s1187,plain,
( spl0_114
| spl0_701 ),
inference(sat_conversion,[],[f278708]) ).
cnf(s3802,plain,
( ~ spl0_1
| spl0_5
| ~ spl0_126 ),
inference(sat_conversion,[],[f606632]) ).
cnf(s3803,plain,
( ~ spl0_1
| spl0_4
| ~ spl0_126 ),
inference(sat_conversion,[],[f606634]) ).
cnf(s13118,plain,
~ spl0_114,
inference(sat_conversion,[],[f722381]) ).
cnf(s13155,plain,
( ~ spl0_127
| ~ spl0_701 ),
inference(sat_conversion,[],[f722691]) ).
cnf(s13289,plain,
spl0_701,
inference(rat,[],[s1187,s13118]) ).
cnf(s13290,plain,
~ spl0_127,
inference(rat,[],[s13155,s13289]) ).
cnf(s13424,plain,
spl0_126,
inference(rat,[],[s164,s13290]) ).
cnf(s13501,plain,
spl0_4,
inference(rat,[],[s3803,s13424,s4]) ).
cnf(s13502,plain,
spl0_5,
inference(rat,[],[s3802,s13424,s4]) ).
cnf(s13577,plain,
$false,
inference(rat,[],[s2,s13502,s13501]) ).
fof(f722702,plain,
$false,
inference(avatar_sat_refutation,[],[s13577]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV757-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 : n002.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:29:52 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
% 18.71/2.97 % (321710)Will run a generic schedule for satisfiability detection.
% 18.71/2.97 % (321716)% WARNING: option uhcvi not known.
% 18.71/2.97 % (321716)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=975344379:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 18.71/2.97 % (321715)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=108933486_2999 on theBenchmark for (2999ds/0Mi)
% 18.71/2.97 % (321717)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=791851451:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 18.71/2.97 % (321718)dis+10_1_sil=32000:sp=arity:random_seed=294509060:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 18.71/2.97 % (321719)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4050889003:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 18.71/2.97 % (321720)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2196876327:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 18.71/2.97 % (321721)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=928326272:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 18.71/2.97 % (321718)Instruction limit reached!
% 18.71/2.97 % (321718)------------------------------
% 18.71/2.97 % (321718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.71/2.97 % (321718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/2.97 % (321718)CaDiCaL version: 2.1.3
% 18.71/2.97 % (321718)Termination reason: Instruction limit
% 18.71/2.97 % (321718)Termination phase: Saturation
% 18.71/2.97 % (321718)Time elapsed: 0.065 s
% 18.71/2.97 % (321718)Peak memory usage: 13 MB
% 18.71/2.97 % (321718)Instructions burned: 103 (million)
% 18.71/2.97 % (321719)Instruction limit reached!
% 18.71/2.97 % (321719)------------------------------
% 18.71/2.97 % (321719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.71/2.97 % (321719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/2.97 % (321719)CaDiCaL version: 2.1.3
% 18.71/2.97 % (321719)Termination reason: Instruction limit
% 18.71/2.97 % (321719)Termination phase: Saturation
% 18.71/2.97 % (321719)Time elapsed: 0.067 s
% 18.71/2.97 % (321719)Peak memory usage: 13 MB
% 18.71/2.97 % (321719)Instructions burned: 116 (million)
% 18.71/2.97 % (321720)Instruction limit reached!
% 18.71/2.97 % (321720)------------------------------
% 18.71/2.97 % (321720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.71/2.97 % (321720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/2.97 % (321720)CaDiCaL version: 2.1.3
% 18.71/2.97 % (321720)Termination reason: Instruction limit
% 18.71/2.97 % (321720)Termination phase: Saturation
% 18.71/2.97 % (321720)Time elapsed: 0.083 s
% 18.71/2.97 % (321720)Peak memory usage: 13 MB
% 18.71/2.97 % (321720)Instructions burned: 132 (million)
% 18.71/2.97 % (321729)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4109129638:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 18.71/2.97 % (321730)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3332659316:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 18.71/2.97 % (321731)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=476336669:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 18.71/2.97 % (321721)Instruction limit reached!
% 18.71/2.97 % (321721)------------------------------
% 18.71/2.97 % (321721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.71/2.97 % (321721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/2.97 % (321721)CaDiCaL version: 2.1.3
% 18.71/2.97 % (321721)Termination reason: Instruction limit
% 18.71/2.97 % (321721)Termination phase: Saturation
% 18.71/2.97 % (321721)Time elapsed: 0.104 s
% 18.71/2.97 % (321721)Peak memory usage: 14 MB
% 18.71/2.97 % (321721)Instructions burned: 160 (million)
% 18.71/2.97 % (321735)ott-21_1_sil=16000:fs=off:random_seed=255287522:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 18.71/2.97 % (321730)Instruction limit reached!
% 18.71/2.97 % (321730)------------------------------
% 18.71/2.97 % (321730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.71/2.97 % (321730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.71/2.97 % (321730)CaDiCaL version: 2.1.3
% 18.71/2.97 % (321730)Termination reason: Instruction limit
% 51.01/7.51 % (321730)Termination phase: Saturation
% 51.01/7.51 % (321730)Time elapsed: 0.083 s
% 51.01/7.51 % (321730)Peak memory usage: 13 MB
% 51.01/7.51 % (321730)Instructions burned: 131 (million)
% 51.01/7.51 % (321737)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1293742661:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 51.01/7.51 % (321735)Instruction limit reached!
% 51.01/7.51 % (321735)------------------------------
% 51.01/7.51 % (321735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.01/7.51 % (321735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.01/7.51 % (321735)CaDiCaL version: 2.1.3
% 51.01/7.51 % (321735)Termination reason: Instruction limit
% 51.01/7.51 % (321735)Termination phase: Saturation
% 51.01/7.51 % (321735)Time elapsed: 0.069 s
% 51.01/7.51 % (321735)Peak memory usage: 12 MB
% 51.01/7.51 % (321735)Instructions burned: 183 (million)
% 51.01/7.51 % TRYING [1]
% 51.01/7.51 % TRYING [2]
% 51.01/7.51 % (321739)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3482008269:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 51.01/7.51 % TRYING [1]
% 51.01/7.51 % TRYING [3]
% 51.01/7.51 % TRYING [2]
% 51.01/7.51 % TRYING [3]
% 51.01/7.51 % (321729)Instruction limit reached!
% 51.01/7.51 % (321729)------------------------------
% 51.01/7.51 % (321729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.01/7.51 % (321729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.01/7.51 % (321729)CaDiCaL version: 2.1.3
% 51.01/7.51 % (321729)Termination reason: Instruction limit
% 51.01/7.51 % (321729)Termination phase: Finite model building constraint generation
% 51.01/7.51 % (321729)Time elapsed: 0.318 s
% 51.01/7.51 % (321729)Peak memory usage: 30 MB
% 51.01/7.51 % (321729)Instructions burned: 716 (million)
% 51.01/7.51 % TRYING [1]
% 51.01/7.51 % (321741)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1019725990:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 51.01/7.51 % TRYING [2]
% 51.01/7.51 % (321737)Instruction limit reached!
% 51.01/7.51 % (321737)------------------------------
% 51.01/7.51 % (321737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.01/7.51 % (321737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.01/7.51 % (321737)CaDiCaL version: 2.1.3
% 51.01/7.51 % (321737)Termination reason: Instruction limit
% 51.01/7.51 % (321737)Termination phase: Saturation
% 51.01/7.51 % (321737)Time elapsed: 0.297 s
% 51.01/7.51 % (321737)Peak memory usage: 15 MB
% 51.01/7.51 % (321737)Instructions burned: 477 (million)
% 51.01/7.51 % (321743)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4247872676:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 51.01/7.51 % (321731)Instruction limit reached!
% 51.01/7.51 % (321731)------------------------------
% 51.01/7.51 % (321731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.01/7.51 % (321731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.01/7.51 % (321731)CaDiCaL version: 2.1.3
% 51.01/7.51 % (321731)Termination reason: Instruction limit
% 51.01/7.51 % (321731)Termination phase: Saturation
% 51.01/7.51 % (321731)Time elapsed: 0.414 s
% 51.01/7.51 % (321731)Peak memory usage: 19 MB
% 51.01/7.51 % (321731)Instructions burned: 685 (million)
% 51.01/7.51 % (321745)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=331313907: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)
% 51.01/7.51 % (321739)Instruction limit reached!
% 51.01/7.51 % (321739)------------------------------
% 51.01/7.51 % (321739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.01/7.51 % (321739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.01/7.51 % (321739)CaDiCaL version: 2.1.3
% 51.01/7.51 % (321739)Termination reason: Instruction limit
% 51.01/7.51 % (321739)Termination phase: Finite model building SAT solving
% 51.01/7.51 % (321739)Time elapsed: 0.418 s
% 51.01/7.51 % (321739)Peak memory usage: 31 MB
% 51.01/7.51 % (321739)Instructions burned: 867 (million)
% 51.01/7.51 % (321747)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1675956073:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 51.01/7.51 % TRYING [4]
% 51.01/7.51 % (321743)Instruction limit reached!
% 51.01/7.51 % (321743)------------------------------
% 51.01/7.51 % (321743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.01/7.51 % (321743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321743)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321743)Termination reason: Instruction limit
% 70.30/15.99 % (321743)Termination phase: Finite model building constraint generation
% 70.30/15.99 % (321743)Time elapsed: 0.439 s
% 70.30/15.99 % (321743)Peak memory usage: 80 MB
% 70.30/15.99 % (321743)Instructions burned: 890 (million)
% 70.30/15.99 % (321745)Instruction limit reached!
% 70.30/15.99 % (321745)------------------------------
% 70.30/15.99 % (321745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321745)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321745)Termination reason: Instruction limit
% 70.30/15.99 % (321745)Termination phase: Saturation
% 70.30/15.99 % (321745)Time elapsed: 0.413 s
% 70.30/15.99 % (321745)Peak memory usage: 18 MB
% 70.30/15.99 % (321745)Instructions burned: 693 (million)
% 70.30/15.99 % (321749)fmb+10_1_sil=64000:random_seed=2284163179:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 70.30/15.99 % (321750)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=731851087:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 70.30/15.99 % (321741)Instruction limit reached!
% 70.30/15.99 % (321741)------------------------------
% 70.30/15.99 % (321741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321741)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321741)Termination reason: Instruction limit
% 70.30/15.99 % (321741)Termination phase: Saturation
% 70.30/15.99 % (321741)Time elapsed: 0.721 s
% 70.30/15.99 % (321741)Peak memory usage: 22 MB
% 70.30/15.99 % (321741)Instructions burned: 1179 (million)
% 70.30/15.99 % (321747)Instruction limit reached!
% 70.30/15.99 % (321747)------------------------------
% 70.30/15.99 % (321747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321747)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321747)Termination reason: Instruction limit
% 70.30/15.99 % (321747)Termination phase: Saturation
% 70.30/15.99 % (321747)Time elapsed: 0.502 s
% 70.30/15.99 % (321747)Peak memory usage: 19 MB
% 70.30/15.99 % (321747)Instructions burned: 879 (million)
% 70.30/15.99 % TRYING [1]
% 70.30/15.99 % (321753)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2008529632:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 70.30/15.99 % (321754)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=948867602:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 70.30/15.99 % TRYING [20]
% 70.30/15.99 % TRYING [2]
% 70.30/15.99 % TRYING [8]
% 70.30/15.99 % TRYING [3]
% 70.30/15.99 % (321753)Instruction limit reached!
% 70.30/15.99 % (321753)------------------------------
% 70.30/15.99 % (321753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321753)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321753)Termination reason: Instruction limit
% 70.30/15.99 % (321753)Termination phase: Finite model building constraint generation
% 70.30/15.99 % (321753)Time elapsed: 0.380 s
% 70.30/15.99 % (321753)Peak memory usage: 54 MB
% 70.30/15.99 % (321753)Instructions burned: 922 (million)
% 70.30/15.99 % (321757)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3361496263:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 70.30/15.99 % (321757)Instruction limit reached!
% 70.30/15.99 % (321757)------------------------------
% 70.30/15.99 % (321757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321757)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321757)Termination reason: Instruction limit
% 70.30/15.99 % (321757)Termination phase: Saturation
% 70.30/15.99 % (321757)Time elapsed: 0.887 s
% 70.30/15.99 % (321757)Peak memory usage: 31 MB
% 70.30/15.99 % (321757)Instructions burned: 1472 (million)
% 70.30/15.99 % (321759)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2305371552:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 70.30/15.99 % TRYING [5]
% 70.30/15.99 % (321759)Cannot represent all propositional literals internally
% 70.30/15.99 % (321759)Refutation not found, incomplete strategy
% 70.30/15.99 % (321759)------------------------------
% 70.30/15.99 % (321759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321759)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321759)Termination reason: Refutation not found, incomplete strategy
% 70.30/15.99 % (321759)Time elapsed: 0.204 s
% 70.30/15.99 % (321759)Peak memory usage: 17 MB
% 70.30/15.99 % (321759)Instructions burned: 412 (million)
% 70.30/15.99 % (321759)------------------------------
% 70.30/15.99 % (321759)------------------------------
% 70.30/15.99 % (321761)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=931981788:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi)
% 70.30/15.99 % TRYING [4]
% 70.30/15.99 % (321761)Cannot represent all propositional literals internally
% 70.30/15.99 % (321761)Refutation not found, incomplete strategy
% 70.30/15.99 % (321761)------------------------------
% 70.30/15.99 % (321761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321761)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321761)Termination reason: Refutation not found, incomplete strategy
% 70.30/15.99 % (321761)Time elapsed: 0.732 s
% 70.30/15.99 % (321761)Peak memory usage: 26 MB
% 70.30/15.99 % (321761)Instructions burned: 1517 (million)
% 70.30/15.99 % (321761)------------------------------
% 70.30/15.99 % (321761)------------------------------
% 70.30/15.99 % (321763)ott-2_1_sil=16000:newcnf=on:random_seed=3272704154:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi)
% 70.30/15.99 % (321763)Instruction limit reached!
% 70.30/15.99 % (321763)------------------------------
% 70.30/15.99 % (321763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321763)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321763)Termination reason: Instruction limit
% 70.30/15.99 % (321763)Termination phase: Saturation
% 70.30/15.99 % (321763)Time elapsed: 0.483 s
% 70.30/15.99 % (321763)Peak memory usage: 16 MB
% 70.30/15.99 % (321763)Instructions burned: 870 (million)
% 70.30/15.99 % (321765)ott+10_1_sil=32000:tgt=ground:random_seed=837436134:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi)
% 70.30/15.99 % (321754)Instruction limit reached!
% 70.30/15.99 % (321754)------------------------------
% 70.30/15.99 % (321754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321754)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321754)Termination reason: Instruction limit
% 70.30/15.99 % (321754)Termination phase: Saturation
% 70.30/15.99 % (321754)Time elapsed: 3.018 s
% 70.30/15.99 % (321754)Peak memory usage: 45 MB
% 70.30/15.99 % (321754)Instructions burned: 5131 (million)
% 70.30/15.99 % (321767)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1609649402:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 70.30/15.99 % TRYING [1]
% 70.30/15.99 % TRYING [2]
% 70.30/15.99 % (321750)Instruction limit reached!
% 70.30/15.99 % (321750)------------------------------
% 70.30/15.99 % (321750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321750)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321750)Termination reason: Instruction limit
% 70.30/15.99 % (321750)Termination phase: Finite model building constraint generation
% 70.30/15.99 % (321750)Time elapsed: 3.526 s
% 70.30/15.99 % (321750)Peak memory usage: 637 MB
% 70.30/15.99 % (321750)Instructions burned: 9516 (million)
% 70.30/15.99 % TRYING [3]
% 70.30/15.99 % (321769)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3589189760:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 70.30/15.99 % TRYING [4]
% 70.30/15.99 % (321769)Instruction limit reached!
% 70.30/15.99 % (321769)------------------------------
% 70.30/15.99 % (321769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321769)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321769)Termination reason: Instruction limit
% 70.30/15.99 % (321769)Termination phase: Saturation
% 70.30/15.99 % (321769)Time elapsed: 2.133 s
% 70.30/15.99 % (321769)Peak memory usage: 40 MB
% 70.30/15.99 % (321769)Instructions burned: 3512 (million)
% 70.30/15.99 % (321771)dis+21_1_sil=32000:sas=cadical:random_seed=2176486:i=3773:amm=off_2932 on theBenchmark for (2932ds/3773Mi)
% 70.30/15.99 % TRYING [5]
% 70.30/15.99 % (321765)Instruction limit reached!
% 70.30/15.99 % (321765)------------------------------
% 70.30/15.99 % (321765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321765)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321765)Termination reason: Instruction limit
% 70.30/15.99 % (321765)Termination phase: Saturation
% 70.30/15.99 % (321765)Time elapsed: 3.254 s
% 70.30/15.99 % (321765)Peak memory usage: 51 MB
% 70.30/15.99 % (321765)Instructions burned: 5115 (million)
% 70.30/15.99 % (321773)ott+11_1_sil=16000:gs=on:random_seed=1876306757:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2927 on theBenchmark for (2927ds/2251Mi)
% 70.30/15.99 % TRYING [5]
% 70.30/15.99 % (321773)Instruction limit reached!
% 70.30/15.99 % (321773)------------------------------
% 70.30/15.99 % (321773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321773)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321773)Termination reason: Instruction limit
% 70.30/15.99 % (321773)Termination phase: Saturation
% 70.30/15.99 % (321773)Time elapsed: 1.324 s
% 70.30/15.99 % (321773)Peak memory usage: 26 MB
% 70.30/15.99 % (321773)Instructions burned: 2252 (million)
% 70.30/15.99 % (321775)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3274027080:fmbsr=1.6:i=67534_2913 on theBenchmark for (2913ds/67534Mi)
% 70.30/15.99 % (321771)Instruction limit reached!
% 70.30/15.99 % (321771)------------------------------
% 70.30/15.99 % (321771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321771)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321771)Termination reason: Instruction limit
% 70.30/15.99 % (321771)Termination phase: Saturation
% 70.30/15.99 % (321771)Time elapsed: 2.197 s
% 70.30/15.99 % (321771)Peak memory usage: 37 MB
% 70.30/15.99 % (321771)Instructions burned: 3774 (million)
% 70.30/15.99 % (321777)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2873549203:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2909 on theBenchmark for (2909ds/4591Mi)
% 70.30/15.99 % (321749)Instruction limit reached!
% 70.30/15.99 % (321749)------------------------------
% 70.30/15.99 % (321749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321749)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321749)Termination reason: Instruction limit
% 70.30/15.99 % (321749)Termination phase: Finite model building constraint generation
% 70.30/15.99 % (321749)Time elapsed: 8.680 s
% 70.30/15.99 % (321749)Peak memory usage: 366 MB
% 70.30/15.99 % (321749)Instructions burned: 22061 (million)
% 70.30/15.99 % (321779)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3691131707:i=29340_2902 on theBenchmark for (2902ds/29340Mi)
% 70.30/15.99 % TRYING [6]
% 70.30/15.99 % TRYING [7]
% 70.30/15.99 % (321777)Instruction limit reached!
% 70.30/15.99 % (321777)------------------------------
% 70.30/15.99 % (321777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321777)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321777)Termination reason: Instruction limit
% 70.30/15.99 % (321777)Termination phase: Saturation
% 70.30/15.99 % (321777)Time elapsed: 2.622 s
% 70.30/15.99 % (321777)Peak memory usage: 58 MB
% 70.30/15.99 % (321777)Instructions burned: 4592 (million)
% 70.30/15.99 % (321781)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=789260715:i=5211_2883 on theBenchmark for (2883ds/5211Mi)
% 70.30/15.99 % TRYING [6]
% 70.30/15.99 % (321781)Instruction limit reached!
% 70.30/15.99 % (321781)------------------------------
% 70.30/15.99 % (321781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321781)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321781)Termination reason: Instruction limit
% 70.30/15.99 % (321781)Termination phase: Saturation
% 70.30/15.99 % (321781)Time elapsed: 2.805 s
% 70.30/15.99 % (321781)Peak memory usage: 50 MB
% 70.30/15.99 % (321781)Instructions burned: 5211 (million)
% 70.30/15.99 % (321783)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2220914249:i=5497:nm=2_2855 on theBenchmark for (2855ds/5497Mi)
% 70.30/15.99 % TRYING [17]
% 70.30/15.99 % (321716) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-321710-321716"...
% 70.30/15.99 % (321716)...printing done.
% 70.30/15.99 % (321716)Refutation found. Thanks to Tanya!
% 70.30/15.99 % SZS status Unsatisfiable for theBenchmark
% 70.30/15.99 % SZS output start Proof for theBenchmark
% See solution above
% 70.30/15.99 % (321716)------------------------------
% 70.30/15.99 % (321716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.30/15.99 % (321716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.30/15.99 % (321716)CaDiCaL version: 2.1.3
% 70.30/15.99 % (321716)Termination reason: Refutation
% 70.30/15.99 % (321716)Time elapsed: 15.471 s
% 70.30/15.99 % (321716)Peak memory usage: 300 MB
% 70.30/15.99 % (321716)Instructions burned: 47203 (million)
% 70.30/15.99 % (321710)Success in time 15.763 s
% 70.30/15.99 % Vampire exiting
%------------------------------------------------------------------------------