%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV017+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:07:55 PM UTC 2026
% Result : Satisfiable 0.35s 6.51s
% Output : Saturation 0.35s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u107,axiom,
party_of_protocol(a) ).
cnf(u112,axiom,
party_of_protocol(b) ).
cnf(u117,axiom,
fresh_to_b(an_a_nonce) ).
cnf(u122,axiom,
party_of_protocol(t) ).
cnf(u127,axiom,
a_nonce(an_a_nonce) ).
cnf(u132,axiom,
fresh_intruder_nonce(an_intruder_nonce) ).
cnf(u136,axiom,
~ a_nonce(generate_key(X0)) ).
cnf(u140,axiom,
a_nonce(generate_b_nonce(X0)) ).
cnf(u144,axiom,
a_nonce(generate_expiration_time(X0)) ).
cnf(u148,axiom,
a_key(generate_key(X0)) ).
cnf(u153,axiom,
a_stored(pair(b,an_a_nonce)) ).
cnf(u158,axiom,
t_holds(key(at,a)) ).
cnf(u163,axiom,
t_holds(key(bt,b)) ).
cnf(u167,axiom,
( ~ a_key(X0)
| ~ a_nonce(X0) ) ).
cnf(u171,axiom,
( intruder_message(X0)
| ~ fresh_intruder_nonce(X0) ) ).
cnf(u175,axiom,
( fresh_to_b(X0)
| ~ fresh_intruder_nonce(X0) ) ).
cnf(u180,axiom,
( fresh_intruder_nonce(generate_intruder_nonce(X0))
| ~ fresh_intruder_nonce(X0) ) ).
cnf(u184,axiom,
( intruder_message(X1)
| ~ intruder_message(pair(X0,X1)) ) ).
cnf(u188,axiom,
( intruder_message(X0)
| ~ intruder_message(pair(X0,X1)) ) ).
cnf(u193,axiom,
message(sent(a,b,pair(a,an_a_nonce))) ).
cnf(u197,axiom,
( intruder_message(X2)
| ~ message(sent(X0,X1,X2)) ) ).
cnf(u201,axiom,
( intruder_message(X2)
| ~ intruder_message(triple(X0,X1,X2)) ) ).
cnf(u205,axiom,
( intruder_message(X1)
| ~ intruder_message(triple(X0,X1,X2)) ) ).
cnf(u209,axiom,
( intruder_message(X0)
| ~ intruder_message(triple(X0,X1,X2)) ) ).
cnf(u213,axiom,
( intruder_message(X3)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ) ).
cnf(u217,axiom,
( intruder_message(X2)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ) ).
cnf(u221,axiom,
( intruder_message(X1)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ) ).
cnf(u225,axiom,
( intruder_message(X0)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ) ).
cnf(u229,axiom,
( intruder_message(pair(X0,X1))
| ~ intruder_message(X0)
| ~ intruder_message(X1) ) ).
cnf(u233,axiom,
( intruder_holds(key(X0,X1))
| ~ intruder_message(X0)
| ~ party_of_protocol(X1) ) ).
cnf(u237,axiom,
( intruder_message(triple(X0,X1,X2))
| ~ intruder_message(X0)
| ~ intruder_message(X1)
| ~ intruder_message(X2) ) ).
cnf(u241,axiom,
( message(sent(X1,X2,X0))
| ~ intruder_message(X0)
| ~ party_of_protocol(X1)
| ~ party_of_protocol(X2) ) ).
cnf(u245,axiom,
( intruder_message(X1)
| ~ intruder_message(encrypt(X0,X1))
| ~ intruder_holds(key(X1,X2))
| ~ party_of_protocol(X2) ) ).
cnf(u249,axiom,
( intruder_message(encrypt(X0,X1))
| ~ intruder_message(X0)
| ~ intruder_holds(key(X1,X2))
| ~ party_of_protocol(X2) ) ).
cnf(u253,axiom,
( intruder_message(quadruple(X0,X1,X2,X3))
| ~ intruder_message(X0)
| ~ intruder_message(X1)
| ~ intruder_message(X2)
| ~ intruder_message(X3) ) ).
cnf(u257,axiom,
( message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt))))
| ~ message(sent(X0,b,pair(X0,X1)))
| ~ fresh_to_b(X1) ) ).
cnf(u261,axiom,
( message(sent(a,X4,pair(X3,encrypt(X0,X2))))
| ~ message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0)))
| ~ a_stored(pair(X4,X5)) ) ).
cnf(u265,axiom,
( message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1)))
| ~ message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5))))
| ~ t_holds(key(X5,X0))
| ~ t_holds(key(X6,X2))
| ~ a_nonce(X3) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV017+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.30 % Computer : n026.cluster.edu
% 0.13/0.30 % Model : x86_64 x86_64
% 0.13/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.30 % Memory : 8046.5625MB
% 0.13/0.30 % OS : Linux 6.8.0-71-generic
% 0.13/0.30 % CPULimit : 300
% 0.13/0.30 % WCLimit : 300
% 0.13/0.30 % DateTime : Mon Sep 28 09:45:17 UTC 2026
% 0.31/0.31 % CPUTime :
% 0.31/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.31/0.36 Running first-order theorem proving
% 0.31/0.36 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
% 16.79/3.56 % (3734385)Detected formulas, will run a generic FOF schedule.
% 16.79/3.56 % (3734394)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1846281801:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 16.79/3.56 % (3734394)Refutation not found, incomplete strategy
% 16.79/3.56 % (3734394)------------------------------
% 16.79/3.56 % (3734394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.79/3.56 % (3734394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/3.56 % (3734394)CaDiCaL version: 2.1.3
% 16.79/3.56 % (3734394)Termination reason: Refutation not found, incomplete strategy
% 16.79/3.56 % (3734394)Time elapsed: 0.0000 s
% 16.79/3.56 % (3734394)Peak memory usage: 86 MB
% 16.79/3.56 % (3734391)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3771127503:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 16.79/3.56 % (3734390)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=1739299526:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 16.79/3.56 % (3734392)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1564484022:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 16.79/3.56 % (3734393)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=852738466:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 16.79/3.56 % (3734393)Refutation not found, incomplete strategy
% 16.79/3.56 % (3734393)------------------------------
% 16.79/3.56 % (3734393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.79/3.56 % (3734393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/3.56 % (3734393)CaDiCaL version: 2.1.3
% 16.79/3.56 % (3734393)Termination reason: Refutation not found, incomplete strategy
% 16.79/3.56 % (3734393)Time elapsed: 0.001 s
% 16.79/3.56 % (3734393)Peak memory usage: 86 MB
% 16.79/3.56 % (3734396)dis-21_1_sil=8000:lcm=predicate:random_seed=599459964:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 16.79/3.56 % (3734395)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=384950973:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 16.79/3.56 % (3734395)Refutation not found, incomplete strategy
% 16.79/3.56 % (3734395)------------------------------
% 16.79/3.56 % (3734395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.79/3.56 % (3734395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/3.56 % (3734395)CaDiCaL version: 2.1.3
% 16.79/3.56 % (3734395)Termination reason: Refutation not found, incomplete strategy
% 16.79/3.56 % (3734395)Time elapsed: 0.003 s
% 16.79/3.56 % (3734395)Peak memory usage: 88 MB
% 16.79/3.56 % (3734395)Instructions burned: 2 (million)
% 16.79/3.56 % (3734396)Instruction limit reached!
% 16.79/3.56 % (3734396)------------------------------
% 16.79/3.56 % (3734396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.79/3.56 % (3734396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/3.56 % (3734396)CaDiCaL version: 2.1.3
% 16.79/3.56 % (3734396)Termination reason: Instruction limit
% 16.79/3.56 % (3734396)Termination phase: Saturation
% 16.79/3.56 % (3734396)Time elapsed: 0.109 s
% 16.79/3.56 % (3734396)Peak memory usage: 89 MB
% 16.79/3.56 % (3734396)Instructions burned: 130 (million)
% 16.79/3.56 % (3734394)------------------------------
% 16.79/3.56 % (3734394)------------------------------
% 16.79/3.56 % (3734405)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1642992091:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 16.79/3.56 % (3734405)Refutation not found, incomplete strategy
% 16.79/3.56 % (3734405)------------------------------
% 16.79/3.56 % (3734405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.79/3.56 % (3734405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/3.56 % (3734405)CaDiCaL version: 2.1.3
% 16.79/3.56 % (3734405)Termination reason: Refutation not found, incomplete strategy
% 16.79/3.56 % (3734405)Time elapsed: 0.001 s
% 16.79/3.56 % (3734405)Peak memory usage: 87 MB
% 16.79/3.56 % (3734404)lrs+10_1_sil=8000:sp=occurrence:random_seed=2494315054:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 17.60/3.65 % (3734404)Refutation not found, incomplete strategy
% 17.60/3.65 % (3734404)------------------------------
% 17.60/3.65 % (3734404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.65 % (3734404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.65 % (3734404)CaDiCaL version: 2.1.3
% 17.60/3.65 % (3734404)Termination reason: Refutation not found, incomplete strategy
% 17.60/3.65 % (3734404)Time elapsed: 0.001 s
% 17.60/3.65 % (3734404)Peak memory usage: 86 MB
% 17.60/3.65 % (3734393)------------------------------
% 17.60/3.65 % (3734393)------------------------------
% 17.60/3.65 % (3734395)------------------------------
% 17.60/3.65 % (3734395)------------------------------
% 17.60/3.65 % (3734405)------------------------------
% 17.60/3.65 % (3734405)------------------------------
% 17.60/3.65 % (3734408)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2341316527:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 17.60/3.65 % (3734408)Refutation not found, incomplete strategy
% 17.60/3.65 % (3734408)------------------------------
% 17.60/3.65 % (3734408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.65 % (3734408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.65 % (3734408)CaDiCaL version: 2.1.3
% 17.60/3.65 % (3734408)Termination reason: Refutation not found, incomplete strategy
% 17.60/3.65 % (3734408)Time elapsed: 0.001 s
% 17.60/3.65 % (3734408)Peak memory usage: 86 MB
% 17.60/3.65 % (3734409)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=299648544:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 17.60/3.65 % (3734404)------------------------------
% 17.60/3.65 % (3734404)------------------------------
% 17.60/3.65 % (3734410)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3234076849:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 17.60/3.65 % (3734410)Refutation not found, incomplete strategy
% 17.60/3.65 % (3734410)------------------------------
% 17.60/3.65 % (3734410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.65 % (3734410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.65 % (3734410)CaDiCaL version: 2.1.3
% 17.60/3.65 % (3734410)Termination reason: Refutation not found, incomplete strategy
% 17.60/3.65 % (3734410)Time elapsed: 0.001 s
% 17.60/3.65 % (3734410)Peak memory usage: 86 MB
% 17.60/3.65 % (3734392)Refutation not found, incomplete strategy
% 17.60/3.65 % (3734392)------------------------------
% 17.60/3.65 % (3734392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.65 % (3734392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.65 % (3734392)CaDiCaL version: 2.1.3
% 17.60/3.65 % (3734392)Termination reason: Refutation not found, incomplete strategy
% 17.60/3.65 % (3734392)Time elapsed: 0.885 s
% 17.60/3.65 % (3734392)Peak memory usage: 127 MB
% 17.60/3.65 % (3734392)Instructions burned: 834 (million)
% 17.60/3.65 % (3734409)Instruction limit reached!
% 17.60/3.65 % (3734409)------------------------------
% 17.60/3.65 % (3734409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.65 % (3734409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.65 % (3734409)CaDiCaL version: 2.1.3
% 17.60/3.65 % (3734409)Termination reason: Instruction limit
% 17.60/3.65 % (3734409)Termination phase: Saturation
% 17.60/3.65 % (3734409)Time elapsed: 0.202 s
% 17.60/3.65 % (3734409)Peak memory usage: 96 MB
% 17.60/3.65 % (3734409)Instructions burned: 249 (million)
% 17.60/3.65 % (3734413)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2281356921:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 17.60/3.65 % (3734408)------------------------------
% 17.60/3.65 % (3734408)------------------------------
% 17.60/3.65 % (3734392)------------------------------
% 17.60/3.65 % (3734392)------------------------------
% 17.60/3.65 % (3734415)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3833408436:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 17.60/3.65 % (3734415)Refutation not found, incomplete strategy
% 17.60/3.65 % (3734415)------------------------------
% 17.60/3.65 % (3734415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.65 % (3734415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/4.16 % (3734415)CaDiCaL version: 2.1.3
% 22.24/4.16 % (3734415)Termination reason: Refutation not found, incomplete strategy
% 22.24/4.16 % (3734415)Time elapsed: 0.002 s
% 22.24/4.16 % (3734415)Peak memory usage: 87 MB
% 22.24/4.16 % (3734415)Instructions burned: 1 (million)
% 22.24/4.16 % (3734410)------------------------------
% 22.24/4.16 % (3734410)------------------------------
% 22.24/4.16 % (3734417)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1591617225:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 22.24/4.16 % (3734417)Refutation not found, incomplete strategy
% 22.24/4.16 % (3734417)------------------------------
% 22.24/4.16 % (3734417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/4.16 % (3734417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/4.16 % (3734417)CaDiCaL version: 2.1.3
% 22.24/4.16 % (3734417)Termination reason: Refutation not found, incomplete strategy
% 22.24/4.16 % (3734417)Time elapsed: 0.003 s
% 22.24/4.16 % (3734417)Peak memory usage: 87 MB
% 22.24/4.16 % (3734417)Instructions burned: 2 (million)
% 22.24/4.16 % (3734418)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=87248976:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 22.24/4.16 % (3734418)Refutation not found, incomplete strategy
% 22.24/4.16 % (3734418)------------------------------
% 22.24/4.16 % (3734418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/4.16 % (3734418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/4.16 % (3734418)CaDiCaL version: 2.1.3
% 22.24/4.16 % (3734418)Termination reason: Refutation not found, incomplete strategy
% 22.24/4.16 % (3734418)Time elapsed: 0.001 s
% 22.24/4.16 % (3734418)Peak memory usage: 88 MB
% 22.24/4.16 % (3734420)lrs+10_1_sil=8000:sp=occurrence:random_seed=3673492264:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 22.24/4.16 % (3734420)Refutation not found, incomplete strategy
% 22.24/4.16 % (3734420)------------------------------
% 22.24/4.16 % (3734420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/4.16 % (3734420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/4.17 % (3734420)CaDiCaL version: 2.1.3
% 22.24/4.17 % (3734420)Termination reason: Refutation not found, incomplete strategy
% 22.24/4.17 % (3734420)Time elapsed: 0.001 s
% 22.24/4.17 % (3734420)Peak memory usage: 86 MB
% 22.24/4.17 % (3734415)------------------------------
% 22.24/4.17 % (3734415)------------------------------
% 22.24/4.17 % (3734418)------------------------------
% 22.24/4.17 % (3734418)------------------------------
% 22.24/4.17 % (3734417)------------------------------
% 22.24/4.17 % (3734417)------------------------------
% 22.24/4.17 % (3734425)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3935563830:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 22.24/4.17 % (3734424)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2505705511:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 22.24/4.17 % (3734424)Refutation not found, incomplete strategy
% 22.24/4.17 % (3734424)------------------------------
% 22.24/4.17 % (3734424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/4.17 % (3734424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/4.17 % (3734424)CaDiCaL version: 2.1.3
% 22.24/4.17 % (3734424)Termination reason: Refutation not found, incomplete strategy
% 22.24/4.17 % (3734424)Time elapsed: 0.002 s
% 22.24/4.17 % (3734424)Peak memory usage: 87 MB
% 22.24/4.17 % (3734424)Instructions burned: 1 (million)
% 22.24/4.17 % (3734420)------------------------------
% 22.24/4.17 % (3734420)------------------------------
% 22.24/4.17 % (3734426)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3197913940:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 22.24/4.17 [W928 09:45:21.115081339 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.24/4.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.24/4.17 [W928 09:45:21.115159652 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115270755 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115298295 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115334069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115356940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115392148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115418376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115455665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115479369 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115515779 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 [W928 09:45:21.115528261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.23/4.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.23/4.55 % (3734426)Instruction limit reached!
% 24.23/4.55 % (3734426)------------------------------
% 24.23/4.55 % (3734426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.23/4.55 % (3734426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.23/4.55 % (3734426)CaDiCaL version: 2.1.3
% 24.23/4.55 % (3734426)Termination reason: Instruction limit
% 24.23/4.55 % (3734426)Termination phase: Saturation
% 24.23/4.55 % (3734426)Time elapsed: 0.111 s
% 24.23/4.55 % (3734426)Peak memory usage: 93 MB
% 24.23/4.55 % (3734426)Instructions burned: 135 (million)
% 24.23/4.55 % (3734424)------------------------------
% 24.23/4.55 % (3734424)------------------------------
% 24.23/4.55 % (3734429)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=101721781:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 24.23/4.55 % (3734429)Refutation not found, incomplete strategy
% 30.57/5.40 % (3734429)------------------------------
% 30.57/5.40 % (3734429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.57/5.40 % (3734429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.57/5.40 % (3734429)CaDiCaL version: 2.1.3
% 30.57/5.40 % (3734429)Termination reason: Refutation not found, incomplete strategy
% 30.57/5.40 % (3734429)Time elapsed: 0.001 s
% 30.57/5.40 % (3734429)Peak memory usage: 86 MB
% 30.57/5.40 % (3734425)Refutation not found, incomplete strategy
% 30.57/5.40 % (3734425)------------------------------
% 30.57/5.40 % (3734425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.57/5.40 % (3734425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.57/5.40 % (3734425)CaDiCaL version: 2.1.3
% 30.57/5.40 % (3734425)Termination reason: Refutation not found, incomplete strategy
% 30.57/5.40 % (3734425)Time elapsed: 0.499 s
% 30.57/5.40 % (3734425)Peak memory usage: 125 MB
% 30.57/5.40 % (3734425)Instructions burned: 826 (million)
% 30.57/5.40 % (3734431)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3733045242:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 30.57/5.40 % (3734432)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1925743422:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 30.57/5.40 % (3734432)Refutation not found, incomplete strategy
% 30.57/5.40 % (3734432)------------------------------
% 30.57/5.40 % (3734432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.57/5.40 % (3734432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.57/5.40 % (3734432)CaDiCaL version: 2.1.3
% 30.57/5.40 % (3734432)Termination reason: Refutation not found, incomplete strategy
% 30.57/5.40 % (3734432)Time elapsed: 0.002 s
% 30.57/5.40 % (3734432)Peak memory usage: 87 MB
% 30.57/5.40 % (3734429)------------------------------
% 30.57/5.40 % (3734429)------------------------------
% 30.57/5.40 % (3734425)------------------------------
% 30.57/5.40 % (3734425)------------------------------
% 30.57/5.40 [W928 09:45:21.718371083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.57/5.40 [W928 09:45:21.718397408 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.57/5.40 [W928 09:45:21.718427150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.57/5.40 [W928 09:45:21.718436673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.57/5.40 [W928 09:45:21.718487074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.57/5.40 [W928 09:45:21.718496831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.57/5.40 [W928 09:45:21.718519646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.57/5.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.81/6.13 [W928 09:45:21.718529236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 35.81/6.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.81/6.13 [W928 09:45:21.718564337 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 35.81/6.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.81/6.13 [W928 09:45:21.718572947 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 35.81/6.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.81/6.13 [W928 09:45:21.718594277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 35.81/6.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.81/6.13 [W928 09:45:21.718603220 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 35.81/6.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.81/6.13 % (3734432)------------------------------
% 35.81/6.13 % (3734432)------------------------------
% 35.81/6.13 % (3734436)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=688785555:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 35.81/6.13 % (3734431)Refutation not found, incomplete strategy
% 35.81/6.13 % (3734431)------------------------------
% 35.81/6.13 % (3734431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/6.13 % (3734431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/6.13 % (3734431)CaDiCaL version: 2.1.3
% 35.81/6.13 % (3734431)Termination reason: Refutation not found, incomplete strategy
% 35.81/6.13 % (3734431)Time elapsed: 0.481 s
% 35.81/6.13 % (3734431)Peak memory usage: 125 MB
% 35.81/6.13 % (3734431)Instructions burned: 821 (million)
% 35.81/6.13 % (3734436)Instruction limit reached!
% 35.81/6.13 % (3734436)------------------------------
% 35.81/6.13 % (3734436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/6.13 % (3734436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/6.13 % (3734436)CaDiCaL version: 2.1.3
% 35.81/6.13 % (3734436)Termination reason: Instruction limit
% 35.81/6.13 % (3734436)Termination phase: Saturation
% 35.81/6.13 % (3734436)Time elapsed: 0.136 s
% 35.81/6.13 % (3734436)Peak memory usage: 91 MB
% 35.81/6.13 % (3734436)Instructions burned: 134 (million)
% 35.81/6.13 % (3734437)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1167937128:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/141Mi)
% 35.81/6.13 % (3734437)Refutation not found, incomplete strategy
% 35.81/6.13 % (3734437)------------------------------
% 35.81/6.13 % (3734437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/6.13 % (3734437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/6.13 % (3734437)CaDiCaL version: 2.1.3
% 35.81/6.13 % (3734437)Termination reason: Refutation not found, incomplete strategy
% 35.81/6.13 % (3734437)Time elapsed: 0.001 s
% 35.81/6.13 % (3734437)Peak memory usage: 86 MB
% 35.81/6.13 % (3734438)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4042504701:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 35.81/6.13 % (3734438)Refutation not found, incomplete strategy
% 35.81/6.13 % (3734438)------------------------------
% 35.81/6.13 % (3734438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/6.13 % (3734438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/6.13 % (3734438)CaDiCaL version: 2.1.3
% 35.81/6.13 % (3734438)Termination reason: Refutation not found, incomplete strategy
% 0.35/6.51 % (3734438)Time elapsed: 0.0000 s
% 0.35/6.51 % (3734438)Peak memory usage: 86 MB
% 0.35/6.51 % (3734431)------------------------------
% 0.35/6.51 % (3734431)------------------------------
% 0.35/6.51 % (3734413)Instruction limit reached!
% 0.35/6.51 % (3734413)------------------------------
% 0.35/6.51 % (3734413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734413)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734413)Termination reason: Instruction limit
% 0.35/6.51 % (3734413)Termination phase: Saturation
% 0.35/6.51 % (3734413)Time elapsed: 2.286 s
% 0.35/6.51 % (3734413)Peak memory usage: 136 MB
% 0.35/6.51 % (3734413)Instructions burned: 2351 (million)
% 0.35/6.51 % (3734441)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2140661499:i=6060:aac=none:ins=25_2966 on theBenchmark for (2966ds/6060Mi)
% 0.35/6.51 % (3734438)------------------------------
% 0.35/6.51 % (3734438)------------------------------
% 0.35/6.51 % (3734437)------------------------------
% 0.35/6.51 % (3734437)------------------------------
% 0.35/6.51 % (3734446)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2031770217:i=667:av=off:fsr=off_2963 on theBenchmark for (2963ds/667Mi)
% 0.35/6.51 % (3734446)Refutation not found, incomplete strategy
% 0.35/6.51 % (3734446)------------------------------
% 0.35/6.51 % (3734446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734446)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734446)Termination reason: Refutation not found, incomplete strategy
% 0.35/6.51 % (3734446)Time elapsed: 0.001 s
% 0.35/6.51 % (3734446)Peak memory usage: 87 MB
% 0.35/6.51 % (3734443)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4014150593:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2963 on theBenchmark for (2963ds/150Mi)
% 0.35/6.51 % (3734444)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=288484296:i=14155:bd=all_2963 on theBenchmark for (2963ds/14155Mi)
% 0.35/6.51 % (3734443)Instruction limit reached!
% 0.35/6.51 % (3734443)------------------------------
% 0.35/6.51 % (3734443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734443)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734443)Termination reason: Instruction limit
% 0.35/6.51 % (3734443)Termination phase: Saturation
% 0.35/6.51 % (3734443)Time elapsed: 0.127 s
% 0.35/6.51 % (3734443)Peak memory usage: 97 MB
% 0.35/6.51 % (3734443)Instructions burned: 150 (million)
% 0.35/6.51 % (3734447)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2964807230:s2a=on:i=185:s2at=1.8:fdi=4_2962 on theBenchmark for (2962ds/185Mi)
% 0.35/6.51 % (3734446)------------------------------
% 0.35/6.51 % (3734446)------------------------------
% 0.35/6.51 % (3734447)Instruction limit reached!
% 0.35/6.51 % (3734447)------------------------------
% 0.35/6.51 % (3734447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734447)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734447)Termination reason: Instruction limit
% 0.35/6.51 % (3734447)Termination phase: Saturation
% 0.35/6.51 % (3734447)Time elapsed: 0.146 s
% 0.35/6.51 % (3734447)Peak memory usage: 92 MB
% 0.35/6.51 % (3734447)Instructions burned: 186 (million)
% 0.35/6.51 % (3734452)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1160887089:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2959 on theBenchmark for (2959ds/193Mi)
% 0.35/6.51 % (3734452)Refutation not found, incomplete strategy
% 0.35/6.51 % (3734452)------------------------------
% 0.35/6.51 % (3734452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734452)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734452)Termination reason: Refutation not found, incomplete strategy
% 0.35/6.51 % (3734452)Time elapsed: 0.001 s
% 0.35/6.51 % (3734452)Peak memory usage: 86 MB
% 0.35/6.51 % (3734453)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2202800262:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2958 on theBenchmark for (2958ds/4850Mi)
% 0.35/6.51 % (3734453)Refutation not found, incomplete strategy
% 0.35/6.51 % (3734453)------------------------------
% 0.35/6.51 % (3734453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734453)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734453)Termination reason: Refutation not found, incomplete strategy
% 0.35/6.51 % (3734453)Time elapsed: 0.001 s
% 0.35/6.51 % (3734453)Peak memory usage: 87 MB
% 0.35/6.51 % (3734453)Instructions burned: 1 (million)
% 0.35/6.51 % (3734454)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3626583019:i=12111:sd=1:ss=included_2958 on theBenchmark for (2958ds/12111Mi)
% 0.35/6.51 % (3734453)------------------------------
% 0.35/6.51 % (3734453)------------------------------
% 0.35/6.51 % (3734452)------------------------------
% 0.35/6.51 % (3734452)------------------------------
% 0.35/6.51 % (3734458)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1184159963:i=319:kws=precedence:fsr=off_2954 on theBenchmark for (2954ds/319Mi)
% 0.35/6.51 % (3734458)First to succeed.
% 0.35/6.51 % (3734458)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3734385"
% 0.35/6.51 % (3734441)Refutation not found, incomplete strategy
% 0.35/6.51 % (3734441)------------------------------
% 0.35/6.51 % (3734441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734441)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734441)Termination reason: Refutation not found, incomplete strategy
% 0.35/6.51 % (3734441)Time elapsed: 1.307 s
% 0.35/6.51 % (3734441)Peak memory usage: 131 MB
% 0.35/6.51 % (3734441)Instructions burned: 1228 (million)
% 0.35/6.51 % (3734459)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1206419656:i=2064:ep=RST_2953 on theBenchmark for (2953ds/2064Mi)
% 0.35/6.51 % (3734459)Refutation not found, incomplete strategy
% 0.35/6.51 % (3734459)------------------------------
% 0.35/6.51 % (3734459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734459)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734459)Termination reason: Refutation not found, incomplete strategy
% 0.35/6.51 % (3734459)Time elapsed: 0.002 s
% 0.35/6.51 % (3734459)Peak memory usage: 87 MB
% 0.35/6.51 % (3734459)Instructions burned: 1 (million)
% 0.35/6.51 % SZS status Satisfiable for theBenchmark
% 0.35/6.51 % SZS output start Saturation.
% See solution above
% 0.35/6.51 % SZS output start Definitions and Model Updates.
% 0.35/6.51 for all inputs,
% 0.35/6.51 define a_holds(X0) := $true
% 0.35/6.51 for all inputs,
% 0.35/6.51 define b_stored(X0) := $true
% 0.35/6.51 for all inputs,
% 0.35/6.51 define b_holds(X0) := $true
% 0.35/6.51 % SZS output end Definitions and Model Updates.
% 0.35/6.51 % (3734458)------------------------------
% 0.35/6.51 % (3734458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.35/6.51 % (3734458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/6.51 % (3734458)CaDiCaL version: 2.1.3
% 0.35/6.51 % (3734458)Termination reason: Satisfiable
% 0.35/6.51 % (3734458)Time elapsed: 0.003 s
% 0.35/6.51 % (3734458)Peak memory usage: 88 MB
% 0.35/6.51 % (3734458)Instructions burned: 3 (million)
% 0.35/6.51 % (3734458)------------------------------
% 0.35/6.51 % (3734458)------------------------------
% 0.35/6.51 % (3734385)Success in time 5.028 s
% 0.35/6.51 % Vampire exiting
%------------------------------------------------------------------------------