%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV550-1.007 : 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 : n020.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:17:57 PM UTC 2026
% Result : Satisfiable 5.97s 1.65s
% Output : Saturation 7.53s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u65,negated_conjecture,
a1 != a2 ).
cnf(u70,negated_conjecture,
sF25 = sF27 ).
cnf(u75,axiom,
select(a2,i1) = sF0 ).
cnf(u80,axiom,
store(a1,i1,sF0) = sF1 ).
cnf(u85,axiom,
select(a1,i1) = sF2 ).
cnf(u90,axiom,
store(a2,i1,sF2) = sF3 ).
cnf(u95,axiom,
select(sF3,i2) = sF4 ).
cnf(u100,axiom,
store(sF1,i2,sF4) = sF5 ).
cnf(u105,axiom,
select(sF1,i2) = sF6 ).
cnf(u110,axiom,
store(sF3,i2,sF6) = sF7 ).
cnf(u115,axiom,
select(sF7,i3) = sF8 ).
cnf(u120,axiom,
store(sF5,i3,sF8) = sF9 ).
cnf(u125,axiom,
select(sF5,i3) = sF10 ).
cnf(u130,axiom,
store(sF7,i3,sF10) = sF11 ).
cnf(u135,axiom,
select(sF11,i4) = sF12 ).
cnf(u140,axiom,
store(sF9,i4,sF12) = sF13 ).
cnf(u145,axiom,
select(sF9,i4) = sF14 ).
cnf(u150,axiom,
store(sF11,i4,sF14) = sF15 ).
cnf(u155,axiom,
select(sF15,i5) = sF16 ).
cnf(u160,axiom,
store(sF13,i5,sF16) = sF17 ).
cnf(u165,axiom,
select(sF13,i5) = sF18 ).
cnf(u170,axiom,
store(sF15,i5,sF18) = sF19 ).
cnf(u175,axiom,
select(sF19,i6) = sF20 ).
cnf(u180,axiom,
store(sF17,i6,sF20) = sF21 ).
cnf(u185,axiom,
select(sF17,i6) = sF22 ).
cnf(u190,axiom,
store(sF19,i6,sF22) = sF23 ).
cnf(u195,axiom,
select(sF23,i7) = sF24 ).
cnf(u200,axiom,
store(sF21,i1,sF24) = sF25 ).
cnf(u205,axiom,
select(sF21,i7) = sF26 ).
cnf(u210,axiom,
store(sF23,i7,sF26) = sF27 ).
cnf(u216,negated_conjecture,
sF25 = store(sF23,i7,sF26) ).
cnf(u235,negated_conjecture,
sF26 = select(sF25,i7) ).
cnf(u240,axiom,
sF24 = select(sF25,i1) ).
cnf(u245,axiom,
sF22 = select(sF23,i6) ).
cnf(u250,axiom,
sF20 = select(sF21,i6) ).
cnf(u255,axiom,
sF18 = select(sF19,i5) ).
cnf(u260,axiom,
sF16 = select(sF17,i5) ).
cnf(u265,axiom,
sF14 = select(sF15,i4) ).
cnf(u270,axiom,
sF12 = select(sF13,i4) ).
cnf(u275,axiom,
sF10 = select(sF11,i3) ).
cnf(u280,axiom,
sF8 = select(sF9,i3) ).
cnf(u285,axiom,
sF6 = select(sF7,i2) ).
cnf(u290,axiom,
sF4 = select(sF5,i2) ).
cnf(u295,axiom,
sF2 = select(sF3,i1) ).
cnf(u300,axiom,
sF0 = select(sF1,i1) ).
cnf(u321,negated_conjecture,
i1 = i7 ).
cnf(u325,negated_conjecture,
sF24 = select(sF23,i1) ).
cnf(u332,axiom,
i1 != i2 ).
cnf(u337,axiom,
sF6 = select(a1,i2) ).
cnf(u350,axiom,
sF4 != select(sF5,i1) ).
cnf(u355,axiom,
sF6 != select(sF7,i1) ).
cnf(u360,axiom,
sF7 != store(sF3,i1,sF6) ).
cnf(u366,axiom,
sF5 != store(sF1,i1,sF4) ).
cnf(u372,axiom,
sF0 != sF6 ).
cnf(u377,axiom,
sF2 != sF4 ).
cnf(u385,axiom,
sF4 = select(a2,i2) ).
cnf(u391,axiom,
i2 != i3 ).
cnf(u396,axiom,
sF10 = select(sF1,i3) ).
cnf(u409,axiom,
sF8 != select(sF9,i2) ).
cnf(u414,axiom,
sF10 != select(sF11,i2) ).
cnf(u419,axiom,
sF11 != store(sF7,i2,sF10) ).
cnf(u425,axiom,
sF9 != store(sF5,i2,sF8) ).
cnf(u431,axiom,
sF4 != sF10 ).
cnf(u436,axiom,
sF6 != sF8 ).
cnf(u444,axiom,
sF8 = select(sF3,i3) ).
cnf(u455,axiom,
sF14 = select(sF5,i4) ).
cnf(u469,axiom,
i3 != i4 ).
cnf(u475,axiom,
sF6 != select(sF3,i3) ).
cnf(u486,axiom,
sF12 = select(sF7,i4) ).
cnf(u532,axiom,
i4 != i5 ).
cnf(u537,axiom,
sF18 = select(sF9,i5) ).
cnf(u551,axiom,
sF16 = select(sF17,i4) ).
cnf(u556,axiom,
sF18 = select(sF19,i4) ).
cnf(u560,axiom,
sF19 != store(sF15,i4,sF18) ).
cnf(u566,axiom,
sF17 != store(sF13,i4,sF16) ).
cnf(u573,axiom,
sF12 = sF18 ).
cnf(u578,axiom,
sF14 = sF16 ).
cnf(u585,axiom,
sF16 = select(sF11,i5) ).
cnf(u596,axiom,
sF22 = select(sF13,i6) ).
cnf(u611,axiom,
i5 = i6 ).
cnf(u617,axiom,
sF14 = select(sF11,i5) ).
cnf(u627,axiom,
sF20 = select(sF15,i6) ).
cnf(u639,axiom,
sF20 = select(sF21,i5) ).
cnf(u644,axiom,
sF22 = select(sF23,i5) ).
cnf(u649,axiom,
sF23 = store(sF19,i5,sF22) ).
cnf(u655,axiom,
sF21 = store(sF17,i5,sF20) ).
cnf(u661,axiom,
sF16 = sF22 ).
cnf(u667,axiom,
sF12 = sF20 ).
cnf(u674,axiom,
i6 = i7 ).
cnf(u678,axiom,
sF26 = select(sF17,i7) ).
cnf(u688,negated_conjecture,
i1 = i6 ).
cnf(u692,negated_conjecture,
sF24 = select(sF19,i1) ).
cnf(u703,negated_conjecture,
sF25 = store(sF23,i1,sF26) ).
cnf(u708,negated_conjecture,
sF26 = select(sF21,i1) ).
cnf(u714,negated_conjecture,
sF24 = sF26 ).
cnf(u735,negated_conjecture,
i1 = i5 ).
cnf(u741,negated_conjecture,
sF20 = select(sF21,i1) ).
cnf(u746,negated_conjecture,
sF22 = select(sF23,i1) ).
cnf(u751,negated_conjecture,
sF23 = store(sF19,i1,sF22) ).
cnf(u756,negated_conjecture,
sF22 = select(sF17,i1) ).
cnf(u761,negated_conjecture,
sF21 = store(sF17,i1,sF20) ).
cnf(u766,negated_conjecture,
sF20 = select(sF19,i1) ).
cnf(u781,negated_conjecture,
sF24 = select(sF17,i1) ).
cnf(u789,negated_conjecture,
sF22 = sF24 ).
cnf(u795,negated_conjecture,
sF25 = store(sF21,i1,sF22) ).
cnf(u820,negated_conjecture,
sF25 = store(sF23,i1,sF22) ).
cnf(u831,negated_conjecture,
sF22 = select(sF15,i1) ).
cnf(u840,axiom,
i1 = i3 ).
cnf(u858,negated_conjecture,
sF20 = sF26 ).
cnf(u865,axiom,
sF14 = select(sF1,i4) ).
cnf(u875,negated_conjecture,
sF20 = sF24 ).
cnf(u880,negated_conjecture,
sF25 = store(sF23,i1,sF20) ).
cnf(u887,axiom,
sF12 = select(sF3,i4) ).
cnf(u896,negated_conjecture,
sF25 = store(sF21,i1,sF20) ).
cnf(u901,negated_conjecture,
sF20 = sF22 ).
cnf(u914,negated_conjecture,
sF12 = select(sF5,i5) ).
cnf(u921,negated_conjecture,
sF23 = store(sF19,i1,sF20) ).
cnf(u932,negated_conjecture,
sF16 = select(sF7,i5) ).
cnf(u938,negated_conjecture,
i2 != i5 ).
cnf(u943,negated_conjecture,
sF12 = select(sF1,i5) ).
cnf(u950,axiom,
sF4 = select(sF11,i2) ).
cnf(u964,negated_conjecture,
sF20 = select(sF13,i1) ).
cnf(u971,negated_conjecture,
sF20 = select(sF9,i1) ).
cnf(u974,negated_conjecture,
i1 != i4 ).
cnf(u1004,negated_conjecture,
sF12 = select(sF13,i1) ).
cnf(u1009,negated_conjecture,
sF12 = select(sF9,i1) ).
cnf(u1018,negated_conjecture,
sF0 = sF12 ).
cnf(u1023,negated_conjecture,
sF23 = store(sF19,i1,sF12) ).
cnf(u1028,negated_conjecture,
sF12 = select(sF23,i1) ).
cnf(u1070,axiom,
sF18 = sF20 ).
cnf(u1077,negated_conjecture,
sF20 = select(sF23,i1) ).
cnf(u1086,axiom,
sF0 = sF8 ).
cnf(u1098,axiom,
sF2 != select(sF11,i2) ).
cnf(u1116,axiom,
sF0 = sF2 ).
cnf(u1122,negated_conjecture,
sF2 = sF12 ).
cnf(u1132,negated_conjecture,
sF18 = select(sF23,i1) ).
cnf(u1146,negated_conjecture,
sF16 = select(sF11,i1) ).
cnf(u1151,negated_conjecture,
sF18 = select(sF9,i1) ).
cnf(u1157,negated_conjecture,
sF16 = select(sF17,i1) ).
cnf(u1162,negated_conjecture,
sF18 = select(sF19,i1) ).
cnf(u1167,negated_conjecture,
sF19 = store(sF15,i1,sF18) ).
cnf(u1172,negated_conjecture,
sF18 = select(sF13,i1) ).
cnf(u1177,negated_conjecture,
sF17 = store(sF13,i1,sF16) ).
cnf(u1182,negated_conjecture,
sF16 = select(sF15,i1) ).
cnf(u1188,axiom,
sF3 = store(a2,i1,sF0) ).
cnf(u1201,negated_conjecture,
sF16 = sF20 ).
cnf(u1212,negated_conjecture,
sF16 = sF18 ).
cnf(u1219,negated_conjecture,
sF19 = store(sF15,i1,sF16) ).
cnf(u1235,negated_conjecture,
sF0 = sF16 ).
cnf(u1254,negated_conjecture,
sF0 = select(sF7,i1) ).
cnf(u1264,negated_conjecture,
sF21 = store(sF17,i1,sF0) ).
cnf(u1277,negated_conjecture,
sF0 = sF24 ).
cnf(u1287,negated_conjecture,
sF25 = store(sF21,i1,sF0) ).
cnf(u1292,negated_conjecture,
sF0 = sF22 ).
cnf(u1297,negated_conjecture,
sF0 = sF20 ).
cnf(u1310,negated_conjecture,
sF17 = store(sF13,i1,sF0) ).
cnf(u1322,negated_conjecture,
sF0 = select(sF25,i1) ).
cnf(u1334,negated_conjecture,
sF23 = store(sF19,i1,sF0) ).
cnf(u1362,axiom,
sF5 != store(sF1,i2,sF0) ).
cnf(u1374,axiom,
sF11 = store(sF7,i1,sF0) ).
cnf(u1386,negated_conjecture,
sF12 = select(sF5,i1) ).
cnf(u1394,axiom,
sF0 != sF4 ).
cnf(u1404,axiom,
sF0 = sF10 ).
cnf(u1427,negated_conjecture,
sF0 = sF14 ).
cnf(u1469,axiom,
sF0 = select(sF9,i1) ).
cnf(u1474,axiom,
sF0 = select(sF11,i1) ).
cnf(u1480,axiom,
sF0 = select(sF5,i1) ).
cnf(u1485,axiom,
sF9 = store(sF5,i1,sF0) ).
cnf(u1500,negated_conjecture,
sF0 = sF18 ).
cnf(u1512,negated_conjecture,
sF19 = store(sF15,i1,sF0) ).
cnf(u1566,axiom,
sF0 != select(sF9,i2) ).
cnf(u1576,negated_conjecture,
sF0 = select(sF3,i1) ).
cnf(u1593,negated_conjecture,
sF0 = select(sF17,i4) ).
cnf(u1615,negated_conjecture,
sF0 = select(sF19,i4) ).
cnf(u1637,negated_conjecture,
sF14 = select(a1,i4) ).
cnf(u1646,negated_conjecture,
sF12 = select(a2,i4) ).
cnf(u1656,axiom,
sF0 != select(sF7,i2) ).
cnf(u1712,axiom,
sF7 != store(sF3,i2,sF0) ).
cnf(u1735,negated_conjecture,
sF25 = store(sF23,i1,sF0) ).
cnf(u1745,axiom,
sF7 != store(sF3,i1,sF0) ).
cnf(u1757,negated_conjecture,
sF0 = select(sF19,i1) ).
cnf(u1782,axiom,
sF11 != store(sF7,i2,sF0) ).
cnf(u1795,axiom,
sF9 != store(sF5,i2,sF0) ).
cnf(u1807,negated_conjecture,
sF0 = select(sF21,i1) ).
cnf(u1817,negated_conjecture,
sF19 != store(sF15,i4,sF0) ).
cnf(u1850,negated_conjecture,
sF15 = store(sF11,i4,sF0) ).
cnf(u1859,negated_conjecture,
sF0 = select(sF15,i4) ).
cnf(u1869,negated_conjecture,
sF17 != store(sF13,i4,sF0) ).
cnf(u1885,negated_conjecture,
sF0 = sF26 ).
cnf(u2009,axiom,
sF0 != select(sF11,i2) ).
cnf(u2024,negated_conjecture,
sF0 = select(sF23,i1) ).
cnf(u2035,negated_conjecture,
sF13 = store(sF9,i4,sF0) ).
cnf(u2044,negated_conjecture,
sF0 = select(sF13,i4) ).
cnf(u2079,axiom,
sF4 = sF6 ).
cnf(u2092,negated_conjecture,
sF0 = select(sF17,i1) ).
cnf(u2130,axiom,
sF0 != select(sF5,i2) ).
cnf(u2267,negated_conjecture,
sF4 = select(sF9,i2) ).
cnf(u2292,axiom,
sF4 = select(sF7,i2) ).
cnf(u2307,axiom,
sF7 = store(sF3,i2,sF4) ).
cnf(u2312,axiom,
sF7 != store(sF3,i1,sF4) ).
cnf(u1718,negated_conjecture,
( select(sF17,X0) = select(sF21,X0)
| i1 = X0 ) ).
cnf(u313,axiom,
( select(sF19,X0) = select(sF23,X0)
| i6 = X0 ) ).
cnf(u2150,axiom,
( select(sF5,X0) = select(sF9,X0)
| i1 = X0 ) ).
cnf(u1301,negated_conjecture,
( select(sF23,X0) = select(sF25,X0)
| i1 = X0 ) ).
cnf(u302,axiom,
( select(a1,X0) = select(sF1,X0)
| i1 = X0 ) ).
cnf(u305,axiom,
( select(sF3,X0) = select(sF7,X0)
| i2 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u2325,negated_conjecture,
( select(sF5,X0) = select(sF7,X0)
| i1 = X0
| i4 = X0 ) ).
cnf(u309,axiom,
( select(sF11,X0) = select(sF15,X0)
| i4 = X0 ) ).
cnf(u312,axiom,
( select(sF17,X0) = select(sF21,X0)
| i6 = X0 ) ).
cnf(u307,axiom,
( select(sF7,X0) = select(sF11,X0)
| i3 = X0 ) ).
cnf(u2260,negated_conjecture,
( select(sF7,X0) = select(sF9,X0)
| i1 = X0
| i4 = X0 ) ).
cnf(u1936,negated_conjecture,
( select(sF15,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u1343,negated_conjecture,
( select(sF17,X0) = select(sF19,X0)
| i1 = X0 ) ).
cnf(u2146,axiom,
( select(sF7,X0) = select(sF11,X0)
| i1 = X0 ) ).
cnf(u2353,negated_conjecture,
( select(sF1,X0) = select(sF3,X0)
| i2 = X0
| i1 = X0
| i4 = X0 ) ).
cnf(u311,axiom,
( select(sF15,X0) = select(sF19,X0)
| i5 = X0 ) ).
cnf(u1787,negated_conjecture,
( select(sF13,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u304,axiom,
( select(sF1,X0) = select(sF5,X0)
| i2 = X0 ) ).
cnf(u2222,negated_conjecture,
( select(sF11,X0) = select(sF13,X0)
| i4 = X0
| i1 = X0 ) ).
cnf(u811,negated_conjecture,
( select(sF19,X0) = select(sF21,X0)
| i1 = X0 ) ).
cnf(u314,axiom,
( select(sF21,X0) = select(sF25,X0)
| i1 = X0 ) ).
cnf(u303,axiom,
( select(a2,X0) = select(sF3,X0)
| i1 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u306,axiom,
( select(sF5,X0) = select(sF9,X0)
| i3 = X0 ) ).
cnf(u2365,negated_conjecture,
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i4 = X0 ) ).
cnf(u310,axiom,
( select(sF13,X0) = select(sF17,X0)
| i5 = X0 ) ).
cnf(u1751,negated_conjecture,
( select(sF15,X0) = select(sF19,X0)
| i1 = X0 ) ).
cnf(u2338,negated_conjecture,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0
| i1 = X0
| i4 = X0 ) ).
cnf(u774,negated_conjecture,
( select(sF21,X0) = select(sF23,X0)
| i1 = X0 ) ).
cnf(u1706,negated_conjecture,
( select(sF19,X0) = select(sF23,X0)
| i1 = X0 ) ).
cnf(u308,axiom,
( select(sF9,X0) = select(sF13,X0)
| i4 = X0 ) ).
cnf(u315,negated_conjecture,
( select(sF23,X0) = select(sF25,X0)
| i7 = X0 ) ).
cnf(u2248,negated_conjecture,
( select(sF9,X0) = select(sF11,X0)
| i4 = X0
| i1 = X0 ) ).
cnf(u2192,negated_conjecture,
( select(sF13,X0) = select(sF15,X0)
| i1 = X0 ) ).
cnf(u2359,negated_conjecture,
( select(sF1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i4 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV550-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n020.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:45:34 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 5.97/1.65 % (113429)Input is clausal, will run a generic CNF schedule.
% 5.97/1.65 % (113438)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=789006406:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.97/1.65 % (113438)Instruction limit reached!
% 5.97/1.65 % (113438)------------------------------
% 5.97/1.65 % (113438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113438)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113438)Termination reason: Instruction limit
% 5.97/1.65 % (113438)Termination phase: Saturation
% 5.97/1.65 % (113438)Time elapsed: 0.027 s
% 5.97/1.65 % (113438)Peak memory usage: 88 MB
% 5.97/1.65 % (113438)Instructions burned: 116 (million)
% 5.97/1.65 % (113435)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=531486967:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.97/1.65 % (113434)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=4101706716:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.97/1.65 % (113436)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1047534471:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.97/1.65 % (113437)lrs+10_1_sil=8000:sp=occurrence:random_seed=3584560788:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.97/1.65 % (113439)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=723578764:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.97/1.65 % (113440)dis-21_1_sil=8000:lcm=predicate:random_seed=1677460774:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.97/1.65 % (113440)Refutation not found, incomplete strategy
% 5.97/1.65 % (113440)------------------------------
% 5.97/1.65 % (113440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113440)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113440)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.65 % (113440)Time elapsed: 0.002 s
% 5.97/1.65 % (113440)Peak memory usage: 88 MB
% 5.97/1.65 % (113440)Instructions burned: 3 (million)
% 5.97/1.65 % (113437)Instruction limit reached!
% 5.97/1.65 % (113437)------------------------------
% 5.97/1.65 % (113437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113437)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113437)Termination reason: Instruction limit
% 5.97/1.65 % (113437)Termination phase: Saturation
% 5.97/1.65 % (113437)Time elapsed: 0.044 s
% 5.97/1.65 % (113437)Peak memory usage: 88 MB
% 5.97/1.65 % (113437)Instructions burned: 108 (million)
% 5.97/1.65 % (113439)Instruction limit reached!
% 5.97/1.65 % (113439)------------------------------
% 5.97/1.65 % (113439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113439)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113439)Termination reason: Instruction limit
% 5.97/1.65 % (113439)Termination phase: Saturation
% 5.97/1.65 % (113439)Time elapsed: 0.078 s
% 5.97/1.65 % (113439)Peak memory usage: 89 MB
% 5.97/1.65 % (113439)Instructions burned: 180 (million)
% 5.97/1.65 % (113442)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=598003232:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.97/1.65 % (113442)Refutation not found, incomplete strategy
% 5.97/1.65 % (113442)------------------------------
% 5.97/1.65 % (113442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113442)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113442)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.65 % (113442)Time elapsed: 0.025 s
% 5.97/1.65 % (113442)Peak memory usage: 89 MB
% 5.97/1.65 % (113442)Instructions burned: 100 (million)
% 5.97/1.65 % (113449)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=757597867:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.97/1.65 % (113450)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2527725082:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.97/1.65 % (113440)------------------------------
% 5.97/1.65 % (113440)------------------------------
% 5.97/1.65 % (113442)------------------------------
% 5.97/1.65 % (113442)------------------------------
% 5.97/1.65 % (113449)Refutation not found, incomplete strategy
% 5.97/1.65 % (113449)------------------------------
% 5.97/1.65 % (113449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113449)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113449)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.65 % (113449)Time elapsed: 0.079 s
% 5.97/1.65 % (113449)Peak memory usage: 89 MB
% 5.97/1.65 % (113449)Instructions burned: 180 (million)
% 5.97/1.65 % (113450)Instruction limit reached!
% 5.97/1.65 % (113450)------------------------------
% 5.97/1.65 % (113450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113450)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113450)Termination reason: Instruction limit
% 5.97/1.65 % (113450)Termination phase: Saturation
% 5.97/1.65 % (113450)Time elapsed: 0.088 s
% 5.97/1.65 % (113450)Peak memory usage: 89 MB
% 5.97/1.65 % (113450)Instructions burned: 220 (million)
% 5.97/1.65 % (113454)lrs+10_64_to=lpo:sil=8000:random_seed=2105112881:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.97/1.65 % (113455)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1965335337:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.97/1.65 % (113454)Instruction limit reached!
% 5.97/1.65 % (113454)------------------------------
% 5.97/1.65 % (113454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113454)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113454)Termination reason: Instruction limit
% 5.97/1.65 % (113454)Termination phase: Saturation
% 5.97/1.65 % (113454)Time elapsed: 0.050 s
% 5.97/1.65 % (113454)Peak memory usage: 88 MB
% 5.97/1.65 % (113454)Instructions burned: 126 (million)
% 5.97/1.65 % (113455)Instruction limit reached!
% 5.97/1.65 % (113455)------------------------------
% 5.97/1.65 % (113455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113455)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113455)Termination reason: Instruction limit
% 5.97/1.65 % (113455)Termination phase: Saturation
% 5.97/1.65 % (113455)Time elapsed: 0.045 s
% 5.97/1.65 % (113455)Peak memory usage: 88 MB
% 5.97/1.65 % (113455)Instructions burned: 197 (million)
% 5.97/1.65 % (113456)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3092093157:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.97/1.65 % (113449)------------------------------
% 5.97/1.65 % (113449)------------------------------
% 5.97/1.65 % (113456)First to succeed.
% 5.97/1.65 % (113456)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-113429"
% 5.97/1.65 % (113459)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2399570285:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.97/1.65 % (113460)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=3925344943:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.97/1.65 % (113460)Instruction limit reached!
% 5.97/1.65 % (113460)------------------------------
% 5.97/1.65 % (113460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113460)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113460)Termination reason: Instruction limit
% 5.97/1.65 % (113460)Termination phase: Saturation
% 5.97/1.65 % (113460)Time elapsed: 0.042 s
% 5.97/1.65 % (113460)Peak memory usage: 89 MB
% 5.97/1.65 % (113460)Instructions burned: 108 (million)
% 5.97/1.65 % (113462)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1499424424:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 5.97/1.65 % (113462)Instruction limit reached!
% 5.97/1.65 % (113462)------------------------------
% 5.97/1.65 % (113462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113462)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113462)Termination reason: Instruction limit
% 5.97/1.65 % (113462)Termination phase: Saturation
% 5.97/1.65 % (113462)Time elapsed: 0.051 s
% 5.97/1.65 % (113462)Peak memory usage: 88 MB
% 5.97/1.65 % (113462)Instructions burned: 107 (million)
% 5.97/1.65 % (113436)Refutation not found, incomplete strategy
% 5.97/1.65 % (113436)------------------------------
% 5.97/1.65 % (113436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.65 % (113436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.65 % (113436)CaDiCaL version: 2.1.3
% 5.97/1.65 % (113436)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.65 % (113436)Time elapsed: 0.772 s
% 5.97/1.65 % (113436)Peak memory usage: 128 MB
% 5.97/1.65 % (113436)Instructions burned: 1189 (million)
% 5.97/1.65 % SZS status Satisfiable for theBenchmark
% 5.97/1.65 % SZS output start Saturation.
% See solution above
% 7.53/1.84 % SZS output start Definitions and Model Updates.
% 7.53/1.84 % SZS output end Definitions and Model Updates.
% 7.53/1.84 % (113456)------------------------------
% 7.53/1.84 % (113456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/1.84 % (113456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.84 % (113456)CaDiCaL version: 2.1.3
% 7.53/1.84 % (113456)Termination reason: Satisfiable
% 7.53/1.84 % (113456)Time elapsed: 0.050 s
% 7.53/1.85 % (113456)Peak memory usage: 89 MB
% 7.53/1.85 % (113456)Instructions burned: 75 (million)
% 7.53/1.85 % (113456)------------------------------
% 7.53/1.85 % (113456)------------------------------
% 7.53/1.85 % (113429)Success in time 0.975 s
% 7.53/1.85 % Vampire exiting
%------------------------------------------------------------------------------