%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV755-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:25 PM UTC 2026
% Result : Unsatisfiable 10.66s 2.17s
% Output : Refutation 11.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 61
% Syntax : Number of formulae : 206 ( 106 unt; 38 def)
% Number of atoms : 339 ( 107 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 237 ( 104 ~; 126 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 2 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 : 91 ( 0 sgn 91 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,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/sandbox2/benchmark/theBenchmark.p',cls_sup1CI_1) ).
fof(f41,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/sandbox2/benchmark/theBenchmark.p',cls_sup1E_0) ).
fof(f226,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/sandbox2/benchmark/theBenchmark.p',cls_List_Oset_Osimps_I2_J_0) ).
fof(f234,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/sandbox2/benchmark/theBenchmark.p',cls_analz__insertI_0) ).
fof(f262,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/sandbox2/benchmark/theBenchmark.p',cls_parts__synth_0) ).
fof(f288,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/sandbox2/benchmark/theBenchmark.p',cls_insertCI_0) ).
fof(f417,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/sandbox2/benchmark/theBenchmark.p',cls_Fake__analz__eq_0) ).
fof(f418,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,[],[f417]) ).
fof(f444,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/sandbox2/benchmark/theBenchmark.p',cls_knows__Spy__Says_0) ).
fof(f501,axiom,
! [X0] : c_Message_Oparts(c_Message_Oanalz(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_parts__analz_0) ).
fof(f502,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oparts(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f501]) ).
fof(f506,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(f507,plain,
! [X0] : c_Message_Oanalz(X0) = c_Message_Oanalz(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f506]) ).
fof(f517,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/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I1_J_0) ).
fof(f563,axiom,
! [X2,X0,X1] :
( hBOOL(c_in(X0,X1,X2))
| ~ hBOOL(hAPP(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f564,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(X1,X0,X2))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f570,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/sandbox2/benchmark/theBenchmark.p',cls_set__ConsD_0) ).
fof(f576,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I5_J_0) ).
fof(f585,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/sandbox2/benchmark/theBenchmark.p',cls_Crypt__synth_1) ).
fof(f605,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/sandbox2/benchmark/theBenchmark.p',cls_analz__conj__parts_0) ).
fof(f607,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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f608,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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f609,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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f610,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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f611,negated_conjecture,
~ hBOOL(c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB))),c_List_Oset(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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f612,negated_conjecture,
( hBOOL(c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f668,definition,
sF2 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f669,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf) = sF2,
inference(reorient_equations,[],[f668]) ).
fof(f670,definition,
sF3 = c_Message_Oanalz(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f671,plain,
c_Message_Oanalz(sF2) = sF3,
inference(reorient_equations,[],[f670]) ).
fof(f672,definition,
sF4 = c_Message_Osynth(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f673,plain,
c_Message_Osynth(sF3) = sF4,
inference(reorient_equations,[],[f672]) ).
fof(f674,definition,
sF5 = c_in(v_Xa,sF4,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f675,plain,
c_in(v_Xa,sF4,tc_Message_Omsg) = sF5,
inference(reorient_equations,[],[f674]) ).
fof(f676,plain,
hBOOL(sF5),
inference(definition_folding,[],[f607,f675,f673,f671,f669]) ).
fof(f677,definition,
sF6 = hAPP(c_Message_Omsg_OKey,v_K),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f678,plain,
hAPP(c_Message_Omsg_OKey,v_K) = sF6,
inference(reorient_equations,[],[f677]) ).
fof(f679,definition,
sF7 = c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f680,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OSpy,v_Ba,v_Xa) = sF7,
inference(reorient_equations,[],[f679]) ).
fof(f681,definition,
sF8 = c_List_Olist_OCons(sF7,v_evsf,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f682,plain,
c_List_Olist_OCons(sF7,v_evsf,tc_Event_Oevent) = sF8,
inference(reorient_equations,[],[f681]) ).
fof(f683,definition,
sF9 = c_Event_Oknows(c_Message_Oagent_OSpy,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f684,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,sF8) = sF9,
inference(reorient_equations,[],[f683]) ).
fof(f685,definition,
sF10 = c_Message_Oanalz(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f686,plain,
c_Message_Oanalz(sF9) = sF10,
inference(reorient_equations,[],[f685]) ).
fof(f687,definition,
sF11 = c_in(sF6,sF10,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f688,plain,
c_in(sF6,sF10,tc_Message_Omsg) = sF11,
inference(reorient_equations,[],[f687]) ).
fof(f689,plain,
~ hBOOL(sF11),
inference(definition_folding,[],[f608,f688,f686,f684,f682,f680,f678]) ).
fof(f690,definition,
sF12 = hAPP(c_Public_OshrK,v_A),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f691,plain,
hAPP(c_Public_OshrK,v_A) = sF12,
inference(reorient_equations,[],[f690]) ).
fof(f692,definition,
sF13 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f693,plain,
c_Message_Omsg_OAgent(v_B) = sF13,
inference(reorient_equations,[],[f692]) ).
fof(f694,definition,
sF14 = c_Message_Omsg_OMPair(sF6,v_X),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f695,plain,
c_Message_Omsg_OMPair(sF6,v_X) = sF14,
inference(reorient_equations,[],[f694]) ).
fof(f696,definition,
sF15 = c_Message_Omsg_OMPair(sF13,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f697,plain,
c_Message_Omsg_OMPair(sF13,sF14) = sF15,
inference(reorient_equations,[],[f696]) ).
fof(f698,definition,
sF16 = c_Message_Omsg_OMPair(v_NA,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f699,plain,
c_Message_Omsg_OMPair(v_NA,sF15) = sF16,
inference(reorient_equations,[],[f698]) ).
fof(f700,definition,
sF17 = c_Message_Omsg_OCrypt(sF12,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f701,plain,
c_Message_Omsg_OCrypt(sF12,sF16) = sF17,
inference(reorient_equations,[],[f700]) ).
fof(f702,definition,
sF18 = c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f703,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,sF17) = sF18,
inference(reorient_equations,[],[f702]) ).
fof(f704,definition,
sF19 = c_List_Oset(sF8,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f705,plain,
c_List_Oset(sF8,tc_Event_Oevent) = sF19,
inference(reorient_equations,[],[f704]) ).
fof(f706,definition,
sF20 = c_in(sF18,sF19,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f707,plain,
c_in(sF18,sF19,tc_Event_Oevent) = sF20,
inference(reorient_equations,[],[f706]) ).
fof(f708,plain,
hBOOL(sF20),
inference(definition_folding,[],[f609,f707,f705,f682,f680,f703,f701,f699,f697,f695,f678,f693,f691]) ).
fof(f709,definition,
sF21 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f710,plain,
c_Message_Omsg_ONonce(v_NB) = sF21,
inference(reorient_equations,[],[f709]) ).
fof(f711,definition,
sF22 = c_Message_Omsg_OCrypt(v_K,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f712,plain,
c_Message_Omsg_OCrypt(v_K,sF21) = sF22,
inference(reorient_equations,[],[f711]) ).
fof(f713,definition,
sF23 = c_Message_Oparts(sF9),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f714,plain,
c_Message_Oparts(sF9) = sF23,
inference(reorient_equations,[],[f713]) ).
fof(f715,definition,
sF24 = c_in(sF22,sF23,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f716,plain,
c_in(sF22,sF23,tc_Message_Omsg) = sF24,
inference(reorient_equations,[],[f715]) ).
fof(f717,plain,
hBOOL(sF24),
inference(definition_folding,[],[f610,f716,f714,f684,f682,f680,f712,f710]) ).
fof(f718,definition,
sF25 = c_Event_Oevent_OSays(v_B,v_A,sF22),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f719,plain,
c_Event_Oevent_OSays(v_B,v_A,sF22) = sF25,
inference(reorient_equations,[],[f718]) ).
fof(f720,definition,
sF26 = c_in(sF25,sF19,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f721,plain,
c_in(sF25,sF19,tc_Event_Oevent) = sF26,
inference(reorient_equations,[],[f720]) ).
fof(f722,plain,
~ hBOOL(sF26),
inference(definition_folding,[],[f611,f721,f705,f682,f680,f719,f712,f710]) ).
fof(f723,definition,
sF27 = c_List_Oset(v_evsf,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f724,plain,
c_List_Oset(v_evsf,tc_Event_Oevent) = sF27,
inference(reorient_equations,[],[f723]) ).
fof(f725,definition,
sF28 = c_in(sF25,sF27,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f726,plain,
c_in(sF25,sF27,tc_Event_Oevent) = sF28,
inference(reorient_equations,[],[f725]) ).
fof(f727,definition,
sF29 = c_Message_Oparts(sF2),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f728,plain,
c_Message_Oparts(sF2) = sF29,
inference(reorient_equations,[],[f727]) ).
fof(f729,definition,
sF30 = c_in(sF22,sF29,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f730,plain,
c_in(sF22,sF29,tc_Message_Omsg) = sF30,
inference(reorient_equations,[],[f729]) ).
fof(f731,definition,
sF31 = c_in(sF18,sF27,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f732,plain,
c_in(sF18,sF27,tc_Event_Oevent) = sF31,
inference(reorient_equations,[],[f731]) ).
fof(f733,definition,
sF32 = c_in(sF6,sF3,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f734,plain,
c_in(sF6,sF3,tc_Message_Omsg) = sF32,
inference(reorient_equations,[],[f733]) ).
fof(f735,plain,
( hBOOL(sF28)
| ~ hBOOL(sF30)
| ~ hBOOL(sF31)
| hBOOL(sF32) ),
inference(definition_folding,[],[f612,f734,f671,f669,f678,f732,f724,f703,f701,f699,f697,f695,f678,f693,f691,f730,f728,f669,f712,f710,f726,f724,f719,f712,f710]) ).
fof(f741,definition,
( spl33_1
<=> hBOOL(sF32) ),
introduced(definition,[new_symbols(definition,[spl33_1])],[avatar_definition]) ).
fof(f742,plain,
( ~ hBOOL(sF32)
| spl33_1 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f743,plain,
( hBOOL(sF32)
| ~ spl33_1 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f745,definition,
( spl33_2
<=> hBOOL(sF31) ),
introduced(definition,[new_symbols(definition,[spl33_2])],[avatar_definition]) ).
fof(f747,plain,
( ~ hBOOL(sF31)
| spl33_2 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f749,definition,
( spl33_3
<=> hBOOL(sF30) ),
introduced(definition,[new_symbols(definition,[spl33_3])],[avatar_definition]) ).
fof(f753,definition,
( spl33_4
<=> hBOOL(sF28) ),
introduced(definition,[new_symbols(definition,[spl33_4])],[avatar_definition]) ).
fof(f755,plain,
( hBOOL(sF28)
| ~ spl33_4 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f756,plain,
( spl33_1
| ~ spl33_2
| ~ spl33_3
| spl33_4 ),
inference(avatar_split_clause,[],[f735,f753,f749,f745,f741]) ).
fof(f802,plain,
c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)) = sF22,
inference(forward_demodulation,[],[f712,f710]) ).
fof(f814,plain,
( hBOOL(sF11)
| ~ hBOOL(hAPP(sF10,sF6)) ),
inference(superposition,[],[f563,f688]) ).
fof(f819,plain,
( hBOOL(sF30)
| ~ hBOOL(hAPP(sF29,sF22)) ),
inference(superposition,[],[f563,f730]) ).
fof(f820,plain,
( hBOOL(sF26)
| ~ hBOOL(hAPP(sF19,sF25)) ),
inference(superposition,[],[f563,f721]) ).
fof(f827,plain,
~ hBOOL(hAPP(sF19,sF25)),
inference(forward_subsumption_resolution,[],[f820,f722]) ).
fof(f829,definition,
( spl33_6
<=> hBOOL(hAPP(sF29,sF22)) ),
introduced(definition,[new_symbols(definition,[spl33_6])],[avatar_definition]) ).
fof(f831,plain,
( ~ hBOOL(hAPP(sF29,sF22))
| spl33_6 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f832,plain,
( ~ spl33_6
| spl33_3 ),
inference(avatar_split_clause,[],[f819,f749,f829]) ).
fof(f839,plain,
~ hBOOL(hAPP(sF10,sF6)),
inference(forward_subsumption_resolution,[],[f814,f689]) ).
fof(f847,plain,
( ~ hBOOL(sF24)
| hBOOL(hAPP(sF23,sF22)) ),
inference(superposition,[],[f564,f716]) ).
fof(f853,plain,
hBOOL(hAPP(sF23,sF22)),
inference(forward_subsumption_resolution,[],[f847,f717]) ).
fof(f863,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,[],[f444,f680]) ).
fof(f917,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,[],[f585,f673]) ).
fof(f925,plain,
! [X2,X0,X1] :
( c_Event_Oevent_OSays(X0,X1,X2) != sF18
| c_Message_Oagent_OServer = X0 ),
inference(superposition,[],[f517,f703]) ).
fof(f984,plain,
c_Message_Oparts(sF2) = c_Message_Oparts(sF3),
inference(superposition,[],[f502,f671]) ).
fof(f985,plain,
c_Message_Oparts(sF9) = c_Message_Oparts(sF10),
inference(superposition,[],[f502,f686]) ).
fof(f988,plain,
sF23 = c_Message_Oparts(sF10),
inference(forward_demodulation,[],[f985,f714]) ).
fof(f989,plain,
sF29 = c_Message_Oparts(sF3),
inference(forward_demodulation,[],[f984,f728]) ).
fof(f1028,plain,
sF3 = c_Message_Oanalz(sF3),
inference(superposition,[],[f507,f671]) ).
fof(f1082,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,[],[f570,f682]) ).
fof(f1083,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,[],[f1082,f705]) ).
fof(f1084,plain,
! [X0] :
( hBOOL(c_in(X0,sF27,tc_Event_Oevent))
| ~ hBOOL(c_in(X0,sF19,tc_Event_Oevent))
| sF7 = X0 ),
inference(forward_demodulation,[],[f1083,f724]) ).
fof(f1086,plain,
( hBOOL(sF31)
| ~ hBOOL(c_in(sF18,sF19,tc_Event_Oevent))
| sF7 = sF18 ),
inference(superposition,[],[f1084,f732]) ).
fof(f1089,plain,
( ~ hBOOL(c_in(sF18,sF19,tc_Event_Oevent))
| sF7 = sF18
| spl33_2 ),
inference(forward_subsumption_resolution,[],[f1086,f747]) ).
fof(f1091,plain,
( ~ hBOOL(sF20)
| sF7 = sF18
| spl33_2 ),
inference(forward_demodulation,[],[f1089,f707]) ).
fof(f1092,plain,
( sF7 = sF18
| spl33_2 ),
inference(forward_subsumption_resolution,[],[f1091,f708]) ).
fof(f1100,plain,
( ! [X2,X0,X1] :
( c_Event_Oevent_OSays(X0,X1,X2) != sF7
| c_Message_Oagent_OServer = X0 )
| spl33_2 ),
inference(backward_demodulation,[],[f925,f1092]) ).
fof(f1200,plain,
( sF7 != sF7
| c_Message_Oagent_OSpy = c_Message_Oagent_OServer
| spl33_2 ),
inference(superposition,[],[f1100,f680]) ).
fof(f1201,plain,
( c_Message_Oagent_OSpy = c_Message_Oagent_OServer
| spl33_2 ),
inference(trivial_inequality_removal,[],[f1200]) ).
fof(f1202,plain,
( $false
| spl33_2 ),
inference(forward_subsumption_resolution,[],[f1201,f576]) ).
fof(f1203,plain,
spl33_2,
inference(avatar_contradiction_clause,[],[f1202]) ).
fof(f1266,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,[],[f863,f682]) ).
fof(f1269,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,sF8) = c_Set_Oinsert(v_Xa,sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f1266,f669]) ).
fof(f1270,plain,
sF9 = c_Set_Oinsert(v_Xa,sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f1269,f684]) ).
fof(f1272,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,[],[f418,f1270]) ).
fof(f1289,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,[],[f1272,f686]) ).
fof(f1291,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,[],[f1289,f671]) ).
fof(f1292,plain,
( sF4 = c_Message_Osynth(sF10)
| ~ hBOOL(c_in(v_Xa,c_Message_Osynth(c_Message_Oanalz(sF2)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1291,f673]) ).
fof(f1293,plain,
( ~ hBOOL(c_in(v_Xa,c_Message_Osynth(sF3),tc_Message_Omsg))
| sF4 = c_Message_Osynth(sF10) ),
inference(forward_demodulation,[],[f1292,f671]) ).
fof(f1294,plain,
( ~ hBOOL(c_in(v_Xa,sF4,tc_Message_Omsg))
| sF4 = c_Message_Osynth(sF10) ),
inference(forward_demodulation,[],[f1293,f673]) ).
fof(f1295,plain,
( ~ hBOOL(sF5)
| sF4 = c_Message_Osynth(sF10) ),
inference(forward_demodulation,[],[f1294,f675]) ).
fof(f1296,plain,
sF4 = c_Message_Osynth(sF10),
inference(forward_subsumption_resolution,[],[f1295,f676]) ).
fof(f1373,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Message_Oparts(c_Message_Osynth(X0)),X1))
| ~ hBOOL(hAPP(c_Message_Oparts(X0),X1)) ),
inference(superposition,[],[f39,f262]) ).
fof(f1435,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,[],[f234,f1270]) ).
fof(f1436,plain,
! [X0] :
( hBOOL(c_in(X0,sF10,tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Message_Oanalz(sF2),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1435,f686]) ).
fof(f1437,plain,
! [X0] :
( hBOOL(c_in(X0,sF10,tc_Message_Omsg))
| ~ hBOOL(c_in(X0,sF3,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1436,f671]) ).
fof(f1438,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF3,tc_Message_Omsg))
| hBOOL(hAPP(sF10,X0)) ),
inference(resolution,[],[f1437,f564]) ).
fof(f1444,plain,
( ~ hBOOL(sF32)
| hBOOL(hAPP(sF10,sF6)) ),
inference(superposition,[],[f1438,f734]) ).
fof(f1601,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(hAPP(c_Message_Oparts(X1),X0)) ),
inference(resolution,[],[f605,f564]) ).
fof(f1677,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,[],[f917,f802]) ).
fof(f1679,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,[],[f1677,f678]) ).
fof(f1680,plain,
( hBOOL(sF32)
| hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1679,f734]) ).
fof(f1681,plain,
( hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg))
| spl33_1 ),
inference(forward_subsumption_resolution,[],[f1680,f742]) ).
fof(f1683,definition,
( spl33_34
<=> hBOOL(c_in(sF22,sF4,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl33_34])],[avatar_definition]) ).
fof(f1685,plain,
( ~ hBOOL(c_in(sF22,sF4,tc_Message_Omsg))
| spl33_34 ),
inference(avatar_component_clause,[],[f1683]) ).
fof(f1687,definition,
( spl33_35
<=> hBOOL(c_in(sF22,sF3,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl33_35])],[avatar_definition]) ).
fof(f1689,plain,
( hBOOL(c_in(sF22,sF3,tc_Message_Omsg))
| ~ spl33_35 ),
inference(avatar_component_clause,[],[f1687]) ).
fof(f1690,plain,
( ~ spl33_34
| spl33_35
| spl33_1 ),
inference(avatar_split_clause,[],[f1681,f741,f1687,f1683]) ).
fof(f1691,plain,
( ~ hBOOL(hAPP(sF4,sF22))
| spl33_34 ),
inference(resolution,[],[f1685,f563]) ).
fof(f1782,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,[],[f41,f262]) ).
fof(f1793,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| hBOOL(hAPP(c_Message_Oparts(sF3),X0))
| hBOOL(hAPP(sF4,X0)) ),
inference(superposition,[],[f1782,f673]) ).
fof(f1797,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| hBOOL(hAPP(sF29,X0))
| hBOOL(hAPP(sF4,X0)) ),
inference(forward_demodulation,[],[f1793,f989]) ).
fof(f1815,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Message_Oparts(X0),X1))
| ~ hBOOL(hAPP(c_Message_Oanalz(X0),X1)) ),
inference(resolution,[],[f1601,f563]) ).
fof(f1842,plain,
! [X0] :
( hBOOL(hAPP(sF29,X0))
| ~ hBOOL(hAPP(c_Message_Oanalz(sF3),X0)) ),
inference(superposition,[],[f1815,f989]) ).
fof(f1851,plain,
! [X0] :
( hBOOL(hAPP(sF29,X0))
| ~ hBOOL(hAPP(sF3,X0)) ),
inference(forward_demodulation,[],[f1842,f1028]) ).
fof(f1920,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,[],[f288,f226]) ).
fof(f1947,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,[],[f1920,f682]) ).
fof(f1948,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,[],[f1947,f705]) ).
fof(f1949,plain,
! [X0] :
( hBOOL(c_in(X0,sF19,tc_Event_Oevent))
| ~ hBOOL(c_in(X0,sF27,tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f1948,f724]) ).
fof(f1951,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF27,tc_Event_Oevent))
| hBOOL(hAPP(sF19,X0)) ),
inference(resolution,[],[f1949,f564]) ).
fof(f1964,plain,
( ~ hBOOL(sF28)
| hBOOL(hAPP(sF19,sF25)) ),
inference(superposition,[],[f1951,f726]) ).
fof(f2085,plain,
! [X0] :
( hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| ~ hBOOL(hAPP(c_Message_Oparts(sF10),X0)) ),
inference(superposition,[],[f1373,f1296]) ).
fof(f2086,plain,
! [X0] :
( hBOOL(hAPP(c_Message_Oparts(sF4),X0))
| ~ hBOOL(hAPP(sF23,X0)) ),
inference(forward_demodulation,[],[f2085,f988]) ).
fof(f2089,plain,
! [X0] :
( hBOOL(hAPP(sF29,X0))
| ~ hBOOL(hAPP(sF23,X0))
| hBOOL(hAPP(sF4,X0)) ),
inference(resolution,[],[f2086,f1797]) ).
fof(f2093,plain,
( ~ hBOOL(hAPP(sF23,sF22))
| hBOOL(hAPP(sF4,sF22))
| spl33_6 ),
inference(resolution,[],[f2089,f831]) ).
fof(f2095,plain,
( hBOOL(hAPP(sF4,sF22))
| spl33_6 ),
inference(forward_subsumption_resolution,[],[f2093,f853]) ).
fof(f2096,plain,
( $false
| spl33_6
| spl33_34 ),
inference(forward_subsumption_resolution,[],[f2095,f1691]) ).
fof(f2097,plain,
( spl33_6
| spl33_34 ),
inference(avatar_contradiction_clause,[],[f2096]) ).
fof(f2104,plain,
( hBOOL(hAPP(sF19,sF25))
| ~ spl33_4 ),
inference(forward_subsumption_resolution,[],[f1964,f755]) ).
fof(f2108,plain,
( $false
| ~ spl33_4 ),
inference(forward_subsumption_resolution,[],[f2104,f827]) ).
fof(f2109,plain,
~ spl33_4,
inference(avatar_contradiction_clause,[],[f2108]) ).
fof(f2114,plain,
( hBOOL(hAPP(sF3,sF22))
| ~ spl33_35 ),
inference(resolution,[],[f1689,f564]) ).
fof(f2117,plain,
( ~ hBOOL(hAPP(sF3,sF22))
| spl33_6 ),
inference(resolution,[],[f831,f1851]) ).
fof(f2118,plain,
( $false
| spl33_6
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f2117,f2114]) ).
fof(f2119,plain,
( spl33_6
| ~ spl33_35 ),
inference(avatar_contradiction_clause,[],[f2118]) ).
fof(f2124,plain,
( hBOOL(hAPP(sF10,sF6))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f1444,f743]) ).
fof(f2125,plain,
( $false
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f2124,f839]) ).
fof(f2126,plain,
~ spl33_1,
inference(avatar_contradiction_clause,[],[f2125]) ).
cnf(s1,plain,
( spl33_1
| ~ spl33_2
| ~ spl33_3
| spl33_4 ),
inference(sat_conversion,[],[f756]) ).
cnf(s3,plain,
( spl33_3
| ~ spl33_6 ),
inference(sat_conversion,[],[f832]) ).
cnf(s17,plain,
spl33_2,
inference(sat_conversion,[],[f1203]) ).
cnf(s25,plain,
( spl33_1
| ~ spl33_34
| spl33_35 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s30,plain,
( spl33_6
| spl33_34 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s34,plain,
~ spl33_4,
inference(sat_conversion,[],[f2109]) ).
cnf(s35,plain,
( spl33_6
| ~ spl33_35 ),
inference(sat_conversion,[],[f2119]) ).
cnf(s38,plain,
~ spl33_1,
inference(sat_conversion,[],[f2126]) ).
cnf(s39,plain,
( ~ spl33_34
| spl33_35 ),
inference(rat,[],[s25,s38]) ).
cnf(s42,plain,
~ spl33_3,
inference(rat,[],[s1,s34,s17,s38]) ).
cnf(s43,plain,
~ spl33_6,
inference(rat,[],[s3,s42]) ).
cnf(s44,plain,
~ spl33_35,
inference(rat,[],[s35,s43]) ).
cnf(s45,plain,
spl33_34,
inference(rat,[],[s30,s43]) ).
cnf(s46,plain,
$false,
inference(rat,[],[s39,s44,s45]) ).
fof(f2127,plain,
$false,
inference(avatar_sat_refutation,[],[s46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV755-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n008.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 12:27:25 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.17/1.84 % (2218077)Input is clausal, will run a generic CNF schedule.
% 7.17/1.84 % (2218085)lrs+10_1_sil=8000:sp=occurrence:random_seed=2589194814:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.17/1.84 % (2218087)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3442922829:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.17/1.84 % (2218086)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3812281807:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.17/1.84 % (2218083)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2799305409:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.17/1.84 % (2218088)dis-21_1_sil=8000:lcm=predicate:random_seed=384990483: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)
% 7.17/1.84 % (2218084)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3975935261:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.17/1.84 % (2218082)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=2529972478:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.17/1.84 % (2218085)Instruction limit reached!
% 7.17/1.84 % (2218085)------------------------------
% 7.17/1.84 % (2218085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.17/1.84 % (2218085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.17/1.84 % (2218085)CaDiCaL version: 2.1.3
% 7.17/1.84 % (2218085)Termination reason: Instruction limit
% 7.17/1.84 % (2218085)Termination phase: Saturation
% 7.17/1.84 % (2218085)Time elapsed: 0.041 s
% 7.17/1.84 % (2218085)Peak memory usage: 90 MB
% 7.17/1.84 % (2218085)Instructions burned: 108 (million)
% 7.17/1.84 % (2218088)Instruction limit reached!
% 7.17/1.84 % (2218088)------------------------------
% 7.17/1.84 % (2218088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.17/1.84 % (2218088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.17/1.84 % (2218088)CaDiCaL version: 2.1.3
% 7.17/1.84 % (2218088)Termination reason: Instruction limit
% 7.17/1.84 % (2218088)Termination phase: Saturation
% 7.17/1.84 % (2218088)Time elapsed: 0.070 s
% 7.17/1.84 % (2218088)Peak memory usage: 89 MB
% 7.17/1.84 % (2218088)Instructions burned: 118 (million)
% 7.17/1.84 % (2218086)Instruction limit reached!
% 7.17/1.84 % (2218086)------------------------------
% 7.17/1.84 % (2218086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.17/1.84 % (2218086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.17/1.84 % (2218086)CaDiCaL version: 2.1.3
% 7.17/1.84 % (2218086)Termination reason: Instruction limit
% 7.17/1.84 % (2218086)Termination phase: Saturation
% 7.17/1.84 % (2218086)Time elapsed: 0.077 s
% 7.17/1.84 % (2218086)Peak memory usage: 89 MB
% 7.17/1.84 % (2218086)Instructions burned: 114 (million)
% 7.17/1.84 % (2218096)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=3905943645:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.17/1.84 % (2218087)Instruction limit reached!
% 7.17/1.84 % (2218087)------------------------------
% 7.17/1.84 % (2218087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.17/1.84 % (2218087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.17/1.84 % (2218087)CaDiCaL version: 2.1.3
% 7.17/1.84 % (2218087)Termination reason: Instruction limit
% 7.17/1.84 % (2218087)Termination phase: Saturation
% 7.17/1.84 % (2218087)Time elapsed: 0.115 s
% 7.17/1.84 % (2218087)Peak memory usage: 90 MB
% 7.17/1.84 % (2218087)Instructions burned: 180 (million)
% 7.17/1.84 % (2218096)Instruction limit reached!
% 7.17/1.84 % (2218096)------------------------------
% 7.17/1.84 % (2218096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.17/1.84 % (2218096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.17/1.84 % (2218096)CaDiCaL version: 2.1.3
% 7.17/1.84 % (2218096)Termination reason: Instruction limit
% 7.17/1.84 % (2218096)Termination phase: Saturation
% 7.17/1.84 % (2218096)Time elapsed: 0.048 s
% 7.17/1.84 % (2218096)Peak memory usage: 90 MB
% 7.17/1.84 % (2218096)Instructions burned: 144 (million)
% 7.17/1.84 % (2218097)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3831171068:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.66/2.17 % (2218098)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1116692661:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.66/2.17 % (2218101)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1478934610:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 10.66/2.17 % (2218100)lrs+10_64_to=lpo:sil=8000:random_seed=457158179:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 10.66/2.17 % (2218101)Instruction limit reached!
% 10.66/2.17 % (2218101)------------------------------
% 10.66/2.17 % (2218101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218101)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218101)Termination reason: Instruction limit
% 10.66/2.17 % (2218101)Termination phase: Saturation
% 10.66/2.17 % (2218101)Time elapsed: 0.060 s
% 10.66/2.17 % (2218101)Peak memory usage: 90 MB
% 10.66/2.17 % (2218101)Instructions burned: 196 (million)
% 10.66/2.17 % (2218097)Instruction limit reached!
% 10.66/2.17 % (2218097)------------------------------
% 10.66/2.17 % (2218097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218097)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218097)Termination reason: Instruction limit
% 10.66/2.17 % (2218097)Termination phase: Saturation
% 10.66/2.17 % (2218097)Time elapsed: 0.105 s
% 10.66/2.17 % (2218097)Peak memory usage: 91 MB
% 10.66/2.17 % (2218097)Instructions burned: 190 (million)
% 10.66/2.17 % (2218100)Instruction limit reached!
% 10.66/2.17 % (2218100)------------------------------
% 10.66/2.17 % (2218100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218100)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218100)Termination reason: Instruction limit
% 10.66/2.17 % (2218100)Termination phase: Saturation
% 10.66/2.17 % (2218100)Time elapsed: 0.078 s
% 10.66/2.17 % (2218100)Peak memory usage: 90 MB
% 10.66/2.17 % (2218100)Instructions burned: 128 (million)
% 10.66/2.17 % (2218098)Instruction limit reached!
% 10.66/2.17 % (2218098)------------------------------
% 10.66/2.17 % (2218098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218098)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218098)Termination reason: Instruction limit
% 10.66/2.17 % (2218098)Termination phase: Saturation
% 10.66/2.17 % (2218098)Time elapsed: 0.132 s
% 10.66/2.17 % (2218098)Peak memory usage: 90 MB
% 10.66/2.17 % (2218098)Instructions burned: 220 (million)
% 10.66/2.17 % (2218106)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2745634710:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 10.66/2.17 % (2218106)Instruction limit reached!
% 10.66/2.17 % (2218106)------------------------------
% 10.66/2.17 % (2218106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218106)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218106)Termination reason: Instruction limit
% 10.66/2.17 % (2218106)Termination phase: Saturation
% 10.66/2.17 % (2218106)Time elapsed: 0.057 s
% 10.66/2.17 % (2218106)Peak memory usage: 91 MB
% 10.66/2.17 % (2218106)Instructions burned: 159 (million)
% 10.66/2.17 % (2218107)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4007186493:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 10.66/2.17 % (2218108)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=3814848874:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 10.66/2.17 % (2218109)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2575168304:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 10.66/2.17 % (2218111)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3971843201:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 10.66/2.17 % (2218108)Instruction limit reached!
% 10.66/2.17 % (2218108)------------------------------
% 10.66/2.17 % (2218108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218108)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218108)Termination reason: Instruction limit
% 10.66/2.17 % (2218108)Termination phase: Saturation
% 10.66/2.17 % (2218108)Time elapsed: 0.059 s
% 10.66/2.17 % (2218108)Peak memory usage: 89 MB
% 10.66/2.17 % (2218108)Instructions burned: 106 (million)
% 10.66/2.17 % (2218109)Instruction limit reached!
% 10.66/2.17 % (2218109)------------------------------
% 10.66/2.17 % (2218109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218109)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218109)Termination reason: Instruction limit
% 10.66/2.17 % (2218109)Termination phase: Saturation
% 10.66/2.17 % (2218109)Time elapsed: 0.073 s
% 10.66/2.17 % (2218109)Peak memory usage: 90 MB
% 10.66/2.17 % (2218109)Instructions burned: 114 (million)
% 10.66/2.17 % (2218111)Instruction limit reached!
% 10.66/2.17 % (2218111)------------------------------
% 10.66/2.17 % (2218111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218111)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218111)Termination reason: Instruction limit
% 10.66/2.17 % (2218111)Termination phase: Saturation
% 10.66/2.17 % (2218111)Time elapsed: 0.082 s
% 10.66/2.17 % (2218111)Peak memory usage: 90 MB
% 10.66/2.17 % (2218111)Instructions burned: 243 (million)
% 10.66/2.17 % (2218116)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1736390608:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 10.66/2.17 % (2218117)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3582436195:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 10.66/2.17 % (2218118)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1939621044:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 10.66/2.17 % (2218117)Instruction limit reached!
% 10.66/2.17 % (2218117)------------------------------
% 10.66/2.17 % (2218117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218117)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218117)Termination reason: Instruction limit
% 10.66/2.17 % (2218117)Termination phase: Saturation
% 10.66/2.17 % (2218117)Time elapsed: 0.069 s
% 10.66/2.17 % (2218117)Peak memory usage: 89 MB
% 10.66/2.17 % (2218117)Instructions burned: 136 (million)
% 10.66/2.17 % (2218122)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3206085298:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 10.66/2.17 % (2218118)Instruction limit reached!
% 10.66/2.17 % (2218118)------------------------------
% 10.66/2.17 % (2218118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218118)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218118)Termination reason: Instruction limit
% 10.66/2.17 % (2218118)Termination phase: Saturation
% 10.66/2.17 % (2218118)Time elapsed: 0.176 s
% 10.66/2.17 % (2218118)Peak memory usage: 96 MB
% 10.66/2.17 % (2218118)Instructions burned: 502 (million)
% 10.66/2.17 % (2218124)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3485005523:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 10.66/2.17 % (2218122)Instruction limit reached!
% 10.66/2.17 % (2218122)------------------------------
% 10.66/2.17 % (2218122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218122)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218122)Termination reason: Instruction limit
% 10.66/2.17 % (2218122)Termination phase: Saturation
% 10.66/2.17 % (2218122)Time elapsed: 0.131 s
% 10.66/2.17 % (2218122)Peak memory usage: 92 MB
% 10.66/2.17 % (2218122)Instructions burned: 192 (million)
% 10.66/2.17 % (2218124)Instruction limit reached!
% 10.66/2.17 % (2218124)------------------------------
% 10.66/2.17 % (2218124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218124)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218124)Termination reason: Instruction limit
% 10.66/2.17 % (2218124)Termination phase: Saturation
% 10.66/2.17 % (2218124)Time elapsed: 0.088 s
% 10.66/2.17 % (2218124)Peak memory usage: 92 MB
% 10.66/2.17 % (2218124)Instructions burned: 264 (million)
% 10.66/2.17 % (2218084)First to succeed.
% 10.66/2.17 % (2218084)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2218077"
% 10.66/2.17 % (2218126)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=54275491:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 10.66/2.17 % (2218127)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2249908571:i=3256:kws=precedence:bd=preordered:av=off_2988 on theBenchmark for (2988ds/3256Mi)
% 10.66/2.17 % (2218126)Instruction limit reached!
% 10.66/2.17 % (2218126)------------------------------
% 10.66/2.17 % (2218126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.66/2.17 % (2218126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.66/2.17 % (2218126)CaDiCaL version: 2.1.3
% 10.66/2.17 % (2218126)Termination reason: Instruction limit
% 10.66/2.17 % (2218126)Termination phase: Saturation
% 10.66/2.17 % (2218126)Time elapsed: 0.104 s
% 10.66/2.17 % (2218126)Peak memory usage: 90 MB
% 10.66/2.17 % (2218126)Instructions burned: 156 (million)
% 10.66/2.17 % (2218082)Also succeeded, but the first one will report.
% 10.66/2.17 % (2218130)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2838461282:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 10.66/2.17 % (2218084)Refutation found. Thanks to Tanya!
% 10.66/2.17 % SZS status Unsatisfiable for theBenchmark
% 10.66/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 11.17/2.36 % (2218084)------------------------------
% 11.17/2.36 % (2218084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.17/2.36 % (2218084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.17/2.36 % (2218084)CaDiCaL version: 2.1.3
% 11.17/2.36 % (2218084)Termination reason: Refutation
% 11.17/2.36 % (2218084)Time elapsed: 1.094 s
% 11.17/2.36 % (2218084)Peak memory usage: 138 MB
% 11.17/2.36 % (2218084)Instructions burned: 1678 (million)
% 11.17/2.36 % (2218084)------------------------------
% 11.17/2.36 % (2218084)------------------------------
% 11.17/2.36 % (2218077)Success in time 1.521 s
% 11.17/2.36 % Vampire exiting
%------------------------------------------------------------------------------