%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV532-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:16:55 PM UTC 2026
% Result : Satisfiable 24.64s 5.43s
% Output : Saturation 24.64s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u261,axiom,
i5 = i4 ).
cnf(u314,axiom,
i8 = i6 ).
cnf(u385,axiom,
i6 = i9 ).
cnf(u427,axiom,
sF8 = sF12 ).
cnf(u431,axiom,
i6 = i4 ).
cnf(u445,axiom,
i0 = i3 ).
cnf(u499,axiom,
i1 = i2 ).
cnf(u549,axiom,
i7 = i6 ).
cnf(u553,axiom,
sF4 = sF41 ).
cnf(u710,axiom,
sF4 = sF51 ).
cnf(u850,axiom,
i2 = i3 ).
cnf(u952,axiom,
sF16 = sF20 ).
cnf(u955,axiom,
i6 != i2 ).
cnf(u1032,axiom,
sF72 = select(sF69,i6) ).
cnf(u228,axiom,
( select(sF28,X0) = select(sF30,X0)
| i2 = X0 ) ).
cnf(u404,axiom,
( select(sF73,X0) = select(sF75,X0)
| i6 = X0 ) ).
cnf(u819,axiom,
( select(sF15,X0) = select(sF54,X0)
| i2 = X0 ) ).
cnf(u879,axiom,
( select(sF62,X0) = select(sF63,X0)
| i2 = X0 ) ).
cnf(u1523,axiom,
sF4 = select(sF62,i2) ).
cnf(u1448,axiom,
sF4 = select(sF26,i2) ).
cnf(u1512,axiom,
sF65 = store(sF63,i2,sF4) ).
cnf(u1463,axiom,
sF34 = store(sF32,i2,sF4) ).
cnf(u1492,axiom,
sF16 = sF72 ).
cnf(u593,axiom,
sF1 = store(a1,i6,sF4) ).
cnf(u1461,axiom,
sF32 = store(sF30,i2,sF4) ).
cnf(u1460,axiom,
sF4 = sF33 ).
cnf(u760,axiom,
sF4 = sF8 ).
cnf(u1309,axiom,
( select(sF62,X0) = select(sF67,X0)
| i2 = X0 ) ).
cnf(u906,axiom,
( select(sF62,X0) = select(sF73,X0)
| i2 = X0
| i6 = X0 ) ).
cnf(u1482,axiom,
sF16 = sF37 ).
cnf(u348,axiom,
sF4 = sF10 ).
cnf(u795,axiom,
sF4 = select(sF54,i2) ).
cnf(u814,axiom,
sF15 = sF52 ).
cnf(u591,axiom,
sF4 = select(sF1,i6) ).
cnf(u878,axiom,
( select(sF60,X0) = select(sF62,X0)
| i2 = X0 ) ).
cnf(u807,axiom,
sF13 = sF50 ).
cnf(u917,axiom,
( select(sF1,X0) = select(sF62,X0)
| i6 = X0
| i2 = X0 ) ).
cnf(u1529,axiom,
sF4 = select(sF73,i2) ).
cnf(u1515,axiom,
sF4 = sF66 ).
cnf(u1484,axiom,
sF16 = select(sF38,i6) ).
cnf(u790,axiom,
sF9 = sF46 ).
cnf(u862,axiom,
i0 = i2 ).
cnf(u730,axiom,
( select(sF36,X0) = select(sF38,X0)
| i6 = X0 ) ).
cnf(u758,axiom,
( select(sF1,X0) = select(sF13,X0)
| i6 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u1452,axiom,
sF4 = select(sF30,i2) ).
cnf(u875,axiom,
( select(sF23,X0) = select(sF25,X0)
| i2 = X0 ) ).
cnf(u1530,axiom,
sF4 = select(sF58,i2) ).
cnf(u572,axiom,
( select(sF13,X0) = select(sF17,X0)
| i6 = X0 ) ).
cnf(u718,axiom,
( select(sF19,X0) = select(sF21,X0)
| i6 = X0 ) ).
cnf(u335,axiom,
( select(sF5,X0) = select(sF7,X0)
| i6 = X0 ) ).
cnf(u567,axiom,
( select(sF1,X0) = select(sF3,X0)
| i6 = X0 ) ).
cnf(u778,axiom,
sF13 = store(sF11,i6,sF4) ).
cnf(u900,axiom,
( select(sF25,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u793,axiom,
sF4 = sF53 ).
cnf(u963,axiom,
sF16 = select(sF23,i6) ).
cnf(u1525,axiom,
sF69 = store(sF67,i2,sF4) ).
cnf(u517,axiom,
( select(sF17,X0) = select(sF19,X0)
| i2 = X0 ) ).
cnf(u1447,axiom,
sF4 = sF27 ).
cnf(u1465,axiom,
sF4 = select(sF36,i2) ).
cnf(u755,axiom,
( select(sF13,X0) = select(sF21,X0)
| i6 = X0
| i2 = X0 ) ).
cnf(u1449,axiom,
sF28 = store(sF26,i2,sF4) ).
cnf(u1521,axiom,
sF62 = store(sF60,i2,sF4) ).
cnf(u620,axiom,
( select(sF1,X0) = select(sF7,X0)
| i6 = X0 ) ).
cnf(u584,axiom,
sF19 = store(sF17,i2,sF4) ).
cnf(u606,axiom,
sF3 = sF40 ).
cnf(u1455,axiom,
sF4 = sF31 ).
cnf(u1526,axiom,
sF4 = select(sF69,i2) ).
cnf(u731,axiom,
( select(sF58,X0) = select(sF60,X0)
| i6 = X0 ) ).
cnf(u342,axiom,
sF4 = sF6 ).
cnf(u1479,axiom,
sF36 = store(sF34,i6,sF16) ).
cnf(u401,axiom,
( select(sF13,X0) = select(sF15,X0)
| i6 = X0 ) ).
cnf(u1481,axiom,
sF16 = select(sF34,i6) ).
cnf(u1450,axiom,
sF4 = select(sF28,i2) ).
cnf(u1476,axiom,
sF16 = select(sF25,i6) ).
cnf(u1478,axiom,
sF16 = sF35 ).
cnf(u1456,axiom,
sF4 = select(sF23,i2) ).
cnf(u824,axiom,
sF56 = store(sF54,i6,sF16) ).
cnf(u1497,axiom,
sF75 = store(sF73,i6,sF16) ).
cnf(u355,axiom,
sF4 = select(sF7,i6) ).
cnf(u772,axiom,
sF4 = sF12 ).
cnf(u595,axiom,
sF4 = sF45 ).
cnf(u826,axiom,
sF16 = sF57 ).
cnf(u594,axiom,
sF4 = sF43 ).
cnf(u909,axiom,
( select(sF62,X0) = select(sF71,X0)
| i2 = X0 ) ).
cnf(u1528,axiom,
sF4 = select(sF71,i2) ).
cnf(u1445,axiom,
sF4 = select(sF21,i2) ).
cnf(u958,axiom,
sF16 = sF22 ).
cnf(u773,axiom,
sF4 = sF47 ).
cnf(u1517,axiom,
sF4 = select(sF67,i2) ).
cnf(u589,axiom,
sF0 = sF4 ).
cnf(u505,axiom,
sF16 = select(sF15,i2) ).
cnf(u1480,axiom,
sF16 = select(sF36,i6) ).
cnf(u1431,axiom,
sF16 = select(sF1,i2) ).
cnf(u1498,axiom,
sF16 = select(sF75,i6) ).
cnf(u876,axiom,
( select(sF25,X0) = select(sF26,X0)
| i2 = X0 ) ).
cnf(u830,axiom,
sF16 = select(sF60,i6) ).
cnf(u1458,axiom,
sF26 = store(sF25,i2,sF4) ).
cnf(u877,axiom,
( select(sF32,X0) = select(sF34,X0)
| i2 = X0 ) ).
cnf(u1527,axiom,
sF71 = store(sF69,i2,sF4) ).
cnf(u585,axiom,
sF4 = select(sF19,i2) ).
cnf(u321,axiom,
sF4 = select(sF3,i6) ).
cnf(u1298,axiom,
sF4 = select(sF54,i6) ).
cnf(u717,axiom,
( select(sF11,X0) = select(sF13,X0)
| i6 = X0 ) ).
cnf(u1524,axiom,
sF4 = sF70 ).
cnf(u1459,axiom,
sF4 = select(sF25,i2) ).
cnf(u1453,axiom,
sF30 = store(sF28,i2,sF4) ).
cnf(u1006,axiom,
( select(sF1,X0) = select(sF58,X0)
| i2 = X0
| i6 = X0 ) ).
cnf(u407,axiom,
sF15 = store(sF13,i6,sF4) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u821,axiom,
sF54 = store(sF15,i2,sF4) ).
cnf(u1494,axiom,
sF16 = select(sF73,i6) ).
cnf(u612,axiom,
sF5 = sF42 ).
cnf(u761,axiom,
( select(sF1,X0) = select(sF11,X0)
| i6 = X0 ) ).
cnf(u562,axiom,
sF16 = select(sF17,i6) ).
cnf(u1454,axiom,
sF4 = sF24 ).
cnf(u351,axiom,
sF4 = sF14 ).
cnf(u803,axiom,
sF11 = sF48 ).
cnf(u736,axiom,
sF4 = select(sF11,i6) ).
cnf(u518,axiom,
( select(sF26,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u907,axiom,
( select(sF25,X0) = select(sF32,X0)
| i2 = X0 ) ).
cnf(u699,axiom,
( select(sF1,X0) = select(sF9,X0)
| i6 = X0 ) ).
cnf(u1483,axiom,
sF38 = store(sF36,i6,sF16) ).
cnf(u1496,axiom,
sF16 = sF74 ).
cnf(u354,axiom,
sF7 = store(sF5,i6,sF4) ).
cnf(u1485,axiom,
sF16 = select(sF32,i6) ).
cnf(u250,axiom,
( select(sF71,X0) = select(sF73,X0)
| i6 = X0 ) ).
cnf(u577,axiom,
sF4 = sF18 ).
cnf(u765,axiom,
( select(sF54,X0) = select(sF58,X0)
| i6 = X0 ) ).
cnf(u1519,axiom,
sF4 = sF68 ).
cnf(u959,axiom,
sF21 = store(sF19,i6,sF16) ).
cnf(u1451,axiom,
sF4 = sF29 ).
cnf(u156,negated_conjecture,
sF38 != sF75 ).
cnf(u1522,axiom,
sF63 = store(sF62,i2,sF4) ).
cnf(u1516,axiom,
sF67 = store(sF65,i2,sF4) ).
cnf(u571,axiom,
( select(sF1,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u827,axiom,
sF58 = store(sF56,i6,sF16) ).
cnf(u1495,axiom,
sF16 = select(sF71,i6) ).
cnf(u402,axiom,
( select(sF34,X0) = select(sF36,X0)
| i6 = X0 ) ).
cnf(u774,axiom,
sF4 = sF49 ).
cnf(u828,axiom,
sF16 = select(sF58,i6) ).
cnf(u1493,axiom,
sF73 = store(sF71,i6,sF16) ).
cnf(u1513,axiom,
sF4 = select(sF65,i2) ).
cnf(u575,axiom,
sF2 = sF4 ).
cnf(u825,axiom,
sF16 = select(sF56,i6) ).
cnf(u619,axiom,
sF7 = sF44 ).
cnf(u1518,axiom,
sF4 = sF61 ).
cnf(u899,axiom,
( select(sF62,X0) = select(sF65,X0)
| i2 = X0 ) ).
cnf(u334,axiom,
( select(a1,X0) = select(sF1,X0)
| i6 = X0 ) ).
cnf(u962,axiom,
sF23 = store(sF21,i6,sF16) ).
cnf(u406,axiom,
sF4 = select(sF15,i6) ).
cnf(u898,axiom,
( select(sF62,X0) = select(sF69,X0)
| i2 = X0 ) ).
cnf(u729,axiom,
( select(sF21,X0) = select(sF23,X0)
| i6 = X0 ) ).
cnf(u1499,axiom,
sF16 = select(sF69,i6) ).
cnf(u960,axiom,
sF16 = select(sF21,i6) ).
cnf(u1457,axiom,
sF25 = store(sF23,i2,sF4) ).
cnf(u556,axiom,
sF17 = store(sF15,i6,sF16) ).
cnf(u829,axiom,
sF60 = store(sF58,i6,sF16) ).
cnf(u600,axiom,
sF4 = select(a1,i6) ).
cnf(u823,axiom,
sF16 = sF55 ).
cnf(u771,axiom,
sF4 = select(sF9,i6) ).
cnf(u586,axiom,
sF1 = sF39 ).
cnf(u1311,axiom,
( select(sF1,X0) = select(sF36,X0)
| i2 = X0
| i6 = X0 ) ).
cnf(u215,axiom,
( select(sF3,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u777,axiom,
sF4 = select(sF13,i6) ).
cnf(u569,axiom,
( select(sF54,X0) = select(sF56,X0)
| i6 = X0 ) ).
cnf(u601,axiom,
sF3 = store(sF1,i6,sF4) ).
cnf(u1520,axiom,
sF4 = select(sF60,i2) ).
cnf(u770,axiom,
sF9 = store(sF7,i6,sF4) ).
cnf(u161,axiom,
sF4 = select(sF5,i6) ).
cnf(u916,axiom,
( select(sF1,X0) = select(sF25,X0)
| i6 = X0
| i2 = X0 ) ).
cnf(u737,axiom,
sF11 = store(sF9,i6,sF4) ).
cnf(u1490,axiom,
sF16 = select(sF62,i6) ).
cnf(u15,axiom,
store(sF3,i6,sF4) = sF5 ).
cnf(u831,axiom,
sF16 = sF59 ).
cnf(u822,axiom,
( select(sF1,X0) = select(sF15,X0)
| i6 = X0 ) ).
cnf(u1464,axiom,
sF4 = select(sF34,i2) ).
cnf(u815,axiom,
( select(sF1,X0) = select(sF54,X0)
| i2 = X0
| i6 = X0 ) ).
cnf(u1510,axiom,
sF4 = sF64 ).
cnf(u961,axiom,
sF16 = select(sF19,i6) ).
cnf(u1514,axiom,
sF4 = select(sF63,i2) ).
cnf(u721,axiom,
i6 = i5 ).
cnf(u1305,axiom,
sF16 = select(sF13,i2) ).
cnf(u1462,axiom,
sF4 = select(sF32,i2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV532-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 % Computer : n015.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Mon Sep 28 11:38:17 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.26 Running first-order theorem proving
% 0.24/0.26 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
% 9.67/3.15 % (2565500)Input is clausal, will run a generic CNF schedule.
% 9.67/3.15 % (2565508)lrs+10_1_sil=8000:sp=occurrence:random_seed=3908790690:i=107:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/107Mi)
% 9.67/3.15 % (2565508)Instruction limit reached!
% 9.67/3.15 % (2565508)------------------------------
% 9.67/3.15 % (2565508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.67/3.15 % (2565508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/3.15 % (2565508)CaDiCaL version: 2.1.3
% 9.67/3.15 % (2565508)Termination reason: Instruction limit
% 9.67/3.15 % (2565508)Termination phase: Property scanning
% 9.67/3.15 % (2565508)Time elapsed: 0.022 s
% 9.67/3.15 % (2565508)Peak memory usage: 84 MB
% 9.67/3.15 % (2565508)Instructions burned: 109 (million)
% 9.67/3.15 % (2565506)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4118253627:i=132376:av=off_2986 on theBenchmark for (2986ds/132376Mi)
% 9.67/3.15 % (2565509)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3167421576:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/114Mi)
% 9.67/3.15 % (2565511)dis-21_1_sil=8000:lcm=predicate:random_seed=39604197:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2986 on theBenchmark for (2986ds/117Mi)
% 9.67/3.15 % (2565510)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2370336958:s2a=on:i=180:gtg=position_2986 on theBenchmark for (2986ds/180Mi)
% 9.67/3.15 % (2565505)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=1694731155:i=140167_2986 on theBenchmark for (2986ds/140167Mi)
% 9.67/3.15 % (2565507)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3967975482:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2986 on theBenchmark for (2986ds/137899Mi)
% 9.67/3.15 % (2565509)Instruction limit reached!
% 9.67/3.15 % (2565509)------------------------------
% 9.67/3.15 % (2565509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.67/3.15 % (2565509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/3.15 % (2565509)CaDiCaL version: 2.1.3
% 9.67/3.15 % (2565509)Termination reason: Instruction limit
% 9.67/3.15 % (2565509)Termination phase: Property scanning
% 9.67/3.15 % (2565509)Time elapsed: 0.043 s
% 9.67/3.15 % (2565509)Peak memory usage: 84 MB
% 9.67/3.15 % (2565509)Instructions burned: 115 (million)
% 9.67/3.15 % (2565511)Instruction limit reached!
% 9.67/3.15 % (2565511)------------------------------
% 9.67/3.15 % (2565511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.67/3.15 % (2565511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/3.15 % (2565511)CaDiCaL version: 2.1.3
% 9.67/3.15 % (2565511)Termination reason: Instruction limit
% 9.67/3.15 % (2565511)Termination phase: Property scanning
% 9.67/3.15 % (2565511)Time elapsed: 0.044 s
% 9.67/3.15 % (2565511)Peak memory usage: 84 MB
% 9.67/3.15 % (2565511)Instructions burned: 119 (million)
% 9.67/3.15 % (2565510)Instruction limit reached!
% 9.67/3.15 % (2565510)------------------------------
% 9.67/3.15 % (2565510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.67/3.15 % (2565510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/3.15 % (2565510)CaDiCaL version: 2.1.3
% 9.67/3.15 % (2565510)Termination reason: Instruction limit
% 9.67/3.15 % (2565510)Termination phase: Property scanning
% 9.67/3.15 % (2565510)Time elapsed: 0.057 s
% 9.67/3.15 % (2565510)Peak memory usage: 84 MB
% 9.67/3.15 % (2565510)Instructions burned: 180 (million)
% 9.67/3.15 % (2565513)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=4186443934:i=143:sd=2:aac=none:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/143Mi)
% 9.67/3.15 % (2565513)Instruction limit reached!
% 9.67/3.15 % (2565513)------------------------------
% 9.67/3.15 % (2565513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.67/3.15 % (2565513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/3.15 % (2565513)CaDiCaL version: 2.1.3
% 9.67/3.15 % (2565513)Termination reason: Instruction limit
% 9.67/3.15 % (2565513)Termination phase: Property scanning
% 9.67/3.15 % (2565513)Time elapsed: 0.028 s
% 9.67/3.15 % (2565513)Peak memory usage: 84 MB
% 9.67/3.15 % (2565513)Instructions burned: 148 (million)
% 13.11/3.78 % (2565520)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3651659904:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2984 on theBenchmark for (2984ds/189Mi)
% 13.11/3.78 % (2565521)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2088127226:st=4:i=219:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/219Mi)
% 13.11/3.78 % (2565522)lrs+10_64_to=lpo:sil=8000:random_seed=192897068:i=126:bd=preordered_2984 on theBenchmark for (2984ds/126Mi)
% 13.11/3.78 % (2565524)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=208830245:avsq=on:i=194:fgj=on:bd=preordered_2983 on theBenchmark for (2983ds/194Mi)
% 13.11/3.78 % (2565524)Instruction limit reached!
% 13.11/3.78 % (2565524)------------------------------
% 13.11/3.78 % (2565524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.11/3.78 % (2565524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.11/3.78 % (2565524)CaDiCaL version: 2.1.3
% 13.11/3.78 % (2565524)Termination reason: Instruction limit
% 13.11/3.78 % (2565524)Termination phase: Saturation
% 13.11/3.78 % (2565524)Time elapsed: 0.046 s
% 13.11/3.78 % (2565524)Peak memory usage: 103 MB
% 13.11/3.78 % (2565524)Instructions burned: 195 (million)
% 13.11/3.78 % (2565520)Instruction limit reached!
% 13.11/3.78 % (2565520)------------------------------
% 13.11/3.78 % (2565520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.11/3.78 % (2565520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.11/3.78 % (2565520)CaDiCaL version: 2.1.3
% 13.11/3.78 % (2565520)Termination reason: Instruction limit
% 13.11/3.78 % (2565520)Termination phase: SInE selection
% 13.11/3.78 % (2565520)Time elapsed: 0.072 s
% 13.11/3.78 % (2565520)Peak memory usage: 83 MB
% 13.11/3.78 % (2565520)Instructions burned: 190 (million)
% 13.11/3.78 % (2565522)Instruction limit reached!
% 13.11/3.78 % (2565522)------------------------------
% 13.11/3.78 % (2565522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.11/3.78 % (2565522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.11/3.78 % (2565522)CaDiCaL version: 2.1.3
% 13.11/3.78 % (2565522)Termination reason: Instruction limit
% 13.11/3.78 % (2565522)Termination phase: Saturation
% 13.11/3.78 % (2565522)Time elapsed: 0.058 s
% 13.11/3.78 % (2565522)Peak memory usage: 99 MB
% 13.11/3.78 % (2565522)Instructions burned: 128 (million)
% 13.11/3.78 % (2565521)Instruction limit reached!
% 13.11/3.78 % (2565521)------------------------------
% 13.11/3.78 % (2565521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.11/3.78 % (2565521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.11/3.78 % (2565521)CaDiCaL version: 2.1.3
% 13.11/3.78 % (2565521)Termination reason: Instruction limit
% 13.11/3.78 % (2565521)Termination phase: Property scanning
% 13.11/3.78 % (2565521)Time elapsed: 0.077 s
% 13.11/3.78 % (2565521)Peak memory usage: 84 MB
% 13.11/3.78 % (2565521)Instructions burned: 222 (million)
% 13.11/3.78 % (2565529)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1901863196:i=157:gtg=all_2982 on theBenchmark for (2982ds/157Mi)
% 13.11/3.78 % (2565529)Instruction limit reached!
% 13.11/3.78 % (2565529)------------------------------
% 13.11/3.78 % (2565529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.11/3.78 % (2565529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.11/3.78 % (2565529)CaDiCaL version: 2.1.3
% 13.11/3.78 % (2565529)Termination reason: Instruction limit
% 13.11/3.78 % (2565529)Termination phase: Property scanning
% 13.11/3.78 % (2565529)Time elapsed: 0.027 s
% 13.11/3.78 % (2565529)Peak memory usage: 84 MB
% 13.11/3.78 % (2565529)Instructions burned: 162 (million)
% 13.11/3.78 % (2565530)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2246468812:i=3394:sd=4:ss=included:sgt=64_2982 on theBenchmark for (2982ds/3394Mi)
% 13.11/3.78 % (2565531)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=1931875358:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2982 on theBenchmark for (2982ds/106Mi)
% 13.11/3.78 % (2565532)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1885141870:i=107_2982 on theBenchmark for (2982ds/107Mi)
% 13.11/3.78 % (2565531)Instruction limit reached!
% 13.11/3.78 % (2565531)------------------------------
% 13.11/3.78 % (2565531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/4.56 % (2565531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/4.56 % (2565531)CaDiCaL version: 2.1.3
% 19.02/4.56 % (2565531)Termination reason: Instruction limit
% 19.02/4.56 % (2565531)Termination phase: SInE selection
% 19.02/4.56 % (2565531)Time elapsed: 0.040 s
% 19.02/4.56 % (2565531)Peak memory usage: 83 MB
% 19.02/4.56 % (2565531)Instructions burned: 108 (million)
% 19.02/4.56 % (2565535)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3257881892:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2981 on theBenchmark for (2981ds/242Mi)
% 19.02/4.56 % (2565532)Instruction limit reached!
% 19.02/4.56 % (2565532)------------------------------
% 19.02/4.56 % (2565532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/4.56 % (2565532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/4.56 % (2565532)CaDiCaL version: 2.1.3
% 19.02/4.56 % (2565532)Termination reason: Instruction limit
% 19.02/4.56 % (2565532)Termination phase: Saturation
% 19.02/4.56 % (2565532)Time elapsed: 0.124 s
% 19.02/4.56 % (2565532)Peak memory usage: 147 MB
% 19.02/4.56 % (2565532)Instructions burned: 108 (million)
% 19.02/4.56 % (2565535)Instruction limit reached!
% 19.02/4.56 % (2565535)------------------------------
% 19.02/4.56 % (2565535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/4.56 % (2565535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/4.56 % (2565535)CaDiCaL version: 2.1.3
% 19.02/4.56 % (2565535)Termination reason: Instruction limit
% 19.02/4.56 % (2565535)Termination phase: Property scanning
% 19.02/4.56 % (2565535)Time elapsed: 0.042 s
% 19.02/4.56 % (2565535)Peak memory usage: 84 MB
% 19.02/4.56 % (2565535)Instructions burned: 246 (million)
% 19.02/4.56 % (2565538)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=104752165:cond=fast:i=5208:av=off_2980 on theBenchmark for (2980ds/5208Mi)
% 19.02/4.56 % (2565541)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=58940673:i=499:bd=all_2979 on theBenchmark for (2979ds/499Mi)
% 19.02/4.56 % (2565540)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3524585846:i=134:sd=2:doe=on:ss=axioms:sgt=14_2979 on theBenchmark for (2979ds/134Mi)
% 19.02/4.56 % (2565540)Instruction limit reached!
% 19.02/4.56 % (2565540)------------------------------
% 19.02/4.56 % (2565540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/4.56 % (2565540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/4.56 % (2565540)CaDiCaL version: 2.1.3
% 19.02/4.56 % (2565540)Termination reason: Instruction limit
% 19.02/4.56 % (2565540)Termination phase: Property scanning
% 19.02/4.56 % (2565540)Time elapsed: 0.049 s
% 19.02/4.56 % (2565540)Peak memory usage: 84 MB
% 19.02/4.56 % (2565540)Instructions burned: 135 (million)
% 19.02/4.56 % (2565541)Instruction limit reached!
% 19.02/4.56 % (2565541)------------------------------
% 19.02/4.56 % (2565541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/4.56 % (2565541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/4.56 % (2565541)CaDiCaL version: 2.1.3
% 19.02/4.56 % (2565541)Termination reason: Instruction limit
% 19.02/4.56 % (2565541)Termination phase: Saturation
% 19.02/4.56 % (2565541)Time elapsed: 0.111 s
% 19.02/4.56 % (2565541)Peak memory usage: 118 MB
% 19.02/4.56 % (2565541)Instructions burned: 501 (million)
% 19.02/4.56 % (2565546)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2941458741:i=264:kws=precedence:fsr=off_2977 on theBenchmark for (2977ds/264Mi)
% 19.02/4.56 % (2565545)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2983937394:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 19.02/4.56 % (2565546)Instruction limit reached!
% 19.02/4.56 % (2565546)------------------------------
% 19.02/4.56 % (2565546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/4.56 % (2565546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/4.56 % (2565546)CaDiCaL version: 2.1.3
% 19.02/4.56 % (2565546)Termination reason: Instruction limit
% 19.02/4.56 % (2565546)Termination phase: Saturation
% 19.02/4.56 % (2565546)Time elapsed: 0.067 s
% 19.02/4.56 % (2565546)Peak memory usage: 108 MB
% 19.02/4.56 % (2565546)Instructions burned: 270 (million)
% 22.75/5.23 % (2565545)Instruction limit reached!
% 22.75/5.23 % (2565545)------------------------------
% 22.75/5.23 % (2565545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565545)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565545)Termination reason: Instruction limit
% 22.75/5.23 % (2565545)Termination phase: Saturation
% 22.75/5.23 % (2565545)Time elapsed: 0.083 s
% 22.75/5.23 % (2565545)Peak memory usage: 103 MB
% 22.75/5.23 % (2565545)Instructions burned: 193 (million)
% 22.75/5.23 % (2565549)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3111106645:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 22.75/5.23 % (2565549)Instruction limit reached!
% 22.75/5.23 % (2565549)------------------------------
% 22.75/5.23 % (2565549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565549)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565549)Termination reason: Instruction limit
% 22.75/5.23 % (2565549)Termination phase: Property scanning
% 22.75/5.23 % (2565549)Time elapsed: 0.027 s
% 22.75/5.23 % (2565549)Peak memory usage: 84 MB
% 22.75/5.23 % (2565549)Instructions burned: 162 (million)
% 22.75/5.23 % (2565550)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=1354735289:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi)
% 22.75/5.23 % (2565505)Refutation not found, incomplete strategy
% 22.75/5.23 % (2565505)------------------------------
% 22.75/5.23 % (2565505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565505)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565505)Termination reason: Refutation not found, incomplete strategy
% 22.75/5.23 % (2565505)Time elapsed: 1.178 s
% 22.75/5.23 % (2565505)Peak memory usage: 135 MB
% 22.75/5.23 % (2565505)Instructions burned: 2159 (million)
% 22.75/5.23 % (2565552)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=403388274:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 22.75/5.23 % (2565552)Instruction limit reached!
% 22.75/5.23 % (2565552)------------------------------
% 22.75/5.23 % (2565552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565552)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565552)Termination reason: Instruction limit
% 22.75/5.23 % (2565552)Termination phase: Property scanning
% 22.75/5.23 % (2565552)Time elapsed: 0.095 s
% 22.75/5.23 % (2565552)Peak memory usage: 84 MB
% 22.75/5.23 % (2565552)Instructions burned: 542 (million)
% 22.75/5.23 % (2565507)Refutation not found, incomplete strategy
% 22.75/5.23 % (2565507)------------------------------
% 22.75/5.23 % (2565507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565507)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565507)Termination reason: Refutation not found, incomplete strategy
% 22.75/5.23 % (2565507)Time elapsed: 1.404 s
% 22.75/5.23 % (2565507)Peak memory usage: 135 MB
% 22.75/5.23 % (2565507)Instructions burned: 2903 (million)
% 22.75/5.23 % (2565505)------------------------------
% 22.75/5.23 % (2565505)------------------------------
% 22.75/5.23 % (2565555)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2569097355:i=180:bd=preordered:av=off_2971 on theBenchmark for (2971ds/180Mi)
% 22.75/5.23 % (2565555)Instruction limit reached!
% 22.75/5.23 % (2565555)------------------------------
% 22.75/5.23 % (2565555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565555)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565555)Termination reason: Instruction limit
% 22.75/5.23 % (2565555)Termination phase: Saturation
% 22.75/5.23 % (2565555)Time elapsed: 0.045 s
% 22.75/5.23 % (2565555)Peak memory usage: 102 MB
% 22.75/5.23 % (2565555)Instructions burned: 183 (million)
% 22.75/5.23 % (2565556)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=104665655:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/10307Mi)
% 22.75/5.23 % (2565558)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1578013196:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 22.75/5.23 % (2565507)------------------------------
% 22.75/5.23 % (2565507)------------------------------
% 22.75/5.23 % (2565558)Instruction limit reached!
% 22.75/5.23 % (2565558)------------------------------
% 22.75/5.23 % (2565558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565558)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565558)Termination reason: Instruction limit
% 22.75/5.23 % (2565558)Termination phase: Property scanning
% 22.75/5.23 % (2565558)Time elapsed: 0.070 s
% 22.75/5.23 % (2565558)Peak memory usage: 84 MB
% 22.75/5.23 % (2565558)Instructions burned: 415 (million)
% 22.75/5.23 % (2565538)Refutation not found, incomplete strategy
% 22.75/5.23 % (2565538)------------------------------
% 22.75/5.23 % (2565538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565538)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565538)Termination reason: Refutation not found, incomplete strategy
% 22.75/5.23 % (2565538)Time elapsed: 1.104 s
% 22.75/5.23 % (2565538)Peak memory usage: 133 MB
% 22.75/5.23 % (2565538)Instructions burned: 2061 (million)
% 22.75/5.23 % (2565561)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3593150308:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 22.75/5.23 % (2565562)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2994660663:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2968 on theBenchmark for (2968ds/303Mi)
% 22.75/5.23 % (2565562)Instruction limit reached!
% 22.75/5.23 % (2565562)------------------------------
% 22.75/5.23 % (2565562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565562)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565562)Termination reason: Instruction limit
% 22.75/5.23 % (2565562)Termination phase: Property scanning
% 22.75/5.23 % (2565562)Time elapsed: 0.059 s
% 22.75/5.23 % (2565562)Peak memory usage: 84 MB
% 22.75/5.23 % (2565562)Instructions burned: 307 (million)
% 22.75/5.23 % (2565538)------------------------------
% 22.75/5.23 % (2565538)------------------------------
% 22.75/5.23 % (2565565)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1566607287:st=4:i=720:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/720Mi)
% 22.75/5.23 % (2565566)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1852390566:i=598:bs=on:bd=preordered:av=off:ss=axioms_2965 on theBenchmark for (2965ds/598Mi)
% 22.75/5.23 % (2565565)Instruction limit reached!
% 22.75/5.23 % (2565565)------------------------------
% 22.75/5.23 % (2565565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565565)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565565)Termination reason: Instruction limit
% 22.75/5.23 % (2565565)Termination phase: Property scanning
% 22.75/5.23 % (2565565)Time elapsed: 0.237 s
% 22.75/5.23 % (2565565)Peak memory usage: 84 MB
% 22.75/5.23 % (2565565)Instructions burned: 721 (million)
% 22.75/5.23 % (2565566)Instruction limit reached!
% 22.75/5.23 % (2565566)------------------------------
% 22.75/5.23 % (2565566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.75/5.23 % (2565566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/5.23 % (2565566)CaDiCaL version: 2.1.3
% 22.75/5.23 % (2565566)Termination reason: Instruction limit
% 22.75/5.23 % (2565566)Termination phase: Property scanning
% 22.75/5.23 % (2565566)Time elapsed: 0.199 s
% 22.75/5.23 % (2565566)Peak memory usage: 84 MB
% 22.75/5.23 % (2565566)Instructions burned: 601 (million)
% 22.75/5.23 % (2565550)Instruction limit reached!
% 22.75/5.23 % (2565550)------------------------------
% 22.75/5.23 % (2565550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.64/5.43 % (2565550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.64/5.43 % (2565550)CaDiCaL version: 2.1.3
% 24.64/5.43 % (2565550)Termination reason: Instruction limit
% 24.64/5.43 % (2565550)Termination phase: Saturation
% 24.64/5.43 % (2565550)Time elapsed: 1.222 s
% 24.64/5.43 % (2565550)Peak memory usage: 220 MB
% 24.64/5.43 % (2565550)Instructions burned: 3262 (million)
% 24.64/5.43 % (2565569)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2831867642:i=2989:sd=3:ss=axioms:sgt=60_2962 on theBenchmark for (2962ds/2989Mi)
% 24.64/5.43 % (2565570)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1974995428:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2961 on theBenchmark for (2961ds/1997Mi)
% 24.64/5.43 % (2565571)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2520520833:i=2088:bd=preordered:av=off_2961 on theBenchmark for (2961ds/2088Mi)
% 24.64/5.43 % (2565556)First to succeed.
% 24.64/5.43 % (2565556)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2565500"
% 24.64/5.43 % SZS status Satisfiable for theBenchmark
% 24.64/5.43 % SZS output start Saturation.
% See solution above
% 24.64/5.43 % SZS output start Definitions and Model Updates.
% 24.64/5.43 % SZS output end Definitions and Model Updates.
% 24.64/5.43 % (2565556)------------------------------
% 24.64/5.43 % (2565556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.64/5.43 % (2565556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.64/5.43 % (2565556)CaDiCaL version: 2.1.3
% 24.64/5.43 % (2565556)Termination reason: Satisfiable
% 24.64/5.43 % (2565556)Time elapsed: 1.160 s
% 24.64/5.43 % (2565556)Peak memory usage: 135 MB
% 24.64/5.43 % (2565556)Instructions burned: 2193 (million)
% 24.64/5.43 % (2565556)------------------------------
% 24.64/5.43 % (2565556)------------------------------
% 24.64/5.43 % (2565500)Success in time 4.535 s
% 24.64/5.43 % Vampire exiting
%------------------------------------------------------------------------------