%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV760-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:19:26 PM UTC 2026
% Result : Unsatisfiable 10.09s 2.54s
% Output : Refutation 11.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 60
% Syntax : Number of formulae : 204 ( 105 unt; 37 def)
% Number of atoms : 336 ( 105 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 236 ( 104 ~; 125 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 8 prp; 0-2 aty)
% Number of functors : 63 ( 63 usr; 47 con; 0-3 aty)
% Number of variables : 94 ( 0 sgn 94 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,axiom,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3))
| ~ hBOOL(hAPP(X0,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sup1CI_1) ).
fof(f43,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X0,tc_fun(X3,tc_bool)),X1))
| hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sup1E_0) ).
fof(f225,axiom,
! [X2,X0,X1] : c_List_Oset(c_List_Olist_OCons(X0,X1,X2),X2) = c_Set_Oinsert(X0,c_List_Oset(X1,X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Oset_Osimps_I2_J_0) ).
fof(f233,axiom,
! [X2,X0,X1] :
( hBOOL(c_in(X0,c_Message_Oanalz(c_Set_Oinsert(X1,X2,tc_Message_Omsg)),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Message_Oanalz(X2),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_analz__insertI_0) ).
fof(f261,axiom,
! [X0] : c_Message_Oparts(c_Message_Osynth(X0)) = c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(X0),c_Message_Osynth(X0),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__synth_0) ).
fof(f290,axiom,
! [X2,X3,X0,X1] :
( hBOOL(c_in(X0,c_Set_Oinsert(X1,X2,X3),X3))
| ~ hBOOL(c_in(X0,X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insertCI_0) ).
fof(f418,axiom,
! [X0,X1] :
( c_Message_Osynth(c_Message_Oanalz(c_Set_Oinsert(X0,X1,tc_Message_Omsg))) = c_Message_Osynth(c_Message_Oanalz(X1))
| ~ hBOOL(c_in(X0,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Fake__analz__eq_0) ).
fof(f419,plain,
! [X0,X1] :
( c_Message_Osynth(c_Message_Oanalz(X1)) = c_Message_Osynth(c_Message_Oanalz(c_Set_Oinsert(X0,X1,tc_Message_Omsg)))
| ~ hBOOL(c_in(X0,c_Message_Osynth(c_Message_Oanalz(X1)),tc_Message_Omsg)) ),
inference(reorient_equations,[],[f418]) ).
fof(f443,axiom,
! [X2,X3,X0,X1] : c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(X0,X1,X2),X3,tc_Event_Oevent)) = c_Set_Oinsert(X2,c_Event_Oknows(c_Message_Oagent_OSpy,X3),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_knows__Spy__Says_0) ).
fof(f502,axiom,
! [X0] : c_Message_Oparts(c_Message_Oanalz(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__analz_0) ).
fof(f503,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oparts(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f502]) ).
fof(f507,axiom,
! [X0] : c_Message_Oanalz(c_Message_Oanalz(X0)) = c_Message_Oanalz(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_analz__idem_0) ).
fof(f508,plain,
! [X0] : c_Message_Oanalz(X0) = c_Message_Oanalz(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f507]) ).
fof(f518,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OSays(X3,X4,X5)
| X0 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I1_J_0) ).
fof(f565,axiom,
! [X2,X0,X1] :
( hBOOL(c_in(X0,X1,X2))
| ~ hBOOL(hAPP(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f566,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(X1,X0,X2))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f572,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(X0,c_List_Oset(c_List_Olist_OCons(X3,X1,X2),X2),X2))
| X0 = X3
| hBOOL(c_in(X0,c_List_Oset(X1,X2),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_set__ConsD_0) ).
fof(f578,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I5_J_0) ).
fof(f587,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(X0,X2),c_Message_Osynth(X1),tc_Message_Omsg))
| hBOOL(c_in(c_Message_Omsg_OCrypt(X0,X2),X1,tc_Message_Omsg))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,X0),X1,tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Crypt__synth_1) ).
fof(f607,axiom,
! [X0,X1] :
( hBOOL(c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_analz__conj__parts_0) ).
fof(f609,negated_conjecture,
hBOOL(c_in(v_Xa,c_Message_Osynth(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf))),tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f610,negated_conjecture,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa),v_evsf,tc_Event_Oevent))),tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f611,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(c_List_Olist_OCons(c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa),v_evsf,tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f612,negated_conjecture,
hBOOL(c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa),v_evsf,tc_Event_Oevent))),tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f613,negated_conjecture,
! [X0] : ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,v_B,v_X),c_List_Oset(c_List_Olist_OCons(c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa),v_evsf,tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f614,negated_conjecture,
( hBOOL(c_in(c_Event_Oevent_OSays(v_x,v_B,v_X),c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf)),tc_Message_Omsg))
| ~ 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_evsf,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f670,definition,
sF2 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f671,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf) = sF2,
inference(reorient_equations,[],[f670]) ).
fof(f672,definition,
sF3 = c_Message_Oanalz(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f673,plain,
c_Message_Oanalz(sF2) = sF3,
inference(reorient_equations,[],[f672]) ).
fof(f674,definition,
sF4 = c_Message_Osynth(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f675,plain,
c_Message_Osynth(sF3) = sF4,
inference(reorient_equations,[],[f674]) ).
fof(f676,definition,
sF5 = c_in(v_Xa,sF4,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f677,plain,
c_in(v_Xa,sF4,tc_Message_Omsg) = sF5,
inference(reorient_equations,[],[f676]) ).
fof(f678,plain,
hBOOL(sF5),
inference(definition_folding,[],[f609,f677,f675,f673,f671]) ).
fof(f679,definition,
sF6 = hAPP(c_Message_Omsg_OKey,v_K),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f680,plain,
hAPP(c_Message_Omsg_OKey,v_K) = sF6,
inference(reorient_equations,[],[f679]) ).
fof(f681,definition,
sF7 = c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f682,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa) = sF7,
inference(reorient_equations,[],[f681]) ).
fof(f683,definition,
sF8 = c_List_Olist_OCons(sF7,v_evsf,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f684,plain,
c_List_Olist_OCons(sF7,v_evsf,tc_Event_Oevent) = sF8,
inference(reorient_equations,[],[f683]) ).
fof(f685,definition,
sF9 = c_Event_Oknows(c_Message_Oagent_OSpy,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f686,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,sF8) = sF9,
inference(reorient_equations,[],[f685]) ).
fof(f687,definition,
sF10 = c_Message_Oanalz(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f688,plain,
c_Message_Oanalz(sF9) = sF10,
inference(reorient_equations,[],[f687]) ).
fof(f689,definition,
sF11 = c_in(sF6,sF10,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f690,plain,
c_in(sF6,sF10,tc_Message_Omsg) = sF11,
inference(reorient_equations,[],[f689]) ).
fof(f691,plain,
~ hBOOL(sF11),
inference(definition_folding,[],[f610,f690,f688,f686,f684,f682,f680]) ).
fof(f692,definition,
sF12 = hAPP(c_Public_OshrK,v_A),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f693,plain,
hAPP(c_Public_OshrK,v_A) = sF12,
inference(reorient_equations,[],[f692]) ).
fof(f694,definition,
sF13 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f695,plain,
c_Message_Omsg_OAgent(v_B) = sF13,
inference(reorient_equations,[],[f694]) ).
fof(f696,definition,
sF14 = c_Message_Omsg_OMPair(sF6,v_X),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f697,plain,
c_Message_Omsg_OMPair(sF6,v_X) = sF14,
inference(reorient_equations,[],[f696]) ).
fof(f698,definition,
sF15 = c_Message_Omsg_OMPair(sF13,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f699,plain,
c_Message_Omsg_OMPair(sF13,sF14) = sF15,
inference(reorient_equations,[],[f698]) ).
fof(f700,definition,
sF16 = c_Message_Omsg_OMPair(v_NA,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f701,plain,
c_Message_Omsg_OMPair(v_NA,sF15) = sF16,
inference(reorient_equations,[],[f700]) ).
fof(f702,definition,
sF17 = c_Message_Omsg_OCrypt(sF12,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f703,plain,
c_Message_Omsg_OCrypt(sF12,sF16) = sF17,
inference(reorient_equations,[],[f702]) ).
fof(f704,definition,
sF18 = c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f705,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,sF17) = sF18,
inference(reorient_equations,[],[f704]) ).
fof(f706,definition,
sF19 = c_List_Oset(sF8,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f707,plain,
c_List_Oset(sF8,tc_Event_Oevent) = sF19,
inference(reorient_equations,[],[f706]) ).
fof(f708,definition,
sF20 = c_in(sF18,sF19,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f709,plain,
c_in(sF18,sF19,tc_Event_Oevent) = sF20,
inference(reorient_equations,[],[f708]) ).
fof(f710,plain,
hBOOL(sF20),
inference(definition_folding,[],[f611,f709,f707,f684,f682,f705,f703,f701,f699,f697,f680,f695,f693]) ).
fof(f711,definition,
sF21 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f712,plain,
c_Message_Omsg_ONonce(v_NB) = sF21,
inference(reorient_equations,[],[f711]) ).
fof(f713,definition,
sF22 = c_Message_Omsg_OCrypt(v_K,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f714,plain,
c_Message_Omsg_OCrypt(v_K,sF21) = sF22,
inference(reorient_equations,[],[f713]) ).
fof(f715,definition,
sF23 = c_Message_Oparts(sF9),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f716,plain,
c_Message_Oparts(sF9) = sF23,
inference(reorient_equations,[],[f715]) ).
fof(f717,definition,
sF24 = c_in(sF22,sF23,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f718,plain,
c_in(sF22,sF23,tc_Message_Omsg) = sF24,
inference(reorient_equations,[],[f717]) ).
fof(f719,plain,
hBOOL(sF24),
inference(definition_folding,[],[f612,f718,f716,f686,f684,f682,f714,f712]) ).
fof(f720,plain,
! [X0] : ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,v_B,v_X),sF19,tc_Event_Oevent)),
inference(definition_folding,[],[f613,f707,f684,f682]) ).
fof(f721,definition,
sF25 = c_Event_Oevent_OSays(v_x,v_B,v_X),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f722,plain,
c_Event_Oevent_OSays(v_x,v_B,v_X) = sF25,
inference(reorient_equations,[],[f721]) ).
fof(f723,definition,
sF26 = c_List_Oset(v_evsf,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f724,plain,
c_List_Oset(v_evsf,tc_Event_Oevent) = sF26,
inference(reorient_equations,[],[f723]) ).
fof(f725,definition,
sF27 = c_in(sF25,sF26,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f726,plain,
c_in(sF25,sF26,tc_Event_Oevent) = sF27,
inference(reorient_equations,[],[f725]) ).
fof(f727,definition,
sF28 = c_Message_Oparts(sF2),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f728,plain,
c_Message_Oparts(sF2) = sF28,
inference(reorient_equations,[],[f727]) ).
fof(f729,definition,
sF29 = c_in(sF22,sF28,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f730,plain,
c_in(sF22,sF28,tc_Message_Omsg) = sF29,
inference(reorient_equations,[],[f729]) ).
fof(f731,definition,
sF30 = c_in(sF18,sF26,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f732,plain,
c_in(sF18,sF26,tc_Event_Oevent) = sF30,
inference(reorient_equations,[],[f731]) ).
fof(f733,definition,
sF31 = c_in(sF6,sF3,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f734,plain,
c_in(sF6,sF3,tc_Message_Omsg) = sF31,
inference(reorient_equations,[],[f733]) ).
fof(f735,plain,
( hBOOL(sF27)
| ~ hBOOL(sF29)
| ~ hBOOL(sF30)
| hBOOL(sF31) ),
inference(definition_folding,[],[f614,f734,f673,f671,f680,f732,f724,f705,f703,f701,f699,f697,f680,f695,f693,f730,f728,f671,f714,f712,f726,f724,f722]) ).
fof(f741,definition,
( spl32_1
<=> hBOOL(sF31) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
fof(f742,plain,
( ~ hBOOL(sF31)
| spl32_1 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f743,plain,
( hBOOL(sF31)
| ~ spl32_1 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f745,definition,
( spl32_2
<=> hBOOL(sF30) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
fof(f747,plain,
( ~ hBOOL(sF30)
| spl32_2 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f749,definition,
( spl32_3
<=> hBOOL(sF29) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
fof(f753,definition,
( spl32_4
<=> hBOOL(sF27) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
fof(f755,plain,
( hBOOL(sF27)
| ~ spl32_4 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f756,plain,
( spl32_1
| ~ spl32_2
| ~ spl32_3
| spl32_4 ),
inference(avatar_split_clause,[],[f735,f753,f749,f745,f741]) ).
fof(f804,plain,
c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)) = sF22,
inference(forward_demodulation,[],[f714,f712]) ).
fof(f816,plain,
( hBOOL(sF11)
| ~ hBOOL(hAPP(sF10,sF6)) ),
inference(superposition,[],[f565,f690]) ).
fof(f821,plain,
( hBOOL(sF29)
| ~ hBOOL(hAPP(sF28,sF22)) ),
inference(superposition,[],[f565,f730]) ).
fof(f829,definition,
( spl32_6
<=> hBOOL(hAPP(sF28,sF22)) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
fof(f831,plain,
( ~ hBOOL(hAPP(sF28,sF22))
| spl32_6 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f832,plain,
( ~ spl32_6
| spl32_3 ),
inference(avatar_split_clause,[],[f821,f749,f829]) ).
fof(f839,plain,
~ hBOOL(hAPP(sF10,sF6)),
inference(forward_subsumption_resolution,[],[f816,f691]) ).
fof(f844,plain,
! [X0] : c_Set_Oinsert(v_Xa,c_Event_Oknows(c_Message_Oagent_OSpy,X0),tc_Message_Omsg) = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(sF7,X0,tc_Event_Oevent)),
inference(superposition,[],[f443,f682]) ).
fof(f852,plain,
( ~ hBOOL(sF24)
| hBOOL(hAPP(sF23,sF22)) ),
inference(superposition,[],[f566,f718]) ).
fof(f857,plain,
hBOOL(hAPP(sF23,sF22)),
inference(forward_subsumption_resolution,[],[f852,f719]) ).
fof(f869,plain,
! [X0,X1] :
( hBOOL(c_in(c_Message_Omsg_OCrypt(X0,X1),sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(X0,X1),sF4,tc_Message_Omsg))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,X0),sF3,tc_Message_Omsg)) ),
inference(superposition,[],[f587,f675]) ).
fof(f902,plain,
! [X0] : ~ hBOOL(hAPP(sF19,c_Event_Oevent_OSays(X0,v_B,v_X))),
inference(resolution,[],[f720,f565]) ).
fof(f904,plain,
~ hBOOL(hAPP(sF19,sF25)),
inference(superposition,[],[f902,f722]) ).
fof(f949,plain,
! [X2,X0,X1] :
( c_Event_Oevent_OSays(X0,X1,X2) != sF18
| c_Message_Oagent_OServer = X0 ),
inference(superposition,[],[f518,f705]) ).
fof(f987,plain,
c_Message_Oparts(sF2) = c_Message_Oparts(sF3),
inference(superposition,[],[f503,f673]) ).
fof(f988,plain,
c_Message_Oparts(sF9) = c_Message_Oparts(sF10),
inference(superposition,[],[f503,f688]) ).
fof(f991,plain,
sF23 = c_Message_Oparts(sF10),
inference(forward_demodulation,[],[f988,f716]) ).
fof(f992,plain,
sF28 = c_Message_Oparts(sF3),
inference(forward_demodulation,[],[f987,f728]) ).
fof(f1064,plain,
sF3 = c_Message_Oanalz(sF3),
inference(superposition,[],[f508,f673]) ).
fof(f1113,plain,
( hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),sF3,tc_Message_Omsg)) ),
inference(superposition,[],[f869,f804]) ).
fof(f1128,plain,
( hBOOL(c_in(sF6,sF3,tc_Message_Omsg))
| hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1113,f680]) ).
fof(f1129,plain,
( hBOOL(sF31)
| hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1128,f734]) ).
fof(f1130,plain,
( hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg))
| spl32_1 ),
inference(forward_subsumption_resolution,[],[f1129,f742]) ).
fof(f1132,definition,
( spl32_20
<=> hBOOL(c_in(sF22,sF4,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl32_20])],[avatar_definition]) ).
fof(f1134,plain,
( ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg))
| spl32_20 ),
inference(avatar_component_clause,[],[f1132]) ).
fof(f1136,definition,
( spl32_21
<=> hBOOL(c_in(sF22,sF3,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
fof(f1138,plain,
( hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1139,plain,
( ~ spl32_20
| spl32_21
| spl32_1 ),
inference(avatar_split_clause,[],[f1130,f741,f1136,f1132]) ).
fof(f1140,plain,
( ~ hBOOL(hAPP(sF4,sF22))
| spl32_20 ),
inference(resolution,[],[f1134,f565]) ).
fof(f1201,plain,
! [X0] :
( ~ hBOOL(c_in(X0,c_List_Oset(sF8,tc_Event_Oevent),tc_Event_Oevent))
| sF7 = X0
| hBOOL(c_in(X0,c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(superposition,[],[f572,f684]) ).
fof(f1202,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF19,tc_Event_Oevent))
| sF7 = X0
| hBOOL(c_in(X0,c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f1201,f707]) ).
fof(f1203,plain,
! [X0] :
( hBOOL(c_in(X0,sF26,tc_Event_Oevent))
| ~ hBOOL(c_in(X0,sF19,tc_Event_Oevent))
| sF7 = X0 ),
inference(forward_demodulation,[],[f1202,f724]) ).
fof(f1207,plain,
( hBOOL(sF30)
| ~ hBOOL(c_in(sF18,sF19,tc_Event_Oevent))
| sF7 = sF18 ),
inference(superposition,[],[f1203,f732]) ).
fof(f1236,plain,
( ~ hBOOL(c_in(sF18,sF19,tc_Event_Oevent))
| sF7 = sF18
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f1207,f747]) ).
fof(f1237,plain,
( ~ hBOOL(sF20)
| sF7 = sF18
| spl32_2 ),
inference(forward_demodulation,[],[f1236,f709]) ).
fof(f1238,plain,
( sF7 = sF18
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f1237,f710]) ).
fof(f1245,plain,
( ! [X2,X0,X1] :
( c_Event_Oevent_OSays(X0,X1,X2) != sF7
| c_Message_Oagent_OServer = X0 )
| spl32_2 ),
inference(backward_demodulation,[],[f949,f1238]) ).
fof(f1346,plain,
( sF7 != sF7
| c_Message_Oagent_OSpy = c_Message_Oagent_OServer
| spl32_2 ),
inference(superposition,[],[f1245,f682]) ).
fof(f1347,plain,
( c_Message_Oagent_OSpy = c_Message_Oagent_OServer
| spl32_2 ),
inference(trivial_inequality_removal,[],[f1346]) ).
fof(f1348,plain,
( $false
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f1347,f578]) ).
fof(f1349,plain,
spl32_2,
inference(avatar_contradiction_clause,[],[f1348]) ).
fof(f1388,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,sF8) = c_Set_Oinsert(v_Xa,c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf),tc_Message_Omsg),
inference(superposition,[],[f844,f684]) ).
fof(f1391,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,sF8) = c_Set_Oinsert(v_Xa,sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f1388,f671]) ).
fof(f1392,plain,
sF9 = c_Set_Oinsert(v_Xa,sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f1391,f686]) ).
fof(f1394,plain,
! [X0] :
( hBOOL(c_in(X0,c_Message_Oanalz(sF9),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Message_Oanalz(sF2),tc_Message_Omsg)) ),
inference(superposition,[],[f233,f1392]) ).
fof(f1395,plain,
( c_Message_Osynth(c_Message_Oanalz(sF2)) = c_Message_Osynth(c_Message_Oanalz(sF9))
| ~ hBOOL(c_in(v_Xa,c_Message_Osynth(c_Message_Oanalz(sF2)),tc_Message_Omsg)) ),
inference(superposition,[],[f419,f1392]) ).
fof(f1412,plain,
( c_Message_Osynth(c_Message_Oanalz(sF2)) = c_Message_Osynth(sF10)
| ~ hBOOL(c_in(v_Xa,c_Message_Osynth(c_Message_Oanalz(sF2)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1395,f688]) ).
fof(f1413,plain,
! [X0] :
( hBOOL(c_in(X0,sF10,tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Message_Oanalz(sF2),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1394,f688]) ).
fof(f1415,plain,
( c_Message_Osynth(sF3) = c_Message_Osynth(sF10)
| ~ hBOOL(c_in(v_Xa,c_Message_Osynth(c_Message_Oanalz(sF2)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1412,f673]) ).
fof(f1416,plain,
! [X0] :
( hBOOL(c_in(X0,sF10,tc_Message_Omsg))
| ~ hBOOL(c_in(X0,sF3,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1413,f673]) ).
fof(f1417,plain,
( sF4 = c_Message_Osynth(sF10)
| ~ hBOOL(c_in(v_Xa,c_Message_Osynth(c_Message_Oanalz(sF2)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1415,f675]) ).
fof(f1418,plain,
( ~ hBOOL(c_in(v_Xa,c_Message_Osynth(sF3),tc_Message_Omsg))
| sF4 = c_Message_Osynth(sF10) ),
inference(forward_demodulation,[],[f1417,f673]) ).
fof(f1419,plain,
( ~ hBOOL(c_in(v_Xa,sF4,tc_Message_Omsg))
| sF4 = c_Message_Osynth(sF10) ),
inference(forward_demodulation,[],[f1418,f675]) ).
fof(f1420,plain,
( ~ hBOOL(sF5)
| sF4 = c_Message_Osynth(sF10) ),
inference(forward_demodulation,[],[f1419,f677]) ).
fof(f1421,plain,
sF4 = c_Message_Osynth(sF10),
inference(forward_subsumption_resolution,[],[f1420,f678]) ).
fof(f1431,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF3,tc_Message_Omsg))
| hBOOL(hAPP(sF10,X0)) ),
inference(resolution,[],[f1416,f566]) ).
fof(f1439,plain,
( ~ hBOOL(sF31)
| hBOOL(hAPP(sF10,sF6)) ),
inference(superposition,[],[f1431,f734]) ).
fof(f1521,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Message_Oparts(c_Message_Osynth(X0)),X1))
| ~ hBOOL(hAPP(c_Message_Oparts(X0),X1)) ),
inference(superposition,[],[f41,f261]) ).
fof(f1637,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(hAPP(c_Message_Oparts(X1),X0)) ),
inference(resolution,[],[f607,f566]) ).
fof(f1863,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Message_Oparts(X0),X1))
| ~ hBOOL(hAPP(c_Message_Oanalz(X0),X1)) ),
inference(resolution,[],[f1637,f565]) ).
fof(f1886,plain,
! [X0] :
( hBOOL(hAPP(sF28,X0))
| ~ hBOOL(hAPP(c_Message_Oanalz(sF3),X0)) ),
inference(superposition,[],[f1863,f992]) ).
fof(f1895,plain,
! [X0] :
( hBOOL(hAPP(sF28,X0))
| ~ hBOOL(hAPP(sF3,X0)) ),
inference(forward_demodulation,[],[f1886,f1064]) ).
fof(f1899,plain,
( ~ hBOOL(hAPP(sF3,sF22))
| spl32_6 ),
inference(resolution,[],[f1895,f831]) ).
fof(f1916,plain,
! [X2,X3,X0,X1] :
( hBOOL(c_in(X3,c_List_Oset(c_List_Olist_OCons(X0,X1,X2),X2),X2))
| ~ hBOOL(c_in(X3,c_List_Oset(X1,X2),X2)) ),
inference(superposition,[],[f290,f225]) ).
fof(f1941,plain,
! [X0] :
( hBOOL(c_in(X0,c_List_Oset(sF8,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X0,c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(superposition,[],[f1916,f684]) ).
fof(f1944,plain,
! [X0] :
( hBOOL(c_in(X0,sF19,tc_Event_Oevent))
| ~ hBOOL(c_in(X0,c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f1941,f707]) ).
fof(f1945,plain,
! [X0] :
( hBOOL(c_in(X0,sF19,tc_Event_Oevent))
| ~ hBOOL(c_in(X0,sF26,tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f1944,f724]) ).
fof(f1947,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF26,tc_Event_Oevent))
| hBOOL(hAPP(sF19,X0)) ),
inference(resolution,[],[f1945,f566]) ).
fof(f1967,plain,
( ~ hBOOL(sF27)
| hBOOL(hAPP(sF19,sF25)) ),
inference(superposition,[],[f1947,f726]) ).
fof(f2036,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_Message_Oparts(c_Message_Osynth(X0)),X1))
| hBOOL(hAPP(c_Message_Oparts(X0),X1))
| hBOOL(hAPP(c_Message_Osynth(X0),X1)) ),
inference(superposition,[],[f43,f261]) ).
fof(f2048,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| hBOOL(hAPP(c_Message_Oparts(sF3),X0))
| hBOOL(hAPP(sF4,X0)) ),
inference(superposition,[],[f2036,f675]) ).
fof(f2052,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| hBOOL(hAPP(sF28,X0))
| hBOOL(hAPP(sF4,X0)) ),
inference(forward_demodulation,[],[f2048,f992]) ).
fof(f2546,plain,
! [X0] :
( hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| ~ hBOOL(hAPP(c_Message_Oparts(sF10),X0)) ),
inference(superposition,[],[f1521,f1421]) ).
fof(f2547,plain,
! [X0] :
( hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| ~ hBOOL(hAPP(sF23,X0)) ),
inference(forward_demodulation,[],[f2546,f991]) ).
fof(f2550,plain,
! [X0] :
( hBOOL(hAPP(sF28,X0))
| ~ hBOOL(hAPP(sF23,X0))
| hBOOL(hAPP(sF4,X0)) ),
inference(resolution,[],[f2547,f2052]) ).
fof(f2554,plain,
( ~ hBOOL(hAPP(sF23,sF22))
| hBOOL(hAPP(sF4,sF22))
| spl32_6 ),
inference(resolution,[],[f2550,f831]) ).
fof(f2556,plain,
( hBOOL(hAPP(sF4,sF22))
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f2554,f857]) ).
fof(f2557,plain,
( $false
| spl32_6
| spl32_20 ),
inference(forward_subsumption_resolution,[],[f2556,f1140]) ).
fof(f2558,plain,
( spl32_6
| spl32_20 ),
inference(avatar_contradiction_clause,[],[f2557]) ).
fof(f2561,plain,
( hBOOL(hAPP(sF3,sF22))
| ~ spl32_21 ),
inference(resolution,[],[f1138,f566]) ).
fof(f2562,plain,
( $false
| spl32_6
| ~ spl32_21 ),
inference(forward_subsumption_resolution,[],[f2561,f1899]) ).
fof(f2563,plain,
( spl32_6
| ~ spl32_21 ),
inference(avatar_contradiction_clause,[],[f2562]) ).
fof(f2568,plain,
( hBOOL(hAPP(sF10,sF6))
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f1439,f743]) ).
fof(f2569,plain,
( $false
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f2568,f839]) ).
fof(f2570,plain,
~ spl32_1,
inference(avatar_contradiction_clause,[],[f2569]) ).
fof(f2582,plain,
( hBOOL(hAPP(sF19,sF25))
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f1967,f755]) ).
fof(f2584,plain,
( $false
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f2582,f904]) ).
fof(f2585,plain,
~ spl32_4,
inference(avatar_contradiction_clause,[],[f2584]) ).
cnf(s1,plain,
( spl32_1
| ~ spl32_2
| ~ spl32_3
| spl32_4 ),
inference(sat_conversion,[],[f756]) ).
cnf(s3,plain,
( spl32_3
| ~ spl32_6 ),
inference(sat_conversion,[],[f832]) ).
cnf(s13,plain,
( spl32_1
| ~ spl32_20
| spl32_21 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s22,plain,
spl32_2,
inference(sat_conversion,[],[f1349]) ).
cnf(s42,plain,
( spl32_6
| spl32_20 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s43,plain,
( spl32_6
| ~ spl32_21 ),
inference(sat_conversion,[],[f2563]) ).
cnf(s46,plain,
~ spl32_1,
inference(sat_conversion,[],[f2570]) ).
cnf(s51,plain,
~ spl32_4,
inference(sat_conversion,[],[f2585]) ).
cnf(s55,plain,
( ~ spl32_20
| spl32_21 ),
inference(rat,[],[s13,s46]) ).
cnf(s56,plain,
~ spl32_3,
inference(rat,[],[s1,s51,s22,s46]) ).
cnf(s57,plain,
~ spl32_6,
inference(rat,[],[s3,s56]) ).
cnf(s58,plain,
~ spl32_21,
inference(rat,[],[s43,s57]) ).
cnf(s59,plain,
spl32_20,
inference(rat,[],[s42,s57]) ).
cnf(s60,plain,
$false,
inference(rat,[],[s55,s58,s59]) ).
fof(f2586,plain,
$false,
inference(avatar_sat_refutation,[],[s60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV760-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 % Computer : n017.cluster.edu
% 0.10/0.24 % Model : x86_64 x86_64
% 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24 % Memory : 8046.5625MB
% 0.10/0.24 % OS : Linux 6.8.0-71-generic
% 0.10/0.24 % CPULimit : 300
% 0.10/0.24 % WCLimit : 300
% 0.10/0.24 % DateTime : Mon Sep 28 12:24:36 UTC 2026
% 0.10/0.24 % CPUTime :
% 0.10/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.28 Running first-order theorem proving
% 0.10/0.28 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.09/2.54 % (3509102)Input is clausal, will run a generic CNF schedule.
% 10.09/2.54 % (3509125)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2245816646:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.09/2.54 % (3509127)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1240384076:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.09/2.54 % (3509123)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=339457252:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.09/2.54 % (3509124)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3419841948:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.09/2.54 % (3509126)lrs+10_1_sil=8000:sp=occurrence:random_seed=2649900214:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.09/2.54 % (3509129)dis-21_1_sil=8000:lcm=predicate:random_seed=4144964437:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.09/2.54 % (3509128)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1440264109:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.09/2.54 % (3509127)Instruction limit reached!
% 10.09/2.54 % (3509127)------------------------------
% 10.09/2.54 % (3509127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509127)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509127)Termination reason: Instruction limit
% 10.09/2.54 % (3509127)Termination phase: Saturation
% 10.09/2.54 % (3509127)Time elapsed: 0.131 s
% 10.09/2.54 % (3509127)Peak memory usage: 89 MB
% 10.09/2.54 % (3509127)Instructions burned: 115 (million)
% 10.09/2.54 % (3509126)Instruction limit reached!
% 10.09/2.54 % (3509126)------------------------------
% 10.09/2.54 % (3509126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509126)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509126)Termination reason: Instruction limit
% 10.09/2.54 % (3509126)Termination phase: Saturation
% 10.09/2.54 % (3509126)Time elapsed: 0.115 s
% 10.09/2.54 % (3509126)Peak memory usage: 89 MB
% 10.09/2.54 % (3509126)Instructions burned: 107 (million)
% 10.09/2.54 % (3509129)Instruction limit reached!
% 10.09/2.54 % (3509129)------------------------------
% 10.09/2.54 % (3509129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509129)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509129)Termination reason: Instruction limit
% 10.09/2.54 % (3509129)Termination phase: Saturation
% 10.09/2.54 % (3509129)Time elapsed: 0.115 s
% 10.09/2.54 % (3509129)Peak memory usage: 89 MB
% 10.09/2.54 % (3509129)Instructions burned: 118 (million)
% 10.09/2.54 % (3509128)Instruction limit reached!
% 10.09/2.54 % (3509128)------------------------------
% 10.09/2.54 % (3509128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509128)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509128)Termination reason: Instruction limit
% 10.09/2.54 % (3509128)Termination phase: Saturation
% 10.09/2.54 % (3509128)Time elapsed: 0.191 s
% 10.09/2.54 % (3509128)Peak memory usage: 90 MB
% 10.09/2.54 % (3509128)Instructions burned: 180 (million)
% 10.09/2.54 % (3509141)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4060358203:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 10.09/2.54 % (3509139)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1191915368:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 10.09/2.54 % (3509140)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1910558973:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 10.09/2.54 % (3509142)lrs+10_64_to=lpo:sil=8000:random_seed=3461940334:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 10.09/2.54 % (3509139)Instruction limit reached!
% 10.09/2.54 % (3509139)------------------------------
% 10.09/2.54 % (3509139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509139)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509139)Termination reason: Instruction limit
% 10.09/2.54 % (3509139)Termination phase: Saturation
% 10.09/2.54 % (3509139)Time elapsed: 0.150 s
% 10.09/2.54 % (3509139)Peak memory usage: 89 MB
% 10.09/2.54 % (3509139)Instructions burned: 143 (million)
% 10.09/2.54 % (3509141)Instruction limit reached!
% 10.09/2.54 % (3509141)------------------------------
% 10.09/2.54 % (3509141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509141)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509141)Termination reason: Instruction limit
% 10.09/2.54 % (3509141)Termination phase: Saturation
% 10.09/2.54 % (3509141)Time elapsed: 0.172 s
% 10.09/2.54 % (3509141)Peak memory usage: 90 MB
% 10.09/2.54 % (3509141)Instructions burned: 220 (million)
% 10.09/2.54 % (3509140)Instruction limit reached!
% 10.09/2.54 % (3509140)------------------------------
% 10.09/2.54 % (3509140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509140)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509140)Termination reason: Instruction limit
% 10.09/2.54 % (3509140)Termination phase: Saturation
% 10.09/2.54 % (3509140)Time elapsed: 0.181 s
% 10.09/2.54 % (3509140)Peak memory usage: 91 MB
% 10.09/2.54 % (3509140)Instructions burned: 190 (million)
% 10.09/2.54 % (3509142)Instruction limit reached!
% 10.09/2.54 % (3509142)------------------------------
% 10.09/2.54 % (3509142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509142)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509142)Termination reason: Instruction limit
% 10.09/2.54 % (3509142)Termination phase: Saturation
% 10.09/2.54 % (3509142)Time elapsed: 0.134 s
% 10.09/2.54 % (3509142)Peak memory usage: 90 MB
% 10.09/2.54 % (3509142)Instructions burned: 126 (million)
% 10.09/2.54 % (3509148)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=611549083:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 10.09/2.54 % (3509147)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1438007733:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 10.09/2.54 % (3509150)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1138573093:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 10.09/2.54 % (3509149)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1100248766:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 10.09/2.54 % (3509148)Instruction limit reached!
% 10.09/2.54 % (3509148)------------------------------
% 10.09/2.54 % (3509148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509148)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509148)Termination reason: Instruction limit
% 10.09/2.54 % (3509148)Termination phase: Saturation
% 10.09/2.54 % (3509148)Time elapsed: 0.172 s
% 10.09/2.54 % (3509148)Peak memory usage: 91 MB
% 10.09/2.54 % (3509148)Instructions burned: 157 (million)
% 10.09/2.54 % (3509150)Instruction limit reached!
% 10.09/2.54 % (3509150)------------------------------
% 10.09/2.54 % (3509150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509150)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509150)Termination reason: Instruction limit
% 10.09/2.54 % (3509150)Termination phase: Saturation
% 10.09/2.54 % (3509150)Time elapsed: 0.104 s
% 10.09/2.54 % (3509150)Peak memory usage: 89 MB
% 10.09/2.54 % (3509150)Instructions burned: 107 (million)
% 10.09/2.54 % (3509147)Instruction limit reached!
% 10.09/2.54 % (3509147)------------------------------
% 10.09/2.54 % (3509147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509147)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509147)Termination reason: Instruction limit
% 10.09/2.54 % (3509147)Termination phase: Saturation
% 10.09/2.54 % (3509147)Time elapsed: 0.195 s
% 10.09/2.54 % (3509147)Peak memory usage: 90 MB
% 10.09/2.54 % (3509147)Instructions burned: 195 (million)
% 10.09/2.54 % (3509155)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3257796996:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 10.09/2.54 % (3509125)First to succeed.
% 10.09/2.54 % (3509125)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3509102"
% 10.09/2.54 % (3509156)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=143323194:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 10.09/2.54 % (3509155)Instruction limit reached!
% 10.09/2.54 % (3509155)------------------------------
% 10.09/2.54 % (3509155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.09/2.54 % (3509155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.09/2.54 % (3509155)CaDiCaL version: 2.1.3
% 10.09/2.54 % (3509155)Termination reason: Instruction limit
% 10.09/2.54 % (3509155)Termination phase: Saturation
% 10.09/2.54 % (3509155)Time elapsed: 0.113 s
% 10.09/2.54 % (3509155)Peak memory usage: 90 MB
% 10.09/2.54 % (3509155)Instructions burned: 107 (million)
% 10.09/2.54 % (3509157)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3857997131:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi)
% 10.09/2.54 % (3509125)Refutation found. Thanks to Tanya!
% 10.09/2.54 % SZS status Unsatisfiable for theBenchmark
% 10.09/2.54 % SZS output start Proof for theBenchmark
% See solution above
% 11.56/2.88 % (3509125)------------------------------
% 11.56/2.88 % (3509125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.88 % (3509125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.88 % (3509125)CaDiCaL version: 2.1.3
% 11.56/2.88 % (3509125)Termination reason: Refutation
% 11.56/2.88 % (3509125)Time elapsed: 1.093 s
% 11.56/2.88 % (3509125)Peak memory usage: 139 MB
% 11.56/2.88 % (3509125)Instructions burned: 1846 (million)
% 11.56/2.88 % (3509125)------------------------------
% 11.56/2.88 % (3509125)------------------------------
% 11.56/2.88 % (3509102)Success in time 1.527 s
% 11.56/2.88 % Vampire exiting
%------------------------------------------------------------------------------