%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV363-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:21:04 PM UTC 2026
% Result : Unsatisfiable 80.22s 11.70s
% Output : Refutation 80.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 20 ( 12 unt; 0 def)
% Number of atoms : 32 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 26 ( 14 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 13 con; 0-3 aty)
% Number of variables : 29 ( 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3444,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)
| c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_OMPair__analz_0) ).
fof(f3465,axiom,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oanalz__conj__parts_0) ).
fof(f3558,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-4.ax',cls_Event_OSays__imp__analz__Spy__dest_0) ).
fof(f3561,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-4.ax',cls_Yahalom_OGets__imp__analz__Spy__dest_0) ).
fof(f3586,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X5),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),X7))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(X3,c_Message_Omsg_ONonce(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Message_Omsg_ONonce(X4),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-7.ax',cls_Yahalom_Ono__nonce__YM1__YM2_0) ).
fof(f3602,negated_conjecture,
c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f3605,negated_conjecture,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f3607,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f3608,negated_conjecture,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f19837,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f3558,f3607]) ).
fof(f20138,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f19837,f3444]) ).
fof(f21258,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f20138,f3465]) ).
fof(f26880,plain,
( ~ c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolution,[],[f3561,f3605]) ).
fof(f26898,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f26880,f3602]) ).
fof(f37122,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f26898,f3444]) ).
fof(f37645,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f37122,f3465]) ).
fof(f37650,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_ONonce(v_NB)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolution,[],[f37645,f3586]) ).
fof(f37657,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_ONonce(v_NB)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f37650,f3602]) ).
fof(f37658,plain,
! [X2,X0,X1] : ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_ONonce(v_NB)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f37657,f3608]) ).
fof(f38784,plain,
$false,
inference(resolution,[],[f37658,f21258]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV363-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 % Computer : n016.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Mon Sep 28 10:48:33 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.20/0.26 Running first-order model finding
% 0.20/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.99/1.61 % (3546657)Will run a generic schedule for satisfiability detection.
% 7.99/1.61 % (3546665)dis+10_1_sil=32000:sp=arity:random_seed=2309934963:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.99/1.61 % (3546663)% WARNING: option uhcvi not known.
% 7.99/1.61 % (3546663)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1422406588:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.99/1.61 % (3546662)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3504029055_2999 on theBenchmark for (2999ds/0Mi)
% 7.99/1.61 % (3546664)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4073031547:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.99/1.61 % (3546666)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1451345332:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.99/1.61 % (3546667)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=988866222:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.99/1.61 % (3546668)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3869078865:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.99/1.61 % (3546665)Instruction limit reached!
% 7.99/1.61 % (3546665)------------------------------
% 7.99/1.61 % (3546665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.61 % (3546665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.61 % (3546665)CaDiCaL version: 2.1.3
% 7.99/1.61 % (3546665)Termination reason: Instruction limit
% 7.99/1.61 % (3546665)Termination phase: Saturation
% 7.99/1.61 % (3546665)Time elapsed: 0.035 s
% 7.99/1.61 % (3546665)Peak memory usage: 15 MB
% 7.99/1.61 % (3546665)Instructions burned: 104 (million)
% 7.99/1.61 % (3546676)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3690934738:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.99/1.61 % (3546666)Instruction limit reached!
% 7.99/1.61 % (3546666)------------------------------
% 7.99/1.61 % (3546666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.61 % (3546666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.61 % (3546666)CaDiCaL version: 2.1.3
% 7.99/1.61 % (3546666)Termination reason: Instruction limit
% 7.99/1.61 % (3546666)Termination phase: Saturation
% 7.99/1.61 % (3546666)Time elapsed: 0.063 s
% 7.99/1.61 % (3546666)Peak memory usage: 16 MB
% 7.99/1.61 % (3546666)Instructions burned: 116 (million)
% 7.99/1.61 % (3546667)Instruction limit reached!
% 7.99/1.61 % (3546667)------------------------------
% 7.99/1.61 % (3546667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.61 % (3546667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.61 % (3546667)CaDiCaL version: 2.1.3
% 7.99/1.61 % (3546667)Termination reason: Instruction limit
% 7.99/1.61 % (3546667)Termination phase: Saturation
% 7.99/1.61 % (3546667)Time elapsed: 0.075 s
% 7.99/1.61 % (3546667)Peak memory usage: 16 MB
% 7.99/1.61 % (3546667)Instructions burned: 131 (million)
% 7.99/1.61 % (3546678)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3530479497:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.99/1.61 % (3546679)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=675153426:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.99/1.61 % (3546668)Instruction limit reached!
% 7.99/1.61 % (3546668)------------------------------
% 7.99/1.61 % (3546668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.61 % (3546668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.61 % (3546668)CaDiCaL version: 2.1.3
% 7.99/1.61 % (3546668)Termination reason: Instruction limit
% 7.99/1.61 % (3546668)Termination phase: Saturation
% 7.99/1.61 % (3546668)Time elapsed: 0.101 s
% 7.99/1.61 % (3546668)Peak memory usage: 17 MB
% 7.99/1.61 % (3546668)Instructions burned: 160 (million)
% 7.99/1.61 % (3546682)ott-21_1_sil=16000:fs=off:random_seed=2184872342:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.99/1.61 % (3546678)Instruction limit reached!
% 7.99/1.61 % (3546678)------------------------------
% 7.99/1.61 % (3546678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.61 % (3546678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.61 % (3546678)CaDiCaL version: 2.1.3
% 38.78/5.86 % (3546678)Termination reason: Instruction limit
% 38.78/5.86 % (3546678)Termination phase: Saturation
% 38.78/5.86 % (3546678)Time elapsed: 0.076 s
% 38.78/5.86 % (3546678)Peak memory usage: 16 MB
% 38.78/5.86 % (3546678)Instructions burned: 131 (million)
% 38.78/5.86 % (3546684)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=208470044:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 38.78/5.86 % (3546682)Instruction limit reached!
% 38.78/5.86 % (3546682)------------------------------
% 38.78/5.86 % (3546682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/5.86 % (3546682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/5.86 % (3546682)CaDiCaL version: 2.1.3
% 38.78/5.86 % (3546682)Termination reason: Instruction limit
% 38.78/5.86 % (3546682)Termination phase: Saturation
% 38.78/5.86 % (3546682)Time elapsed: 0.091 s
% 38.78/5.86 % (3546682)Peak memory usage: 16 MB
% 38.78/5.86 % (3546682)Instructions burned: 181 (million)
% 38.78/5.86 % (3546676)Instruction limit reached!
% 38.78/5.86 % (3546676)------------------------------
% 38.78/5.86 % (3546676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/5.86 % (3546676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/5.86 % (3546676)CaDiCaL version: 2.1.3
% 38.78/5.86 % (3546676)Termination reason: Instruction limit
% 38.78/5.86 % (3546676)Termination phase: Finite model building preprocessing
% 38.78/5.86 % (3546676)Time elapsed: 0.184 s
% 38.78/5.86 % (3546676)Peak memory usage: 23 MB
% 38.78/5.86 % (3546676)Instructions burned: 720 (million)
% 38.78/5.86 % (3546686)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3335234110:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 38.78/5.86 % (3546687)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3830556057:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 38.78/5.86 % TRYING [1]
% 38.78/5.86 % TRYING [2]
% 38.78/5.86 % (3546679)Instruction limit reached!
% 38.78/5.86 % (3546679)------------------------------
% 38.78/5.86 % (3546679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/5.86 % (3546679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/5.86 % (3546679)CaDiCaL version: 2.1.3
% 38.78/5.86 % (3546679)Termination reason: Instruction limit
% 38.78/5.86 % (3546679)Termination phase: Saturation
% 38.78/5.86 % (3546679)Time elapsed: 0.358 s
% 38.78/5.86 % (3546679)Peak memory usage: 19 MB
% 38.78/5.86 % (3546679)Instructions burned: 685 (million)
% 38.78/5.86 % (3546684)Instruction limit reached!
% 38.78/5.86 % (3546684)------------------------------
% 38.78/5.86 % (3546684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/5.86 % (3546684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/5.86 % (3546684)CaDiCaL version: 2.1.3
% 38.78/5.86 % (3546684)Termination reason: Instruction limit
% 38.78/5.86 % (3546684)Termination phase: Saturation
% 38.78/5.86 % (3546684)Time elapsed: 0.292 s
% 38.78/5.86 % (3546684)Peak memory usage: 17 MB
% 38.78/5.86 % (3546684)Instructions burned: 478 (million)
% 38.78/5.86 % (3546690)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1910209933:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 38.78/5.86 % (3546692)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2421980442:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 38.78/5.86 % TRYING [1]
% 38.78/5.86 % (3546687)Instruction limit reached!
% 38.78/5.86 % (3546687)------------------------------
% 38.78/5.86 % (3546687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/5.86 % (3546687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/5.86 % (3546687)CaDiCaL version: 2.1.3
% 38.78/5.86 % (3546687)Termination reason: Instruction limit
% 38.78/5.86 % (3546687)Termination phase: Saturation
% 38.78/5.86 % (3546687)Time elapsed: 0.395 s
% 38.78/5.86 % (3546687)Peak memory usage: 29 MB
% 38.78/5.86 % (3546687)Instructions burned: 1181 (million)
% 38.78/5.86 % (3546694)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=926890448:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 38.78/5.86 % (3546686)Instruction limit reached!
% 38.78/5.86 % (3546686)------------------------------
% 38.78/5.86 % (3546686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/5.86 % (3546686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.60/9.37 % (3546686)CaDiCaL version: 2.1.3
% 63.60/9.37 % (3546686)Termination reason: Instruction limit
% 63.60/9.37 % (3546686)Termination phase: Finite model building constraint generation
% 63.60/9.37 % (3546686)Time elapsed: 0.422 s
% 63.60/9.37 % (3546686)Peak memory usage: 30 MB
% 63.60/9.37 % (3546686)Instructions burned: 865 (million)
% 63.60/9.37 % (3546696)fmb+10_1_sil=64000:random_seed=3437747220:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 63.60/9.37 % (3546690)Cannot represent all propositional literals internally
% 63.60/9.37 % (3546690)Refutation not found, incomplete strategy
% 63.60/9.37 % (3546690)------------------------------
% 63.60/9.37 % (3546690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.60/9.37 % (3546690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.60/9.37 % (3546690)CaDiCaL version: 2.1.3
% 63.60/9.37 % (3546690)Termination reason: Refutation not found, incomplete strategy
% 63.60/9.37 % (3546690)Time elapsed: 0.345 s
% 63.60/9.37 % (3546690)Peak memory usage: 26 MB
% 63.60/9.37 % (3546690)Instructions burned: 697 (million)
% 63.60/9.37 % (3546690)------------------------------
% 63.60/9.37 % (3546690)------------------------------
% 63.60/9.37 % (3546698)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3989433720:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 63.60/9.37 % (3546694)Instruction limit reached!
% 63.60/9.37 % (3546694)------------------------------
% 63.60/9.37 % (3546694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.60/9.37 % (3546694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.60/9.37 % (3546694)CaDiCaL version: 2.1.3
% 63.60/9.37 % (3546694)Termination reason: Instruction limit
% 63.60/9.37 % (3546694)Termination phase: Saturation
% 63.60/9.37 % (3546694)Time elapsed: 0.231 s
% 63.60/9.37 % (3546694)Peak memory usage: 21 MB
% 63.60/9.37 % (3546694)Instructions burned: 883 (million)
% 63.60/9.37 % (3546700)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1858465139:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 63.60/9.37 % (3546692)Instruction limit reached!
% 63.60/9.37 % (3546692)------------------------------
% 63.60/9.37 % (3546692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.60/9.37 % (3546692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.60/9.37 % (3546692)CaDiCaL version: 2.1.3
% 63.60/9.37 % (3546692)Termination reason: Instruction limit
% 63.60/9.37 % (3546692)Termination phase: Saturation
% 63.60/9.37 % (3546692)Time elapsed: 0.406 s
% 63.60/9.37 % (3546692)Peak memory usage: 22 MB
% 63.60/9.37 % (3546692)Instructions burned: 693 (million)
% 63.60/9.37 % (3546702)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3898470871:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 63.60/9.37 % TRYING [1]
% 63.60/9.37 % (3546700)Cannot represent all propositional literals internally
% 63.60/9.37 % (3546700)Refutation not found, incomplete strategy
% 63.60/9.37 % (3546700)------------------------------
% 63.60/9.37 % (3546700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.60/9.37 % (3546700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.60/9.37 % (3546700)CaDiCaL version: 2.1.3
% 63.60/9.37 % (3546700)Termination reason: Refutation not found, incomplete strategy
% 63.60/9.37 % (3546700)Time elapsed: 0.184 s
% 63.60/9.37 % (3546700)Peak memory usage: 25 MB
% 63.60/9.37 % (3546700)Instructions burned: 693 (million)
% 63.60/9.37 % (3546700)------------------------------
% 63.60/9.37 % (3546700)------------------------------
% 63.60/9.37 % (3546704)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1426213296:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 63.60/9.37 % (3546698)Cannot represent all propositional literals internally
% 63.60/9.37 % (3546698)Refutation not found, incomplete strategy
% 63.60/9.37 % (3546698)------------------------------
% 63.60/9.37 % (3546698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.60/9.37 % (3546698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.60/9.37 % (3546698)CaDiCaL version: 2.1.3
% 63.60/9.37 % (3546698)Termination reason: Refutation not found, incomplete strategy
% 63.60/9.37 % (3546698)Time elapsed: 0.348 s
% 63.60/9.37 % (3546698)Peak memory usage: 25 MB
% 63.60/9.37 % (3546698)Instructions burned: 693 (million)
% 63.60/9.37 % (3546698)------------------------------
% 63.60/9.37 % (3546698)------------------------------
% 63.60/9.37 % (3546706)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3814620298:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 70.68/10.33 % TRYING [2]
% 70.68/10.33 % (3546704)Instruction limit reached!
% 70.68/10.33 % (3546704)------------------------------
% 70.68/10.33 % (3546704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.68/10.33 % (3546704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.33 % (3546704)CaDiCaL version: 2.1.3
% 70.68/10.33 % (3546704)Termination reason: Instruction limit
% 70.68/10.33 % (3546704)Termination phase: Saturation
% 70.68/10.33 % (3546704)Time elapsed: 0.476 s
% 70.68/10.33 % (3546704)Peak memory usage: 35 MB
% 70.68/10.33 % (3546704)Instructions burned: 1472 (million)
% 70.68/10.33 % (3546708)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2774725364:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi)
% 70.68/10.33 % (3546706)Cannot represent all propositional literals internally
% 70.68/10.33 % (3546706)Refutation not found, incomplete strategy
% 70.68/10.33 % (3546706)------------------------------
% 70.68/10.33 % (3546706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.68/10.33 % (3546706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.33 % (3546706)CaDiCaL version: 2.1.3
% 70.68/10.33 % (3546706)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.33 % (3546706)Time elapsed: 0.360 s
% 70.68/10.33 % (3546706)Peak memory usage: 26 MB
% 70.68/10.33 % (3546706)Instructions burned: 715 (million)
% 70.68/10.33 % (3546706)------------------------------
% 70.68/10.33 % (3546706)------------------------------
% 70.68/10.33 % (3546710)ott-2_1_sil=16000:newcnf=on:random_seed=3677483887:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi)
% 70.68/10.33 % (3546710)Instruction limit reached!
% 70.68/10.33 % (3546710)------------------------------
% 70.68/10.33 % (3546710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.68/10.33 % (3546710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.33 % (3546710)CaDiCaL version: 2.1.3
% 70.68/10.33 % (3546710)Termination reason: Instruction limit
% 70.68/10.33 % (3546710)Termination phase: Saturation
% 70.68/10.33 % (3546710)Time elapsed: 0.446 s
% 70.68/10.33 % (3546710)Peak memory usage: 18 MB
% 70.68/10.33 % (3546710)Instructions burned: 869 (million)
% 70.68/10.33 % (3546712)ott+10_1_sil=32000:tgt=ground:random_seed=687188290:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi)
% 70.68/10.33 % (3546708)Instruction limit reached!
% 70.68/10.33 % (3546708)------------------------------
% 70.68/10.33 % (3546708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.68/10.33 % (3546708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.33 % (3546708)CaDiCaL version: 2.1.3
% 70.68/10.33 % (3546708)Termination reason: Instruction limit
% 70.68/10.33 % (3546708)Termination phase: Finite model building preprocessing
% 70.68/10.33 % (3546708)Time elapsed: 0.580 s
% 70.68/10.33 % (3546708)Peak memory usage: 42 MB
% 70.68/10.33 % (3546708)Instructions burned: 2176 (million)
% 70.68/10.33 % (3546714)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2517942258:i=54282_2977 on theBenchmark for (2977ds/54282Mi)
% 70.68/10.33 % TRYING [1]
% 70.68/10.33 % TRYING [2]
% 70.68/10.33 % (3546702)Instruction limit reached!
% 70.68/10.33 % (3546702)------------------------------
% 70.68/10.33 % (3546702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.68/10.33 % (3546702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.33 % (3546702)CaDiCaL version: 2.1.3
% 70.68/10.33 % (3546702)Termination reason: Instruction limit
% 70.68/10.33 % (3546702)Termination phase: Saturation
% 70.68/10.33 % (3546702)Time elapsed: 3.217 s
% 70.68/10.33 % (3546702)Peak memory usage: 52 MB
% 70.68/10.33 % (3546702)Instructions burned: 5131 (million)
% 70.68/10.33 % (3546716)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1821922628:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 70.68/10.33 % (3546712)Instruction limit reached!
% 70.68/10.33 % (3546712)------------------------------
% 70.68/10.33 % (3546712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.68/10.33 % (3546712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.33 % (3546712)CaDiCaL version: 2.1.3
% 70.68/10.33 % (3546712)Termination reason: Instruction limit
% 70.68/10.33 % (3546712)Termination phase: Saturation
% 70.68/10.33 % (3546712)Time elapsed: 3.397 s
% 70.68/10.33 % (3546712)Peak memory usage: 69 MB
% 70.68/10.33 % (3546712)Instructions burned: 5114 (million)
% 41.53/11.69 % (3546718)dis+21_1_sil=32000:sas=cadical:random_seed=3256521482:i=3773:amm=off_2944 on theBenchmark for (2944ds/3773Mi)
% 41.53/11.69 % (3546716)Instruction limit reached!
% 41.53/11.69 % (3546716)------------------------------
% 41.53/11.69 % (3546716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.69 % (3546716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.69 % (3546716)CaDiCaL version: 2.1.3
% 41.53/11.69 % (3546716)Termination reason: Instruction limit
% 41.53/11.69 % (3546716)Termination phase: Saturation
% 41.53/11.69 % (3546716)Time elapsed: 2.239 s
% 41.53/11.69 % (3546716)Peak memory usage: 47 MB
% 41.53/11.69 % (3546716)Instructions burned: 3513 (million)
% 41.53/11.69 % (3546720)ott+11_1_sil=16000:gs=on:random_seed=2089285471:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 41.53/11.69 % (3546714)Cannot represent all propositional literals internally
% 41.53/11.69 % (3546714)Refutation not found, incomplete strategy
% 41.53/11.69 % (3546714)------------------------------
% 41.53/11.69 % (3546714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.69 % (3546714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.69 % (3546714)CaDiCaL version: 2.1.3
% 41.53/11.69 % (3546714)Termination reason: Refutation not found, incomplete strategy
% 41.53/11.69 % (3546714)Time elapsed: 5.498 s
% 41.53/11.69 % (3546714)Peak memory usage: 983 MB
% 41.53/11.69 % (3546714)Instructions burned: 14876 (million)
% 41.53/11.69 % (3546714)------------------------------
% 41.53/11.69 % (3546714)------------------------------
% 41.53/11.69 % (3546722)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1794200591:fmbsr=1.6:i=67534_2921 on theBenchmark for (2921ds/67534Mi)
% 41.53/11.69 % (3546718)Instruction limit reached!
% 41.53/11.69 % (3546718)------------------------------
% 41.53/11.69 % (3546718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.69 % (3546718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.69 % (3546718)CaDiCaL version: 2.1.3
% 41.53/11.69 % (3546718)Termination reason: Instruction limit
% 41.53/11.69 % (3546718)Termination phase: Saturation
% 41.53/11.69 % (3546718)Time elapsed: 2.276 s
% 41.53/11.69 % (3546718)Peak memory usage: 39 MB
% 41.53/11.69 % (3546718)Instructions burned: 3774 (million)
% 41.53/11.69 % (3546724)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3510198831:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2921 on theBenchmark for (2921ds/4591Mi)
% 41.53/11.69 % (3546720)Instruction limit reached!
% 41.53/11.69 % (3546720)------------------------------
% 41.53/11.69 % (3546720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.69 % (3546720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.69 % (3546720)CaDiCaL version: 2.1.3
% 41.53/11.69 % (3546720)Termination reason: Instruction limit
% 41.53/11.69 % (3546720)Termination phase: Saturation
% 41.53/11.69 % (3546720)Time elapsed: 1.478 s
% 41.53/11.69 % (3546720)Peak memory usage: 81 MB
% 41.53/11.69 % (3546720)Instructions burned: 2251 (million)
% 41.53/11.69 % (3546726)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3213684833:i=29340_2919 on theBenchmark for (2919ds/29340Mi)
% 41.53/11.69 % (3546722)Cannot represent all propositional literals internally
% 41.53/11.69 % (3546722)Refutation not found, incomplete strategy
% 41.53/11.69 % (3546722)------------------------------
% 41.53/11.69 % (3546722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.69 % (3546722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.69 % (3546722)CaDiCaL version: 2.1.3
% 41.53/11.69 % (3546722)Termination reason: Refutation not found, incomplete strategy
% 41.53/11.69 % (3546722)Time elapsed: 0.193 s
% 41.53/11.69 % (3546722)Peak memory usage: 24 MB
% 41.53/11.69 % (3546722)Instructions burned: 724 (million)
% 41.53/11.69 % (3546722)------------------------------
% 41.53/11.69 % (3546722)------------------------------
% 41.53/11.69 % (3546728)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=77162246:i=5211_2919 on theBenchmark for (2919ds/5211Mi)
% 41.53/11.69 % (3546662)Cannot represent all propositional literals internally
% 41.53/11.69 % (3546662)Refutation not found, incomplete strategy
% 41.53/11.69 % (3546662)------------------------------
% 41.53/11.69 % (3546662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.69 % (3546662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.70 % (3546662)CaDiCaL version: 2.1.3
% 41.53/11.70 % (3546662)Termination reason: Refutation not found, incomplete strategy
% 41.53/11.70 % (3546662)Time elapsed: 8.989 s
% 41.53/11.70 % (3546662)Peak memory usage: 983 MB
% 41.53/11.70 % (3546662)Instructions burned: 14876 (million)
% 41.53/11.70 % (3546662)------------------------------
% 41.53/11.70 % (3546662)------------------------------
% 41.53/11.70 % (3546730)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1270187124:i=5497:nm=2_2907 on theBenchmark for (2907ds/5497Mi)
% 41.53/11.70 % (3546728)Instruction limit reached!
% 41.53/11.70 % (3546728)------------------------------
% 41.53/11.70 % (3546728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.70 % (3546728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.70 % (3546728)CaDiCaL version: 2.1.3
% 41.53/11.70 % (3546728)Termination reason: Instruction limit
% 41.53/11.70 % (3546728)Termination phase: Saturation
% 41.53/11.70 % (3546728)Time elapsed: 1.379 s
% 41.53/11.70 % (3546728)Peak memory usage: 43 MB
% 41.53/11.70 % (3546728)Instructions burned: 5212 (million)
% 41.53/11.70 % (3546732)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2937109516:fmbsr=2:i=46332_2905 on theBenchmark for (2905ds/46332Mi)
% 41.53/11.70 % (3546730)Cannot represent all propositional literals internally
% 41.53/11.70 % (3546730)Refutation not found, incomplete strategy
% 41.53/11.70 % (3546730)------------------------------
% 41.53/11.70 % (3546730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.70 % (3546730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.70 % (3546730)CaDiCaL version: 2.1.3
% 41.53/11.70 % (3546730)Termination reason: Refutation not found, incomplete strategy
% 41.53/11.70 % (3546730)Time elapsed: 0.365 s
% 41.53/11.70 % (3546730)Peak memory usage: 26 MB
% 41.53/11.70 % (3546730)Instructions burned: 715 (million)
% 41.53/11.70 % (3546730)------------------------------
% 41.53/11.70 % (3546730)------------------------------
% 41.53/11.70 % (3546734)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=143116450:i=14071_2903 on theBenchmark for (2903ds/14071Mi)
% 41.53/11.70 % (3546732)Cannot represent all propositional literals internally
% 41.53/11.70 % (3546732)Refutation not found, incomplete strategy
% 41.53/11.70 % (3546732)------------------------------
% 41.53/11.70 % (3546732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.70 % (3546732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.70 % (3546732)CaDiCaL version: 2.1.3
% 41.53/11.70 % (3546732)Termination reason: Refutation not found, incomplete strategy
% 41.53/11.70 % (3546732)Time elapsed: 0.191 s
% 41.53/11.70 % (3546732)Peak memory usage: 24 MB
% 41.53/11.70 % (3546732)Instructions burned: 724 (million)
% 41.53/11.70 % (3546732)------------------------------
% 41.53/11.70 % (3546732)------------------------------
% 41.53/11.70 % (3546736)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1675249600:i=22565:add=on:rawr=on_2903 on theBenchmark for (2903ds/22565Mi)
% 41.53/11.70 % (3546734)Cannot represent all propositional literals internally
% 41.53/11.70 % (3546734)Refutation not found, incomplete strategy
% 41.53/11.70 % (3546734)------------------------------
% 41.53/11.70 % (3546734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.70 % (3546734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.70 % (3546734)CaDiCaL version: 2.1.3
% 41.53/11.70 % (3546734)Termination reason: Refutation not found, incomplete strategy
% 41.53/11.70 % (3546734)Time elapsed: 0.353 s
% 41.53/11.70 % (3546734)Peak memory usage: 25 MB
% 41.53/11.70 % (3546734)Instructions burned: 694 (million)
% 41.53/11.70 % (3546734)------------------------------
% 41.53/11.70 % (3546734)------------------------------
% 41.53/11.70 % (3546738)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2997388586:i=8173:av=off_2900 on theBenchmark for (2900ds/8173Mi)
% 41.53/11.70 % (3546724)Instruction limit reached!
% 41.53/11.70 % (3546724)------------------------------
% 41.53/11.70 % (3546724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.53/11.70 % (3546724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.53/11.70 % (3546724)CaDiCaL version: 2.1.3
% 41.53/11.70 % (3546724)Termination reason: Instruction limit
% 41.53/11.70 % (3546724)Termination phase: Saturation
% 41.53/11.70 % (3546724)Time elapsed: 2.139 s
% 41.53/11.70 % (3546724)Peak memory usage: 44 MB
% 41.53/11.70 % (3546724)Instructions burned: 4594 (million)
% 80.22/11.70 % (3546740)dis+10_16:1_sil=16000:random_seed=4070896362:i=9155:fsr=off_2899 on theBenchmark for (2899ds/9155Mi)
% 80.22/11.70 % (3546738) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3546657-3546738"...
% 80.22/11.70 % (3546738)...printing done.
% 80.22/11.70 % (3546738)Refutation found. Thanks to Tanya!
% 80.22/11.70 % SZS status Unsatisfiable for theBenchmark
% 80.22/11.70 % SZS output start Proof for theBenchmark
% See solution above
% 80.22/11.70 % (3546738)------------------------------
% 80.22/11.70 % (3546738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.22/11.70 % (3546738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.22/11.70 % (3546738)CaDiCaL version: 2.1.3
% 80.22/11.70 % (3546738)Termination reason: Refutation
% 80.22/11.70 % (3546738)Time elapsed: 1.301 s
% 80.22/11.70 % (3546738)Peak memory usage: 39 MB
% 80.22/11.70 % (3546738)Instructions burned: 1925 (million)
% 80.22/11.70 % (3546657)Success in time 11.417 s
% 80.22/11.70 % Vampire exiting
%------------------------------------------------------------------------------