%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV814-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 : n019.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:34 PM UTC 2026
% Result : Unsatisfiable 10.05s 2.07s
% Output : Refutation 10.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 26
% Syntax : Number of formulae : 83 ( 53 unt; 16 def)
% Number of atoms : 128 ( 67 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 90 ( 45 ~; 44 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-3 aty)
% Number of functors : 43 ( 43 usr; 33 con; 0-3 aty)
% Number of variables : 66 ( 0 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f622,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Says__imp__parts__knows__Spy_0) ).
fof(f632,axiom,
! [X0,X1] : c_Message_Omsg_ONonce(X0) != hAPP(c_Message_Omsg_OKey,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I30_J_0) ).
fof(f652,axiom,
! [X2,X3,X0,X1,X4,X5] :
( X0 = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3)))
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(X3,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cert__A__form_1) ).
fof(f653,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3))) = X0
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(X3,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
inference(reorient_equations,[],[f652]) ).
fof(f678,axiom,
! [X2,X3,X0,X1] :
( c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OCrypt(X2,X3)
| X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I7_J_1) ).
fof(f683,axiom,
! [X2,X3,X0,X1] :
( c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OMPair(X2,X3)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I6_J_0) ).
fof(f702,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f704,negated_conjecture,
c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f707,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f710,negated_conjecture,
v_A = v_Aa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f712,negated_conjecture,
c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) = v_X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_9) ).
fof(f713,plain,
v_X = c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),
inference(reorient_equations,[],[f712]) ).
fof(f752,plain,
~ c_in(v_Aa,c_Event_Obad,tc_Message_Oagent),
inference(definition_unfolding,[],[f702,f710]) ).
fof(f755,definition,
sF0 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f756,plain,
tc_List_Olist(tc_Event_Oevent) = sF0,
inference(reorient_equations,[],[f755]) ).
fof(f757,plain,
c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,sF0),
inference(definition_folding,[],[f704,f756]) ).
fof(f758,definition,
sF1 = hAPP(c_Public_OshrK,v_Aa),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f759,plain,
hAPP(c_Public_OshrK,v_Aa) = sF1,
inference(reorient_equations,[],[f758]) ).
fof(f760,definition,
sF2 = c_Message_Omsg_ONonce(v_NA),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f761,plain,
c_Message_Omsg_ONonce(v_NA) = sF2,
inference(reorient_equations,[],[f760]) ).
fof(f762,definition,
sF3 = c_Message_Omsg_OAgent(v_Ba),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f763,plain,
c_Message_Omsg_OAgent(v_Ba) = sF3,
inference(reorient_equations,[],[f762]) ).
fof(f764,definition,
sF4 = hAPP(c_Message_Omsg_OKey,v_Ka),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f765,plain,
hAPP(c_Message_Omsg_OKey,v_Ka) = sF4,
inference(reorient_equations,[],[f764]) ).
fof(f766,definition,
sF5 = c_Message_Omsg_OMPair(sF4,v_X),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f767,plain,
c_Message_Omsg_OMPair(sF4,v_X) = sF5,
inference(reorient_equations,[],[f766]) ).
fof(f768,definition,
sF6 = c_Message_Omsg_OMPair(sF3,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f769,plain,
c_Message_Omsg_OMPair(sF3,sF5) = sF6,
inference(reorient_equations,[],[f768]) ).
fof(f770,definition,
sF7 = c_Message_Omsg_OMPair(sF2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f771,plain,
c_Message_Omsg_OMPair(sF2,sF6) = sF7,
inference(reorient_equations,[],[f770]) ).
fof(f772,definition,
sF8 = c_Message_Omsg_OCrypt(sF1,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f773,plain,
c_Message_Omsg_OCrypt(sF1,sF7) = sF8,
inference(reorient_equations,[],[f772]) ).
fof(f774,definition,
sF9 = c_Event_Oevent_OSays(v_S,v_Aa,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f775,plain,
c_Event_Oevent_OSays(v_S,v_Aa,sF8) = sF9,
inference(reorient_equations,[],[f774]) ).
fof(f776,definition,
sF10 = c_List_Oset(v_evs3,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f777,plain,
c_List_Oset(v_evs3,tc_Event_Oevent) = sF10,
inference(reorient_equations,[],[f776]) ).
fof(f778,plain,
c_in(sF9,sF10,tc_Event_Oevent),
inference(definition_folding,[],[f707,f777,f775,f773,f771,f769,f767,f765,f763,f761,f759]) ).
fof(f790,definition,
sF16 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f791,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3) = sF16,
inference(reorient_equations,[],[f790]) ).
fof(f795,definition,
sF18 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f796,plain,
c_Message_Omsg_ONonce(v_NB) = sF18,
inference(reorient_equations,[],[f795]) ).
fof(f797,definition,
sF19 = c_Message_Omsg_OMPair(sF18,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f798,plain,
c_Message_Omsg_OMPair(sF18,sF18) = sF19,
inference(reorient_equations,[],[f797]) ).
fof(f799,definition,
sF20 = c_Message_Omsg_OCrypt(v_K,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f800,plain,
c_Message_Omsg_OCrypt(v_K,sF19) = sF20,
inference(reorient_equations,[],[f799]) ).
fof(f801,plain,
v_X = sF20,
inference(definition_folding,[],[f713,f800,f798,f796,f796]) ).
fof(f903,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3))) = X0
| c_in(X3,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF0) ),
inference(backward_demodulation,[],[f653,f756]) ).
fof(f910,plain,
sF6 = c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),sF5),
inference(forward_demodulation,[],[f769,f763]) ).
fof(f911,plain,
sF7 = c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),sF6),
inference(forward_demodulation,[],[f771,f761]) ).
fof(f914,plain,
c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)) = sF19,
inference(forward_demodulation,[],[f798,f796]) ).
fof(f915,plain,
v_X = c_Message_Omsg_OCrypt(v_K,sF19),
inference(forward_demodulation,[],[f800,f801]) ).
fof(f1012,plain,
! [X0,X1] :
( c_Message_Omsg_OCrypt(X0,X1) != v_X
| sF19 = X1 ),
inference(superposition,[],[f678,f915]) ).
fof(f1028,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_Aa))) = X3
| c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF0) ),
inference(superposition,[],[f903,f759]) ).
fof(f1037,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_Aa))) = X3
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF0) ),
inference(forward_subsumption_resolution,[],[f1028,f752]) ).
fof(f1047,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF4,X2)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa))) = X2
| ~ c_in(X3,c_NS__Shared__Mirabelle_Ons__shared,sF0) ),
inference(superposition,[],[f1037,f765]) ).
fof(f1055,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF5))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa)))
| ~ c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,sF0) ),
inference(superposition,[],[f1047,f767]) ).
fof(f1059,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF5))),c_Message_Oparts(sF16),tc_Message_Omsg)
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa)))
| ~ c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,sF0) ),
inference(superposition,[],[f1055,f791]) ).
fof(f1061,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF5))),c_Message_Oparts(sF16),tc_Message_Omsg)
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa))) ),
inference(forward_subsumption_resolution,[],[f1059,f757]) ).
fof(f1063,definition,
( spl35_5
<=> v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa))) ),
introduced(definition,[new_symbols(definition,[spl35_5])],[avatar_definition]) ).
fof(f1064,plain,
( v_X != c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa)))
| spl35_5 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1065,plain,
( v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa)))
| ~ spl35_5 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1070,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF6)),c_Message_Oparts(sF16),tc_Message_Omsg)
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa))) ),
inference(superposition,[],[f1061,f910]) ).
fof(f1121,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF10,tc_Event_Oevent)
| c_in(X2,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(superposition,[],[f622,f777]) ).
fof(f1122,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF10,tc_Event_Oevent)
| c_in(X2,c_Message_Oparts(sF16),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f1121,f791]) ).
fof(f1137,plain,
( ~ c_in(sF9,sF10,tc_Event_Oevent)
| c_in(sF8,c_Message_Oparts(sF16),tc_Message_Omsg) ),
inference(superposition,[],[f1122,f775]) ).
fof(f1141,plain,
c_in(sF8,c_Message_Oparts(sF16),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f1137,f778]) ).
fof(f1253,plain,
! [X0] : c_Message_Omsg_ONonce(X0) != sF4,
inference(superposition,[],[f632,f765]) ).
fof(f2357,plain,
( ! [X0] : ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF6)),c_Message_Oparts(sF16),tc_Message_Omsg)
| spl35_5 ),
inference(forward_subsumption_resolution,[],[f1070,f1064]) ).
fof(f2388,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF1,sF7),c_Message_Oparts(sF16),tc_Message_Omsg)
| spl35_5 ),
inference(superposition,[],[f2357,f911]) ).
fof(f2389,plain,
( ~ c_in(sF8,c_Message_Oparts(sF16),tc_Message_Omsg)
| spl35_5 ),
inference(forward_demodulation,[],[f2388,f773]) ).
fof(f2391,plain,
( $false
| spl35_5 ),
inference(forward_subsumption_resolution,[],[f2389,f1141]) ).
fof(f2392,plain,
spl35_5,
inference(avatar_contradiction_clause,[],[f2391]) ).
fof(f2412,plain,
( v_X != v_X
| sF19 = c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa))
| ~ spl35_5 ),
inference(superposition,[],[f1012,f1065]) ).
fof(f2420,plain,
( sF19 = c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(v_Aa))
| ~ spl35_5 ),
inference(trivial_inequality_removal,[],[f2412]) ).
fof(f2614,plain,
( ! [X0,X1] :
( c_Message_Omsg_OMPair(X0,X1) != sF19
| sF4 = X0 )
| ~ spl35_5 ),
inference(superposition,[],[f683,f2420]) ).
fof(f3075,plain,
( sF19 != sF19
| c_Message_Omsg_ONonce(v_NB) = sF4
| ~ spl35_5 ),
inference(superposition,[],[f2614,f914]) ).
fof(f3076,plain,
( c_Message_Omsg_ONonce(v_NB) = sF4
| ~ spl35_5 ),
inference(trivial_inequality_removal,[],[f3075]) ).
fof(f3077,plain,
( $false
| ~ spl35_5 ),
inference(forward_subsumption_resolution,[],[f3076,f1253]) ).
fof(f3078,plain,
~ spl35_5,
inference(avatar_contradiction_clause,[],[f3077]) ).
cnf(s38,plain,
spl35_5,
inference(sat_conversion,[],[f2392]) ).
cnf(s58,plain,
~ spl35_5,
inference(sat_conversion,[],[f3078]) ).
cnf(s60,plain,
$false,
inference(rat,[],[s38,s58]) ).
fof(f3084,plain,
$false,
inference(avatar_sat_refutation,[],[s60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV814-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.06/0.17 % Computer : n019.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 12:37:20 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.20 Running first-order theorem proving
% 0.06/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.16/1.88 % (3974587)Input is clausal, will run a generic CNF schedule.
% 7.16/1.88 % (3974594)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2950129123:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.16/1.88 % (3974595)lrs+10_1_sil=8000:sp=occurrence:random_seed=2913859800:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.16/1.88 % (3974593)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1397229073:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.16/1.88 % (3974597)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1446055639:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.16/1.88 % (3974592)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=1085011154:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.16/1.88 % (3974596)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=629330958:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.16/1.88 % (3974598)dis-21_1_sil=8000:lcm=predicate:random_seed=3025651574: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.16/1.88 % (3974595)Instruction limit reached!
% 7.16/1.88 % (3974595)------------------------------
% 7.16/1.88 % (3974595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.88 % (3974595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.88 % (3974595)CaDiCaL version: 2.1.3
% 7.16/1.88 % (3974595)Termination reason: Instruction limit
% 7.16/1.88 % (3974595)Termination phase: Saturation
% 7.16/1.88 % (3974595)Time elapsed: 0.070 s
% 7.16/1.88 % (3974595)Peak memory usage: 89 MB
% 7.16/1.88 % (3974595)Instructions burned: 107 (million)
% 7.16/1.88 % (3974598)Instruction limit reached!
% 7.16/1.88 % (3974598)------------------------------
% 7.16/1.88 % (3974598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.88 % (3974598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.88 % (3974598)CaDiCaL version: 2.1.3
% 7.16/1.88 % (3974598)Termination reason: Instruction limit
% 7.16/1.88 % (3974598)Termination phase: Saturation
% 7.16/1.88 % (3974598)Time elapsed: 0.070 s
% 7.16/1.88 % (3974598)Peak memory usage: 89 MB
% 7.16/1.88 % (3974598)Instructions burned: 118 (million)
% 7.16/1.88 % (3974596)Instruction limit reached!
% 7.16/1.88 % (3974596)------------------------------
% 7.16/1.88 % (3974596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.88 % (3974596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.88 % (3974596)CaDiCaL version: 2.1.3
% 7.16/1.88 % (3974596)Termination reason: Instruction limit
% 7.16/1.88 % (3974596)Termination phase: Saturation
% 7.16/1.88 % (3974596)Time elapsed: 0.071 s
% 7.16/1.88 % (3974596)Peak memory usage: 89 MB
% 7.16/1.88 % (3974596)Instructions burned: 115 (million)
% 7.16/1.88 % (3974597)Instruction limit reached!
% 7.16/1.88 % (3974597)------------------------------
% 7.16/1.88 % (3974597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.88 % (3974597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.88 % (3974597)CaDiCaL version: 2.1.3
% 7.16/1.88 % (3974597)Termination reason: Instruction limit
% 7.16/1.88 % (3974597)Termination phase: Saturation
% 7.16/1.88 % (3974597)Time elapsed: 0.118 s
% 7.16/1.88 % (3974597)Peak memory usage: 90 MB
% 7.16/1.88 % (3974597)Instructions burned: 180 (million)
% 7.16/1.88 % (3974607)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3789923016: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)
% 7.16/1.88 % (3974608)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2271577415:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.16/1.88 % (3974606)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=3862701451:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.16/1.88 % (3974609)lrs+10_64_to=lpo:sil=8000:random_seed=198289173:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.16/1.88 % (3974606)Instruction limit reached!
% 10.05/2.07 % (3974606)------------------------------
% 10.05/2.07 % (3974606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974606)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974606)Termination reason: Instruction limit
% 10.05/2.07 % (3974606)Termination phase: Saturation
% 10.05/2.07 % (3974606)Time elapsed: 0.090 s
% 10.05/2.07 % (3974606)Peak memory usage: 90 MB
% 10.05/2.07 % (3974606)Instructions burned: 144 (million)
% 10.05/2.07 % (3974607)Instruction limit reached!
% 10.05/2.07 % (3974607)------------------------------
% 10.05/2.07 % (3974607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974607)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974607)Termination reason: Instruction limit
% 10.05/2.07 % (3974607)Termination phase: Saturation
% 10.05/2.07 % (3974607)Time elapsed: 0.104 s
% 10.05/2.07 % (3974607)Peak memory usage: 91 MB
% 10.05/2.07 % (3974607)Instructions burned: 190 (million)
% 10.05/2.07 % (3974608)Instruction limit reached!
% 10.05/2.07 % (3974608)------------------------------
% 10.05/2.07 % (3974608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974608)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974608)Termination reason: Instruction limit
% 10.05/2.07 % (3974608)Termination phase: Saturation
% 10.05/2.07 % (3974608)Time elapsed: 0.121 s
% 10.05/2.07 % (3974608)Peak memory usage: 90 MB
% 10.05/2.07 % (3974608)Instructions burned: 220 (million)
% 10.05/2.07 % (3974609)Instruction limit reached!
% 10.05/2.07 % (3974609)------------------------------
% 10.05/2.07 % (3974609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974609)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974609)Termination reason: Instruction limit
% 10.05/2.07 % (3974609)Termination phase: Saturation
% 10.05/2.07 % (3974609)Time elapsed: 0.081 s
% 10.05/2.07 % (3974609)Peak memory usage: 90 MB
% 10.05/2.07 % (3974609)Instructions burned: 127 (million)
% 10.05/2.07 % (3974614)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3643416334:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 10.05/2.07 % (3974615)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1538489213:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 10.05/2.07 % (3974614)Instruction limit reached!
% 10.05/2.07 % (3974614)------------------------------
% 10.05/2.07 % (3974614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974614)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974614)Termination reason: Instruction limit
% 10.05/2.07 % (3974614)Termination phase: Saturation
% 10.05/2.07 % (3974614)Time elapsed: 0.062 s
% 10.05/2.07 % (3974614)Peak memory usage: 90 MB
% 10.05/2.07 % (3974614)Instructions burned: 195 (million)
% 10.05/2.07 % (3974616)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2604562018:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 10.05/2.07 % (3974617)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=1374154798:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 10.05/2.07 % (3974620)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1736400608:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 10.05/2.07 % (3974615)Instruction limit reached!
% 10.05/2.07 % (3974615)------------------------------
% 10.05/2.07 % (3974615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974615)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974615)Termination reason: Instruction limit
% 10.05/2.07 % (3974615)Termination phase: Saturation
% 10.05/2.07 % (3974615)Time elapsed: 0.104 s
% 10.05/2.07 % (3974615)Peak memory usage: 91 MB
% 10.05/2.07 % (3974615)Instructions burned: 157 (million)
% 10.05/2.07 % (3974617)Instruction limit reached!
% 10.05/2.07 % (3974617)------------------------------
% 10.05/2.07 % (3974617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974617)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974617)Termination reason: Instruction limit
% 10.05/2.07 % (3974617)Termination phase: Saturation
% 10.05/2.07 % (3974617)Time elapsed: 0.061 s
% 10.05/2.07 % (3974617)Peak memory usage: 89 MB
% 10.05/2.07 % (3974617)Instructions burned: 107 (million)
% 10.05/2.07 % (3974620)Instruction limit reached!
% 10.05/2.07 % (3974620)------------------------------
% 10.05/2.07 % (3974620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974620)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974620)Termination reason: Instruction limit
% 10.05/2.07 % (3974620)Termination phase: Saturation
% 10.05/2.07 % (3974620)Time elapsed: 0.038 s
% 10.05/2.07 % (3974620)Peak memory usage: 90 MB
% 10.05/2.07 % (3974620)Instructions burned: 107 (million)
% 10.05/2.07 % (3974626)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2491765463:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 10.05/2.07 % (3974624)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=983112157:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.05/2.07 % (3974625)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1501457924:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 10.05/2.07 % (3974626)Instruction limit reached!
% 10.05/2.07 % (3974626)------------------------------
% 10.05/2.07 % (3974626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974626)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974626)Termination reason: Instruction limit
% 10.05/2.07 % (3974626)Termination phase: Saturation
% 10.05/2.07 % (3974626)Time elapsed: 0.044 s
% 10.05/2.07 % (3974626)Peak memory usage: 90 MB
% 10.05/2.07 % (3974626)Instructions burned: 135 (million)
% 10.05/2.07 % (3974630)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=545422780:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 10.05/2.07 % (3974624)Instruction limit reached!
% 10.05/2.07 % (3974624)------------------------------
% 10.05/2.07 % (3974624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974624)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974624)Termination reason: Instruction limit
% 10.05/2.07 % (3974624)Termination phase: Saturation
% 10.05/2.07 % (3974624)Time elapsed: 0.148 s
% 10.05/2.07 % (3974624)Peak memory usage: 90 MB
% 10.05/2.07 % (3974624)Instructions burned: 242 (million)
% 10.05/2.07 % (3974632)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2254148856:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 10.05/2.07 % (3974630)Instruction limit reached!
% 10.05/2.07 % (3974630)------------------------------
% 10.05/2.07 % (3974630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974630)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974630)Termination reason: Instruction limit
% 10.05/2.07 % (3974630)Termination phase: Saturation
% 10.05/2.07 % (3974630)Time elapsed: 0.167 s
% 10.05/2.07 % (3974630)Peak memory usage: 96 MB
% 10.05/2.07 % (3974630)Instructions burned: 500 (million)
% 10.05/2.07 % (3974594)First to succeed.
% 10.05/2.07 % (3974594)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3974587"
% 10.05/2.07 % (3974634)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2198338137:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 10.05/2.07 % (3974632)Instruction limit reached!
% 10.05/2.07 % (3974632)------------------------------
% 10.05/2.07 % (3974632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974632)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974632)Termination reason: Instruction limit
% 10.05/2.07 % (3974632)Termination phase: Saturation
% 10.05/2.07 % (3974632)Time elapsed: 0.135 s
% 10.05/2.07 % (3974632)Peak memory usage: 91 MB
% 10.05/2.07 % (3974632)Instructions burned: 191 (million)
% 10.05/2.07 % (3974634)Instruction limit reached!
% 10.05/2.07 % (3974634)------------------------------
% 10.05/2.07 % (3974634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.07 % (3974634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.07 % (3974634)CaDiCaL version: 2.1.3
% 10.05/2.07 % (3974634)Termination reason: Instruction limit
% 10.05/2.07 % (3974634)Termination phase: Saturation
% 10.05/2.07 % (3974634)Time elapsed: 0.083 s
% 10.05/2.07 % (3974634)Peak memory usage: 92 MB
% 10.05/2.07 % (3974634)Instructions burned: 266 (million)
% 10.05/2.07 % (3974636)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1418394067:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 10.05/2.07 % (3974637)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=1268843328:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 10.05/2.07 % (3974594)Refutation found. Thanks to Tanya!
% 10.05/2.07 % SZS status Unsatisfiable for theBenchmark
% 10.05/2.07 % SZS output start Proof for theBenchmark
% See solution above
% 10.45/2.17 % (3974594)------------------------------
% 10.45/2.17 % (3974594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.17 % (3974594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.17 % (3974594)CaDiCaL version: 2.1.3
% 10.45/2.17 % (3974594)Termination reason: Refutation
% 10.45/2.17 % (3974594)Time elapsed: 1.035 s
% 10.45/2.17 % (3974594)Peak memory usage: 139 MB
% 10.45/2.17 % (3974594)Instructions burned: 1938 (million)
% 10.45/2.17 % (3974594)------------------------------
% 10.45/2.17 % (3974594)------------------------------
% 10.45/2.17 % (3974587)Success in time 1.429 s
% 10.45/2.17 % Vampire exiting
%------------------------------------------------------------------------------