%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV531-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 : n014.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 25.54s 5.58s
% Output : Saturation 25.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u261,axiom,
i5 = i4 ).
cnf(u265,axiom,
sF14 = select(sF9,i4) ).
cnf(u318,axiom,
i8 = i6 ).
cnf(u322,axiom,
sF43 = select(sF39,i6) ).
cnf(u389,axiom,
i0 = i3 ).
cnf(u393,axiom,
sF68 = select(sF69,i0) ).
cnf(u446,axiom,
sF12 = select(sF13,i9) ).
cnf(u490,axiom,
i1 != i2 ).
cnf(u495,axiom,
sF64 = select(sF65,i1) ).
cnf(u544,axiom,
i7 = i6 ).
cnf(u548,axiom,
sF4 = sF41 ).
cnf(u700,axiom,
i6 = i4 ).
cnf(u704,axiom,
sF4 = sF49 ).
cnf(u874,axiom,
sF16 = sF20 ).
cnf(u878,axiom,
i6 = i2 ).
cnf(u895,axiom,
i2 = i3 ).
cnf(u1599,axiom,
sF14 = select(sF5,i4) ).
cnf(u1610,axiom,
sF12 = select(sF9,i9) ).
cnf(u1621,axiom,
sF12 = select(sF5,i9) ).
cnf(u1636,axiom,
i8 = i7 ).
cnf(u1669,axiom,
sF31 = select(sF32,i0) ).
cnf(u1676,axiom,
sF57 = select(sF58,i5) ).
cnf(u1695,axiom,
sF72 = select(sF73,i9) ).
cnf(u1704,axiom,
sF20 = select(sF21,i5) ).
cnf(u1713,axiom,
sF49 = select(sF50,i9) ).
cnf(u1722,axiom,
sF35 = select(sF36,i5) ).
cnf(u1741,axiom,
sF53 = select(sF54,i7) ).
cnf(u1952,axiom,
sF27 = select(sF28,i2) ).
cnf(u2063,axiom,
i7 = i9 ).
cnf(u2067,axiom,
i6 = i9 ).
cnf(u2136,axiom,
i0 = i2 ).
cnf(u2209,axiom,
i7 = i5 ).
cnf(u3019,axiom,
sF4 = select(sF67,i6) ).
cnf(u2998,axiom,
( select(sF21,X0) = select(sF25,X0)
| i6 = X0 ) ).
cnf(u2794,axiom,
sF54 = store(sF15,i1,sF4) ).
cnf(u2562,axiom,
( select(sF5,X0) = select(sF7,X0)
| i6 = X0 ) ).
cnf(u3028,axiom,
sF73 = store(sF71,i6,sF4) ).
cnf(u2370,axiom,
( select(sF28,X0) = select(sF32,X0)
| i6 = X0 ) ).
cnf(u2885,axiom,
sF16 = select(sF28,i1) ).
cnf(u2897,axiom,
sF16 = select(sF1,i1) ).
cnf(u2815,axiom,
sF16 = sF59 ).
cnf(u1116,axiom,
i6 = i3 ).
cnf(u2816,axiom,
sF16 = select(sF56,i6) ).
cnf(u3091,axiom,
sF4 = sF37 ).
cnf(u3090,axiom,
sF36 = store(sF34,i6,sF4) ).
cnf(u2442,axiom,
sF4 = sF43 ).
cnf(u2041,axiom,
( select(sF11,X0) = select(sF13,X0)
| i6 = X0 ) ).
cnf(u2849,axiom,
sF16 = select(sF67,i1) ).
cnf(u2795,axiom,
sF16 = sF55 ).
cnf(u2444,axiom,
sF4 = select(sF1,i6) ).
cnf(u2563,axiom,
( select(sF5,X0) = select(sF9,X0)
| i6 = X0 ) ).
cnf(u2887,axiom,
sF16 = select(sF26,i6) ).
cnf(u2759,axiom,
sF4 = select(sF19,i1) ).
cnf(u2520,axiom,
sF4 = sF53 ).
cnf(u2890,axiom,
sF16 = select(sF25,i6) ).
cnf(u2396,axiom,
( select(sF28,X0) = select(sF34,X0)
| i6 = X0 ) ).
cnf(u716,axiom,
i6 = i5 ).
cnf(u2591,axiom,
sF4 = select(sF7,i6) ).
cnf(u2057,axiom,
sF4 = select(sF9,i6) ).
cnf(u2390,axiom,
( select(sF69,X0) = select(sF71,X0)
| i6 = X0 ) ).
cnf(u2509,axiom,
sF11 = sF48 ).
cnf(u2790,axiom,
( select(sF54,X0) = select(sF58,X0)
| i6 = X0 ) ).
cnf(u3015,axiom,
sF65 = store(sF63,i6,sF4) ).
cnf(u245,axiom,
( select(sF65,X0) = select(sF67,X0)
| i1 = X0 ) ).
cnf(u1797,axiom,
sF2 = sF4 ).
cnf(u225,axiom,
( select(sF26,X0) = select(sF28,X0)
| i1 = X0 ) ).
cnf(u2096,axiom,
sF4 = sF18 ).
cnf(u2889,axiom,
sF26 = store(sF25,i6,sF16) ).
cnf(u3013,axiom,
sF4 = select(sF63,i1) ).
cnf(u2969,axiom,
( select(sF1,X0) = select(sF54,X0)
| i6 = X0
| i1 = X0 ) ).
cnf(u2814,axiom,
sF16 = select(sF58,i6) ).
cnf(u15,axiom,
store(sF3,i6,sF4) = sF5 ).
cnf(u3025,axiom,
sF4 = sF74 ).
cnf(u2818,axiom,
sF16 = select(sF60,i6) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u2564,axiom,
sF3 = store(sF1,i6,sF4) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u3021,axiom,
sF4 = select(sF69,i6) ).
cnf(u1907,axiom,
sF5 = sF42 ).
cnf(u2854,axiom,
sF62 = store(sF60,i6,sF16) ).
cnf(u2590,axiom,
sF7 = store(sF5,i6,sF4) ).
cnf(u3079,axiom,
sF30 = store(sF28,i6,sF4) ).
cnf(u2582,axiom,
( select(sF58,X0) = select(sF60,X0)
| i6 = X0 ) ).
cnf(u2602,axiom,
sF4 = select(sF54,i6) ).
cnf(u3084,axiom,
sF4 = sF35 ).
cnf(u2580,axiom,
( select(sF21,X0) = select(sF23,X0)
| i6 = X0 ) ).
cnf(u2474,axiom,
sF4 = sF47 ).
cnf(u3078,axiom,
sF4 = sF33 ).
cnf(u3023,axiom,
sF71 = store(sF69,i6,sF4) ).
cnf(u3017,axiom,
sF4 = sF68 ).
cnf(u3087,axiom,
sF4 = select(sF38,i6) ).
cnf(u2470,axiom,
sF13 = store(sF11,i6,sF4) ).
cnf(u784,axiom,
sF4 = sF8 ).
cnf(u2848,axiom,
sF67 = store(sF65,i1,sF16) ).
cnf(u3026,axiom,
sF4 = select(sF75,i6) ).
cnf(u2584,axiom,
( select(sF5,X0) = select(sF11,X0)
| i6 = X0 ) ).
cnf(u2812,axiom,
sF16 = sF57 ).
cnf(u1888,axiom,
sF1 = sF39 ).
cnf(u156,negated_conjecture,
sF38 != sF75 ).
cnf(u2603,axiom,
( select(sF1,X0) = select(sF13,X0)
| i6 = X0 ) ).
cnf(u2369,axiom,
( select(sF67,X0) = select(sF69,X0)
| i6 = X0 ) ).
cnf(u2592,axiom,
sF11 = store(sF9,i6,sF4) ).
cnf(u2491,axiom,
sF9 = sF46 ).
cnf(u2879,axiom,
sF16 = select(sF21,i6) ).
cnf(u2819,axiom,
sF60 = store(sF58,i6,sF16) ).
cnf(u2850,axiom,
sF16 = select(sF63,i6) ).
cnf(u2929,axiom,
( select(sF17,X0) = select(sF21,X0)
| i1 = X0
| i6 = X0 ) ).
cnf(u3030,axiom,
sF4 = select(sF62,i1) ).
cnf(u2878,axiom,
sF21 = store(sF19,i6,sF16) ).
cnf(u3022,axiom,
sF4 = select(sF71,i6) ).
cnf(u2877,axiom,
sF16 = sF22 ).
cnf(u2387,axiom,
( select(sF25,X0) = select(sF26,X0)
| i6 = X0 ) ).
cnf(u2581,axiom,
( select(sF36,X0) = select(sF38,X0)
| i6 = X0 ) ).
cnf(u2978,axiom,
( select(sF1,X0) = select(sF69,X0)
| i1 = X0
| i6 = X0 ) ).
cnf(u2577,axiom,
sF4 = select(sF15,i6) ).
cnf(u3016,axiom,
sF4 = select(sF65,i6) ).
cnf(u2389,axiom,
( select(sF62,X0) = select(sF63,X0)
| i6 = X0 ) ).
cnf(u2884,axiom,
sF28 = store(sF26,i1,sF16) ).
cnf(u2558,axiom,
( select(sF54,X0) = select(sF56,X0)
| i6 = X0 ) ).
cnf(u2557,axiom,
( select(sF15,X0) = select(sF17,X0)
| i6 = X0 ) ).
cnf(u2760,axiom,
( select(sF15,X0) = select(sF54,X0)
| i1 = X0 ) ).
cnf(u2881,axiom,
sF23 = store(sF21,i6,sF16) ).
cnf(u3020,axiom,
sF69 = store(sF67,i6,sF4) ).
cnf(u2888,axiom,
sF25 = store(sF23,i6,sF16) ).
cnf(u3024,axiom,
sF4 = sF72 ).
cnf(u2556,axiom,
( select(sF1,X0) = select(sF3,X0)
| i6 = X0 ) ).
cnf(u3027,axiom,
sF75 = store(sF73,i6,sF4) ).
cnf(u3077,axiom,
sF4 = select(sF26,i1) ).
cnf(u3075,axiom,
sF4 = sF29 ).
cnf(u3080,axiom,
sF4 = select(sF30,i6) ).
cnf(u2352,axiom,
sF4 = sF6 ).
cnf(u2758,axiom,
sF4 = select(sF54,i1) ).
cnf(u2616,axiom,
( select(sF69,X0) = select(sF73,X0)
| i6 = X0 ) ).
cnf(u2612,axiom,
sF16 = select(sF17,i6) ).
cnf(u2851,axiom,
sF16 = select(sF69,i1) ).
cnf(u2515,axiom,
sF4 = sF51 ).
cnf(u1872,axiom,
sF0 = sF4 ).
cnf(u2847,axiom,
sF16 = sF66 ).
cnf(u161,axiom,
sF4 = select(sF5,i6) ).
cnf(u2517,axiom,
sF13 = sF50 ).
cnf(u2439,axiom,
sF4 = sF10 ).
cnf(u2597,axiom,
sF9 = store(sF7,i6,sF4) ).
cnf(u2469,axiom,
sF4 = select(sF13,i6) ).
cnf(u2386,axiom,
( select(sF23,X0) = select(sF25,X0)
| i6 = X0 ) ).
cnf(u3083,axiom,
sF34 = store(sF32,i6,sF4) ).
cnf(u3085,axiom,
sF32 = store(sF30,i6,sF4) ).
cnf(u3088,axiom,
sF38 = store(sF36,i6,sF4) ).
cnf(u2955,axiom,
sF16 = select(sF17,i1) ).
cnf(u3082,axiom,
sF4 = select(sF34,i6) ).
cnf(u1920,axiom,
sF7 = sF44 ).
cnf(u2820,axiom,
sF4 = select(sF21,i1) ).
cnf(u2811,axiom,
( select(sF54,X0) = select(sF62,X0)
| i6 = X0 ) ).
cnf(u2620,axiom,
( select(sF1,X0) = select(sF15,X0)
| i6 = X0 ) ).
cnf(u2953,axiom,
( select(sF1,X0) = select(sF17,X0)
| i6 = X0 ) ).
cnf(u2832,axiom,
sF16 = sF61 ).
cnf(u2438,axiom,
sF4 = select(sF3,i6) ).
cnf(u2883,axiom,
sF16 = sF27 ).
cnf(u2755,axiom,
sF19 = store(sF17,i1,sF4) ).
cnf(u2882,axiom,
sF16 = select(sF23,i6) ).
cnf(u2462,axiom,
( select(sF62,X0) = select(sF65,X0)
| i6 = X0 ) ).
cnf(u2576,axiom,
sF15 = store(sF13,i6,sF4) ).
cnf(u2443,axiom,
sF4 = sF45 ).
cnf(u2891,axiom,
sF16 = select(sF28,i6) ).
cnf(u2886,axiom,
sF16 = sF24 ).
cnf(u3029,axiom,
sF4 = select(sF73,i6) ).
cnf(u2056,axiom,
sF4 = select(sF11,i6) ).
cnf(u3018,axiom,
sF4 = sF70 ).
cnf(u37,axiom,
select(sF15,i1) = sF16 ).
cnf(u2561,axiom,
( select(a1,X0) = select(sF1,X0)
| i6 = X0 ) ).
cnf(u3092,axiom,
sF4 = select(sF25,i1) ).
cnf(u2567,axiom,
sF1 = store(a1,i6,sF4) ).
cnf(u3086,axiom,
sF4 = select(sF32,i6) ).
cnf(u2541,axiom,
sF15 = sF52 ).
cnf(u2880,axiom,
sF16 = select(sF19,i6) ).
cnf(u3081,axiom,
sF4 = sF31 ).
cnf(u2853,axiom,
sF63 = store(sF62,i6,sF16) ).
cnf(u3014,axiom,
sF4 = select(sF65,i1) ).
cnf(u2817,axiom,
sF56 = store(sF54,i6,sF16) ).
cnf(u2042,axiom,
( select(sF19,X0) = select(sF21,X0)
| i6 = X0 ) ).
cnf(u3011,axiom,
sF4 = sF64 ).
cnf(u1899,axiom,
sF3 = sF40 ).
cnf(u2983,axiom,
( select(sF25,X0) = select(sF28,X0)
| i1 = X0
| i6 = X0 ) ).
cnf(u2752,axiom,
i6 != i1 ).
cnf(u2565,axiom,
sF4 = select(a1,i6) ).
cnf(u2852,axiom,
sF16 = select(sF62,i6) ).
cnf(u2365,axiom,
( select(sF28,X0) = select(sF30,X0)
| i6 = X0 ) ).
cnf(u2052,axiom,
sF4 = sF14 ).
cnf(u2611,axiom,
sF17 = store(sF15,i6,sF16) ).
cnf(u220,axiom,
( select(sF17,X0) = select(sF19,X0)
| i1 = X0 ) ).
cnf(u2792,axiom,
( select(sF69,X0) = select(sF75,X0)
| i6 = X0 ) ).
cnf(u213,axiom,
( select(sF3,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u2619,axiom,
( select(sF28,X0) = select(sF36,X0)
| i6 = X0 ) ).
cnf(u2385,axiom,
i6 = i0 ).
cnf(u2471,axiom,
sF4 = sF12 ).
cnf(u2604,axiom,
( select(sF1,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u2813,axiom,
sF58 = store(sF56,i6,sF16) ).
cnf(u3089,axiom,
sF4 = select(sF36,i6) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV531-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.21 % Computer : n014.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Mon Sep 28 11:34:31 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.27 Running first-order theorem proving
% 0.20/0.27 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
% 4.40/2.99 % (1724518)Input is clausal, will run a generic CNF schedule.
% 4.40/2.99 % (1724526)lrs+10_1_sil=8000:sp=occurrence:random_seed=853611964:i=107:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/107Mi)
% 4.40/2.99 % (1724526)Instruction limit reached!
% 4.40/2.99 % (1724526)------------------------------
% 4.40/2.99 % (1724526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.40/2.99 % (1724526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/2.99 % (1724526)CaDiCaL version: 2.1.3
% 4.40/2.99 % (1724526)Termination reason: Instruction limit
% 4.40/2.99 % (1724526)Termination phase: Property scanning
% 4.40/2.99 % (1724526)Time elapsed: 0.023 s
% 4.40/2.99 % (1724526)Peak memory usage: 84 MB
% 4.40/2.99 % (1724526)Instructions burned: 110 (million)
% 4.40/2.99 % (1724525)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1428833483:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2986 on theBenchmark for (2986ds/137899Mi)
% 4.40/2.99 % (1724528)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3588445121:s2a=on:i=180:gtg=position_2986 on theBenchmark for (2986ds/180Mi)
% 4.40/2.99 % (1724529)dis-21_1_sil=8000:lcm=predicate:random_seed=3542691562: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)
% 4.40/2.99 % (1724524)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=685690748:i=132376:av=off_2986 on theBenchmark for (2986ds/132376Mi)
% 4.40/2.99 % (1724523)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=2475509521:i=140167_2986 on theBenchmark for (2986ds/140167Mi)
% 4.40/2.99 % (1724527)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1740709786:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/114Mi)
% 4.40/2.99 % (1724527)Instruction limit reached!
% 4.40/2.99 % (1724527)------------------------------
% 4.40/2.99 % (1724527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.40/2.99 % (1724527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/2.99 % (1724527)CaDiCaL version: 2.1.3
% 4.40/2.99 % (1724527)Termination reason: Instruction limit
% 4.40/2.99 % (1724527)Termination phase: Property scanning
% 4.40/2.99 % (1724527)Time elapsed: 0.044 s
% 4.40/2.99 % (1724527)Peak memory usage: 84 MB
% 4.40/2.99 % (1724527)Instructions burned: 115 (million)
% 4.40/2.99 % (1724529)Instruction limit reached!
% 4.40/2.99 % (1724529)------------------------------
% 4.40/2.99 % (1724529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.40/2.99 % (1724529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/2.99 % (1724529)CaDiCaL version: 2.1.3
% 4.40/2.99 % (1724529)Termination reason: Instruction limit
% 4.40/2.99 % (1724529)Termination phase: Property scanning
% 4.40/2.99 % (1724529)Time elapsed: 0.051 s
% 4.40/2.99 % (1724529)Peak memory usage: 84 MB
% 4.40/2.99 % (1724529)Instructions burned: 119 (million)
% 4.40/2.99 % (1724528)Instruction limit reached!
% 4.40/2.99 % (1724528)------------------------------
% 4.40/2.99 % (1724528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.40/2.99 % (1724528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/2.99 % (1724528)CaDiCaL version: 2.1.3
% 4.40/2.99 % (1724528)Termination reason: Instruction limit
% 4.40/2.99 % (1724528)Termination phase: Property scanning
% 4.40/2.99 % (1724528)Time elapsed: 0.058 s
% 4.40/2.99 % (1724528)Peak memory usage: 84 MB
% 4.40/2.99 % (1724528)Instructions burned: 182 (million)
% 4.40/2.99 % (1724531)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=2799882652:i=143:sd=2:aac=none:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/143Mi)
% 4.40/2.99 % (1724531)Instruction limit reached!
% 4.40/2.99 % (1724531)------------------------------
% 4.40/2.99 % (1724531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.40/2.99 % (1724531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/2.99 % (1724531)CaDiCaL version: 2.1.3
% 4.40/2.99 % (1724531)Termination reason: Instruction limit
% 4.40/2.99 % (1724531)Termination phase: Property scanning
% 4.40/2.99 % (1724531)Time elapsed: 0.029 s
% 4.40/2.99 % (1724531)Peak memory usage: 84 MB
% 4.40/2.99 % (1724531)Instructions burned: 146 (million)
% 12.67/3.76 % (1724538)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3056723524: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)
% 12.67/3.76 % (1724539)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=418603336:st=4:i=219:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/219Mi)
% 12.67/3.76 % (1724542)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=959820099:avsq=on:i=194:fgj=on:bd=preordered_2984 on theBenchmark for (2984ds/194Mi)
% 12.67/3.76 % (1724541)lrs+10_64_to=lpo:sil=8000:random_seed=562511578:i=126:bd=preordered_2984 on theBenchmark for (2984ds/126Mi)
% 12.67/3.76 % (1724542)Instruction limit reached!
% 12.67/3.76 % (1724542)------------------------------
% 12.67/3.76 % (1724542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.76 % (1724542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.76 % (1724542)CaDiCaL version: 2.1.3
% 12.67/3.76 % (1724542)Termination reason: Instruction limit
% 12.67/3.76 % (1724542)Termination phase: Saturation
% 12.67/3.76 % (1724542)Time elapsed: 0.046 s
% 12.67/3.76 % (1724542)Peak memory usage: 103 MB
% 12.67/3.76 % (1724542)Instructions burned: 197 (million)
% 12.67/3.76 % (1724541)Instruction limit reached!
% 12.67/3.76 % (1724541)------------------------------
% 12.67/3.76 % (1724541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.76 % (1724541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.76 % (1724541)CaDiCaL version: 2.1.3
% 12.67/3.76 % (1724541)Termination reason: Instruction limit
% 12.67/3.76 % (1724541)Termination phase: Saturation
% 12.67/3.76 % (1724541)Time elapsed: 0.058 s
% 12.67/3.76 % (1724541)Peak memory usage: 99 MB
% 12.67/3.76 % (1724541)Instructions burned: 128 (million)
% 12.67/3.76 % (1724538)Instruction limit reached!
% 12.67/3.76 % (1724538)------------------------------
% 12.67/3.76 % (1724538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.76 % (1724538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.76 % (1724538)CaDiCaL version: 2.1.3
% 12.67/3.76 % (1724538)Termination reason: Instruction limit
% 12.67/3.76 % (1724538)Termination phase: SInE selection
% 12.67/3.76 % (1724538)Time elapsed: 0.074 s
% 12.67/3.76 % (1724538)Peak memory usage: 83 MB
% 12.67/3.76 % (1724538)Instructions burned: 191 (million)
% 12.67/3.76 % (1724539)Instruction limit reached!
% 12.67/3.76 % (1724539)------------------------------
% 12.67/3.76 % (1724539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.76 % (1724539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.76 % (1724539)CaDiCaL version: 2.1.3
% 12.67/3.76 % (1724539)Termination reason: Instruction limit
% 12.67/3.76 % (1724539)Termination phase: Property scanning
% 12.67/3.76 % (1724539)Time elapsed: 0.078 s
% 12.67/3.76 % (1724539)Peak memory usage: 84 MB
% 12.67/3.76 % (1724539)Instructions burned: 222 (million)
% 12.67/3.76 % (1724547)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1175389526:i=157:gtg=all_2983 on theBenchmark for (2983ds/157Mi)
% 12.67/3.76 % (1724547)Instruction limit reached!
% 12.67/3.76 % (1724547)------------------------------
% 12.67/3.76 % (1724547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.76 % (1724547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.76 % (1724547)CaDiCaL version: 2.1.3
% 12.67/3.76 % (1724547)Termination reason: Instruction limit
% 12.67/3.76 % (1724547)Termination phase: Property scanning
% 12.67/3.76 % (1724547)Time elapsed: 0.027 s
% 12.67/3.76 % (1724547)Peak memory usage: 84 MB
% 12.67/3.76 % (1724547)Instructions burned: 158 (million)
% 12.67/3.76 % (1724548)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4083649566:i=3394:sd=4:ss=included:sgt=64_2983 on theBenchmark for (2983ds/3394Mi)
% 12.67/3.76 % (1724550)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4251717922:i=107_2982 on theBenchmark for (2982ds/107Mi)
% 12.67/3.76 % (1724549)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=1886900422:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2983 on theBenchmark for (2983ds/106Mi)
% 12.67/3.76 % (1724549)Instruction limit reached!
% 12.67/3.76 % (1724549)------------------------------
% 12.67/3.76 % (1724549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.51/4.51 % (1724549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.51/4.51 % (1724549)CaDiCaL version: 2.1.3
% 18.51/4.51 % (1724549)Termination reason: Instruction limit
% 18.51/4.51 % (1724549)Termination phase: SInE selection
% 18.51/4.51 % (1724549)Time elapsed: 0.041 s
% 18.51/4.51 % (1724549)Peak memory usage: 83 MB
% 18.51/4.51 % (1724549)Instructions burned: 107 (million)
% 18.51/4.51 % (1724552)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3023116297:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2982 on theBenchmark for (2982ds/242Mi)
% 18.51/4.51 % (1724552)Instruction limit reached!
% 18.51/4.51 % (1724552)------------------------------
% 18.51/4.51 % (1724552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.51/4.51 % (1724552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.51/4.51 % (1724552)CaDiCaL version: 2.1.3
% 18.51/4.51 % (1724552)Termination reason: Instruction limit
% 18.51/4.51 % (1724552)Termination phase: Property scanning
% 18.51/4.51 % (1724552)Time elapsed: 0.042 s
% 18.51/4.51 % (1724552)Peak memory usage: 84 MB
% 18.51/4.51 % (1724552)Instructions burned: 247 (million)
% 18.51/4.51 % (1724550)Instruction limit reached!
% 18.51/4.51 % (1724550)------------------------------
% 18.51/4.51 % (1724550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.51/4.51 % (1724550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.51/4.51 % (1724550)CaDiCaL version: 2.1.3
% 18.51/4.51 % (1724550)Termination reason: Instruction limit
% 18.51/4.51 % (1724550)Termination phase: Saturation
% 18.51/4.51 % (1724550)Time elapsed: 0.125 s
% 18.51/4.51 % (1724550)Peak memory usage: 147 MB
% 18.51/4.51 % (1724550)Instructions burned: 107 (million)
% 18.51/4.51 % (1724557)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3997829471:cond=fast:i=5208:av=off_2981 on theBenchmark for (2981ds/5208Mi)
% 18.51/4.51 % (1724558)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2420613670:i=134:sd=2:doe=on:ss=axioms:sgt=14_2980 on theBenchmark for (2980ds/134Mi)
% 18.51/4.51 % (1724558)Instruction limit reached!
% 18.51/4.51 % (1724558)------------------------------
% 18.51/4.51 % (1724558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.51/4.51 % (1724558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.51/4.51 % (1724558)CaDiCaL version: 2.1.3
% 18.51/4.51 % (1724558)Termination reason: Instruction limit
% 18.51/4.51 % (1724558)Termination phase: Property scanning
% 18.51/4.51 % (1724558)Time elapsed: 0.027 s
% 18.51/4.51 % (1724558)Peak memory usage: 84 MB
% 18.51/4.51 % (1724558)Instructions burned: 139 (million)
% 18.51/4.51 % (1724559)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3901575702:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 18.51/4.51 % (1724562)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2361050921:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 18.51/4.51 % (1724562)Instruction limit reached!
% 18.51/4.51 % (1724562)------------------------------
% 18.51/4.51 % (1724562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.51/4.51 % (1724562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.51/4.51 % (1724562)CaDiCaL version: 2.1.3
% 18.51/4.51 % (1724562)Termination reason: Instruction limit
% 18.51/4.51 % (1724562)Termination phase: Saturation
% 18.51/4.51 % (1724562)Time elapsed: 0.046 s
% 18.51/4.51 % (1724562)Peak memory usage: 103 MB
% 18.51/4.51 % (1724562)Instructions burned: 196 (million)
% 18.51/4.51 % (1724565)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3324516467:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 18.51/4.51 % (1724559)Instruction limit reached!
% 18.51/4.51 % (1724559)------------------------------
% 18.51/4.51 % (1724559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.51/4.51 % (1724559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.51/4.51 % (1724559)CaDiCaL version: 2.1.3
% 18.51/4.51 % (1724559)Termination reason: Instruction limit
% 18.51/4.51 % (1724559)Termination phase: Saturation
% 18.51/4.51 % (1724559)Time elapsed: 0.206 s
% 18.51/4.51 % (1724559)Peak memory usage: 118 MB
% 18.51/4.51 % (1724559)Instructions burned: 499 (million)
% 24.15/5.29 % (1724565)Instruction limit reached!
% 24.15/5.29 % (1724565)------------------------------
% 24.15/5.29 % (1724565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/5.29 % (1724565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/5.29 % (1724565)CaDiCaL version: 2.1.3
% 24.15/5.29 % (1724565)Termination reason: Instruction limit
% 24.15/5.29 % (1724565)Termination phase: Saturation
% 24.15/5.29 % (1724565)Time elapsed: 0.068 s
% 24.15/5.29 % (1724565)Peak memory usage: 108 MB
% 24.15/5.29 % (1724565)Instructions burned: 266 (million)
% 24.15/5.29 % (1724568)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=476048588:i=3256:kws=precedence:bd=preordered:av=off_2976 on theBenchmark for (2976ds/3256Mi)
% 24.15/5.29 % (1724567)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1110864259:cond=on:i=156:bs=on:gtg=exists_all:er=known_2977 on theBenchmark for (2977ds/156Mi)
% 24.15/5.29 % (1724567)Instruction limit reached!
% 24.15/5.29 % (1724567)------------------------------
% 24.15/5.29 % (1724567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/5.29 % (1724567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/5.29 % (1724567)CaDiCaL version: 2.1.3
% 24.15/5.29 % (1724567)Termination reason: Instruction limit
% 24.15/5.29 % (1724567)Termination phase: Property scanning
% 24.15/5.29 % (1724567)Time elapsed: 0.050 s
% 24.15/5.29 % (1724567)Peak memory usage: 84 MB
% 24.15/5.29 % (1724567)Instructions burned: 157 (million)
% 24.15/5.29 % (1724571)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4119729149:i=537:av=off:ss=included_2975 on theBenchmark for (2975ds/537Mi)
% 24.15/5.29 % (1724523)Refutation not found, incomplete strategy
% 24.15/5.29 % (1724523)------------------------------
% 24.15/5.29 % (1724523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/5.29 % (1724523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/5.29 % (1724523)CaDiCaL version: 2.1.3
% 24.15/5.29 % (1724523)Termination reason: Refutation not found, incomplete strategy
% 24.15/5.29 % (1724523)Time elapsed: 1.184 s
% 24.15/5.29 % (1724523)Peak memory usage: 135 MB
% 24.15/5.29 % (1724523)Instructions burned: 2169 (million)
% 24.15/5.29 % (1724571)Instruction limit reached!
% 24.15/5.29 % (1724571)------------------------------
% 24.15/5.29 % (1724571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/5.29 % (1724571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/5.29 % (1724571)CaDiCaL version: 2.1.3
% 24.15/5.29 % (1724571)Termination reason: Instruction limit
% 24.15/5.29 % (1724571)Termination phase: Property scanning
% 24.15/5.29 % (1724571)Time elapsed: 0.192 s
% 24.15/5.29 % (1724571)Peak memory usage: 84 MB
% 24.15/5.29 % (1724571)Instructions burned: 540 (million)
% 24.15/5.29 % (1724523)------------------------------
% 24.15/5.29 % (1724523)------------------------------
% 24.15/5.29 % (1724573)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2065728980:i=180:bd=preordered:av=off_2972 on theBenchmark for (2972ds/180Mi)
% 24.15/5.29 % (1724557)Refutation not found, incomplete strategy
% 24.15/5.29 % (1724557)------------------------------
% 24.15/5.29 % (1724557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/5.29 % (1724557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/5.29 % (1724557)CaDiCaL version: 2.1.3
% 24.15/5.29 % (1724557)Termination reason: Refutation not found, incomplete strategy
% 24.15/5.29 % (1724557)Time elapsed: 0.981 s
% 24.15/5.29 % (1724557)Peak memory usage: 133 MB
% 24.15/5.29 % (1724557)Instructions burned: 2061 (million)
% 24.15/5.29 % (1724573)Instruction limit reached!
% 24.15/5.29 % (1724573)------------------------------
% 24.15/5.29 % (1724573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/5.29 % (1724573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/5.29 % (1724573)CaDiCaL version: 2.1.3
% 24.15/5.29 % (1724573)Termination reason: Instruction limit
% 24.15/5.29 % (1724573)Termination phase: Saturation
% 24.15/5.29 % (1724573)Time elapsed: 0.081 s
% 24.15/5.29 % (1724573)Peak memory usage: 102 MB
% 24.15/5.29 % (1724573)Instructions burned: 181 (million)
% 24.15/5.29 % (1724574)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=1189312400:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/10307Mi)
% 24.80/5.37 % (1724557)------------------------------
% 24.80/5.37 % (1724557)------------------------------
% 24.80/5.37 % (1724525)Refutation not found, incomplete strategy
% 24.80/5.37 % (1724525)------------------------------
% 24.80/5.37 % (1724525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724525)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724525)Termination reason: Refutation not found, incomplete strategy
% 24.80/5.37 % (1724525)Time elapsed: 1.701 s
% 24.80/5.37 % (1724525)Peak memory usage: 138 MB
% 24.80/5.37 % (1724525)Instructions burned: 3283 (million)
% 24.80/5.37 % (1724576)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=2940757571:i=412:gtgl=4:gtg=exists_all_2969 on theBenchmark for (2969ds/412Mi)
% 24.80/5.37 % (1724578)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=1481861679:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 24.80/5.37 % (1724576)Instruction limit reached!
% 24.80/5.37 % (1724576)------------------------------
% 24.80/5.37 % (1724576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724576)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724576)Termination reason: Instruction limit
% 24.80/5.37 % (1724576)Termination phase: Property scanning
% 24.80/5.37 % (1724576)Time elapsed: 0.134 s
% 24.80/5.37 % (1724576)Peak memory usage: 84 MB
% 24.80/5.37 % (1724576)Instructions burned: 419 (million)
% 24.80/5.37 % (1724525)------------------------------
% 24.80/5.37 % (1724525)------------------------------
% 24.80/5.37 % (1724581)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=2936145114:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2967 on theBenchmark for (2967ds/303Mi)
% 24.80/5.37 % (1724581)Instruction limit reached!
% 24.80/5.37 % (1724581)------------------------------
% 24.80/5.37 % (1724581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724581)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724581)Termination reason: Instruction limit
% 24.80/5.37 % (1724581)Termination phase: Property scanning
% 24.80/5.37 % (1724581)Time elapsed: 0.113 s
% 24.80/5.37 % (1724581)Peak memory usage: 84 MB
% 24.80/5.37 % (1724581)Instructions burned: 306 (million)
% 24.80/5.37 % (1724582)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=315043640:st=4:i=720:sd=3:fsr=off:ss=axioms_2965 on theBenchmark for (2965ds/720Mi)
% 24.80/5.37 % (1724568)Instruction limit reached!
% 24.80/5.37 % (1724568)------------------------------
% 24.80/5.37 % (1724568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724568)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724568)Termination reason: Instruction limit
% 24.80/5.37 % (1724568)Termination phase: Saturation
% 24.80/5.37 % (1724568)Time elapsed: 1.205 s
% 24.80/5.37 % (1724568)Peak memory usage: 220 MB
% 24.80/5.37 % (1724568)Instructions burned: 3258 (million)
% 24.80/5.37 % (1724584)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2416372039:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 24.80/5.37 % (1724586)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1683432005:i=2989:sd=3:ss=axioms:sgt=60_2963 on theBenchmark for (2963ds/2989Mi)
% 24.80/5.37 % (1724582)Instruction limit reached!
% 24.80/5.37 % (1724582)------------------------------
% 24.80/5.37 % (1724582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724582)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724582)Termination reason: Instruction limit
% 24.80/5.37 % (1724582)Termination phase: Property scanning
% 24.80/5.37 % (1724582)Time elapsed: 0.238 s
% 24.80/5.37 % (1724582)Peak memory usage: 84 MB
% 24.80/5.37 % (1724582)Instructions burned: 721 (million)
% 24.80/5.37 % (1724578)Refutation not found, incomplete strategy
% 24.80/5.37 % (1724578)------------------------------
% 24.80/5.37 % (1724578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724578)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724578)Termination reason: Refutation not found, incomplete strategy
% 24.80/5.37 % (1724578)Time elapsed: 0.670 s
% 24.80/5.37 % (1724578)Peak memory usage: 136 MB
% 24.80/5.37 % (1724578)Instructions burned: 2209 (million)
% 24.80/5.37 % (1724584)Instruction limit reached!
% 24.80/5.37 % (1724584)------------------------------
% 24.80/5.37 % (1724584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724584)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724584)Termination reason: Instruction limit
% 24.80/5.37 % (1724584)Termination phase: Property scanning
% 24.80/5.37 % (1724584)Time elapsed: 0.201 s
% 24.80/5.37 % (1724584)Peak memory usage: 84 MB
% 24.80/5.37 % (1724584)Instructions burned: 604 (million)
% 24.80/5.37 % (1724589)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=1132250246:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2961 on theBenchmark for (2961ds/1997Mi)
% 24.80/5.37 % (1724590)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=3113012580:i=2088:bd=preordered:av=off_2961 on theBenchmark for (2961ds/2088Mi)
% 24.80/5.37 % (1724578)------------------------------
% 24.80/5.37 % (1724578)------------------------------
% 24.80/5.37 % (1724593)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3655377651:i=1098:nicw=on_2959 on theBenchmark for (2959ds/1098Mi)
% 24.80/5.37 % (1724574)First to succeed.
% 24.80/5.37 % (1724574)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1724518"
% 24.80/5.37 % (1724593)Instruction limit reached!
% 24.80/5.37 % (1724593)------------------------------
% 24.80/5.37 % (1724593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724593)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724593)Termination reason: Instruction limit
% 24.80/5.37 % (1724593)Termination phase: Saturation
% 24.80/5.37 % (1724593)Time elapsed: 0.278 s
% 24.80/5.37 % (1724593)Peak memory usage: 148 MB
% 24.80/5.37 % (1724593)Instructions burned: 1098 (million)
% 24.80/5.37 % (1724595)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2310492115:i=433:bd=preordered_2955 on theBenchmark for (2955ds/433Mi)
% 24.80/5.37 % (1724595)Refutation not found, incomplete strategy
% 24.80/5.37 % (1724595)------------------------------
% 24.80/5.37 % (1724595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724595)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724595)Termination reason: Refutation not found, incomplete strategy
% 24.80/5.37 % (1724595)Time elapsed: 0.045 s
% 24.80/5.37 % (1724595)Peak memory usage: 91 MB
% 24.80/5.37 % (1724595)Instructions burned: 208 (million)
% 24.80/5.37 % (1724589)Instruction limit reached!
% 24.80/5.37 % (1724589)------------------------------
% 24.80/5.37 % (1724589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724589)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724589)Termination reason: Instruction limit
% 24.80/5.37 % (1724589)Termination phase: Property scanning
% 24.80/5.37 % (1724589)Time elapsed: 0.644 s
% 24.80/5.37 % (1724589)Peak memory usage: 84 MB
% 24.80/5.37 % (1724589)Instructions burned: 1998 (million)
% 24.80/5.37 % (1724548)Instruction limit reached!
% 24.80/5.37 % (1724548)------------------------------
% 24.80/5.37 % (1724548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/5.37 % (1724548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/5.37 % (1724548)CaDiCaL version: 2.1.3
% 24.80/5.37 % (1724548)Termination reason: Instruction limit
% 24.80/5.37 % (1724548)Termination phase: Saturation
% 24.80/5.37 % (1724548)Time elapsed: 2.773 s
% 25.54/5.58 % (1724548)Peak memory usage: 155 MB
% 25.54/5.58 % (1724548)Instructions burned: 3394 (million)
% 25.54/5.58 % SZS status Satisfiable for theBenchmark
% 25.54/5.58 % SZS output start Saturation.
% See solution above
% 25.54/5.58 % SZS output start Definitions and Model Updates.
% 25.54/5.58 % SZS output end Definitions and Model Updates.
% 25.54/5.58 % (1724574)------------------------------
% 25.54/5.58 % (1724574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.54/5.58 % (1724574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.54/5.58 % (1724574)CaDiCaL version: 2.1.3
% 25.54/5.58 % (1724574)Termination reason: Satisfiable
% 25.54/5.58 % (1724574)Time elapsed: 1.334 s
% 25.54/5.58 % (1724574)Peak memory usage: 137 MB
% 25.54/5.58 % (1724574)Instructions burned: 2475 (million)
% 25.54/5.58 % (1724574)------------------------------
% 25.54/5.58 % (1724574)------------------------------
% 25.54/5.58 % (1724518)Success in time 4.668 s
% 25.54/5.58 % Vampire exiting
%------------------------------------------------------------------------------