%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV536-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:16 PM UTC 2026
% Result : Satisfiable 35.87s 9.26s
% Output : Saturation 0.32s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u264,axiom,
i5 != i9 ).
cnf(u269,axiom,
sF12 = select(sF9,i9) ).
cnf(u314,axiom,
i8 != i6 ).
cnf(u319,axiom,
sF43 = select(sF39,i6) ).
cnf(u381,axiom,
i7 != i6 ).
cnf(u386,axiom,
sF4 = sF41 ).
cnf(u456,axiom,
i6 != i9 ).
cnf(u461,axiom,
sF72 = select(sF73,i9) ).
cnf(u575,axiom,
i1 != i2 ).
cnf(u580,axiom,
sF64 = select(sF65,i1) ).
cnf(u613,axiom,
i0 != i3 ).
cnf(u618,axiom,
sF68 = select(sF69,i0) ).
cnf(u866,axiom,
i4 != i2 ).
cnf(u1521,axiom,
i6 != sF76 ).
cnf(u2236,axiom,
sF12 = select(sF5,i9) ).
cnf(u2247,axiom,
sF14 = select(sF9,i4) ).
cnf(u2258,axiom,
sF14 = select(sF5,i4) ).
cnf(u2277,axiom,
sF2 = select(sF39,i8) ).
cnf(u2679,axiom,
i0 != i2 ).
cnf(u2684,axiom,
sF31 = select(sF28,i0) ).
cnf(u2763,axiom,
sF53 = select(sF54,i7) ).
cnf(u3345,axiom,
sF12 = select(sF1,i9) ).
cnf(u3354,axiom,
sF14 = select(sF1,i4) ).
cnf(u3373,axiom,
i1 = i0 ).
cnf(u3442,axiom,
sF12 = select(sF13,i9) ).
cnf(u3455,axiom,
sF20 = select(sF21,i5) ).
cnf(u3464,axiom,
sF57 = select(sF58,i5) ).
cnf(u3477,axiom,
sF49 = select(sF50,i9) ).
cnf(u3492,axiom,
sF33 = select(sF28,i3) ).
cnf(u3501,axiom,
sF16 = select(sF17,i1) ).
cnf(u3518,axiom,
sF16 = select(sF13,i1) ).
cnf(u3523,axiom,
sF18 = select(sF13,i7) ).
cnf(u3534,axiom,
sF51 = select(sF46,i4) ).
cnf(u3539,axiom,
sF49 = select(sF46,i9) ).
cnf(u3556,axiom,
i4 = i1 ).
cnf(u3647,axiom,
sF49 = sF55 ).
cnf(u3658,axiom,
sF53 = select(sF50,i7) ).
cnf(u3669,axiom,
sF8 = select(sF5,i5) ).
cnf(u3684,axiom,
sF8 = select(sF1,i5) ).
cnf(u3697,axiom,
sF53 = sF59 ).
cnf(u3707,axiom,
sF57 = select(sF54,i5) ).
cnf(u3718,axiom,
sF53 = select(sF46,i7) ).
cnf(u3731,axiom,
sF47 = select(sF42,i5) ).
cnf(u3748,axiom,
sF20 = sF29 ).
cnf(u3766,axiom,
sF18 = select(sF9,i7) ).
cnf(u3775,axiom,
sF2 = sF18 ).
cnf(u3801,axiom,
sF49 = select(sF42,i9) ).
cnf(u3810,axiom,
sF51 = select(sF42,i4) ).
cnf(u3817,axiom,
sF49 = select(sF39,i9) ).
cnf(u3826,axiom,
sF53 = select(sF42,i7) ).
cnf(u3839,axiom,
sF18 = sF53 ).
cnf(u3869,axiom,
sF4 = select(sF1,i7) ).
cnf(u3878,axiom,
sF12 = sF49 ).
cnf(u3907,axiom,
sF6 = select(sF13,i5) ).
cnf(u3914,axiom,
i9 = sF76 ).
cnf(u4001,axiom,
sF47 = select(sF39,i5) ).
cnf(u4020,axiom,
sF20 = select(sF17,i5) ).
cnf(u4057,axiom,
sF8 = sF47 ).
cnf(u4076,axiom,
sF51 = select(sF39,i4) ).
cnf(u4085,axiom,
sF14 = sF51 ).
cnf(u4115,axiom,
sF57 = sF64 ).
cnf(u4159,axiom,
sF6 = sF20 ).
cnf(u4193,axiom,
sF70 = select(sF73,i4) ).
cnf(u4204,axiom,
sF74 = select(sF69,i6) ).
cnf(u4211,axiom,
sF35 = select(sF32,i5) ).
cnf(u4226,axiom,
sF35 = select(sF28,i5) ).
cnf(u4235,axiom,
sF18 = sF35 ).
cnf(u4267,axiom,
sF14 = select(sF17,sF76) ).
cnf(u4280,axiom,
sF74 = select(sF65,i6) ).
cnf(u4285,axiom,
sF8 = select(sF50,i8) ).
cnf(u4294,axiom,
sF33 = select(sF36,i4) ).
cnf(u4299,axiom,
sF6 = select(sF46,i8) ).
cnf(u4314,axiom,
sF18 = select(sF25,i5) ).
cnf(u4319,axiom,
sF72 = select(sF69,sF76) ).
cnf(u4326,axiom,
sF37 = select(sF32,sF76) ).
cnf(u4337,axiom,
sF37 = select(sF28,sF76) ).
cnf(u4344,axiom,
sF37 = select(sF25,sF76) ).
cnf(u4353,axiom,
sF12 = select(sF58,i7) ).
cnf(u4372,axiom,
sF27 = select(sF17,i2) ).
cnf(u4379,axiom,
sF14 = sF37 ).
cnf(u4390,axiom,
sF33 = select(sF17,i3) ).
cnf(u4403,axiom,
sF27 = select(sF13,i2) ).
cnf(u4412,axiom,
sF27 = select(sF9,i2) ).
cnf(u4423,axiom,
sF27 = select(sF5,i2) ).
cnf(u4430,axiom,
sF27 = select(sF1,i2) ).
cnf(u4439,axiom,
sF33 = select(sF13,i3) ).
cnf(u4448,axiom,
sF33 = select(sF9,i3) ).
cnf(u4459,axiom,
sF33 = select(sF5,i3) ).
cnf(u4466,axiom,
sF33 = select(sF1,i3) ).
cnf(u4477,axiom,
sF6 = select(sF32,i2) ).
cnf(u4484,axiom,
sF72 = select(sF65,sF76) ).
cnf(u4489,axiom,
sF14 = select(sF54,sF76) ).
cnf(u4502,axiom,
sF57 = select(sF50,i5) ).
cnf(u4511,axiom,
sF6 = sF57 ).
cnf(u4566,axiom,
sF70 = select(sF62,i3) ).
cnf(u4571,axiom,
sF74 = select(sF62,i6) ).
cnf(u4576,axiom,
sF18 = select(sF62,i5) ).
cnf(u4591,axiom,
sF66 = select(sF58,i2) ).
cnf(u4600,axiom,
sF66 = select(sF54,i2) ).
cnf(u4609,axiom,
sF66 = select(sF50,i2) ).
cnf(u4618,axiom,
sF66 = select(sF46,i2) ).
cnf(u4625,axiom,
sF70 = select(sF58,i3) ).
cnf(u4634,axiom,
sF70 = select(sF54,i3) ).
cnf(u4643,axiom,
sF66 = select(sF42,i2) ).
cnf(u4650,axiom,
sF66 = select(sF39,i2) ).
cnf(u4659,axiom,
sF27 = sF66 ).
cnf(u4698,axiom,
sF70 = select(sF50,i3) ).
cnf(u4707,axiom,
sF70 = select(sF46,i3) ).
cnf(u4714,axiom,
sF70 = select(sF42,i3) ).
cnf(u4721,axiom,
sF70 = select(sF39,i3) ).
cnf(u4730,axiom,
sF33 = sF70 ).
cnf(u4771,axiom,
sF74 = select(sF58,i6) ).
cnf(u4780,axiom,
sF74 = select(sF54,i6) ).
cnf(u4789,axiom,
sF74 = select(sF50,i6) ).
cnf(u4798,axiom,
sF74 = select(sF46,i6) ).
cnf(u4809,axiom,
sF4 = sF74 ).
cnf(u4848,axiom,
sF72 = select(sF62,sF76) ).
cnf(u4857,axiom,
sF72 = select(sF58,sF76) ).
cnf(u4866,axiom,
sF14 = sF72 ).
cnf(u3576,axiom,
i4 = i0 ).
cnf(u4734,axiom,
sF71 = store(sF69,i4,sF33) ).
cnf(u4239,axiom,
sF36 = store(sF34,sF76,sF18) ).
cnf(u3583,axiom,
( select(sF32,X0) = select(sF34,X0)
| i4 = X0 ) ).
cnf(u3614,axiom,
sF18 = select(sF23,i5) ).
cnf(u3570,axiom,
( select(sF17,X0) = select(sF19,X0)
| i4 = X0 ) ).
cnf(u4091,axiom,
sF14 = select(sF52,sF76) ).
cnf(u4873,axiom,
sF14 = select(sF65,sF76) ).
cnf(u3846,axiom,
sF18 = sF59 ).
cnf(u4244,axiom,
sF18 = select(sF32,i5) ).
cnf(u3611,axiom,
sF12 = select(sF17,i4) ).
cnf(u3315,axiom,
sF6 = select(sF46,i5) ).
cnf(u3609,axiom,
sF18 = sF22 ).
cnf(u3481,axiom,
( select(sF39,X0) = select(sF42,X0)
| i8 = X0
| i6 = X0 ) ).
cnf(u3317,axiom,
sF6 = select(sF39,i6) ).
cnf(u3945,axiom,
sF12 = select(sF42,sF76) ).
cnf(u3568,axiom,
sF18 = select(sF19,i4) ).
cnf(u4815,axiom,
sF4 = select(sF69,i6) ).
cnf(u4165,axiom,
sF6 = sF29 ).
cnf(u241,axiom,
( select(sF46,X0) = select(sF48,X0)
| i8 = X0 ) ).
cnf(u4669,axiom,
sF27 = select(sF58,i2) ).
cnf(u4735,axiom,
sF33 = select(sF71,i4) ).
cnf(u4740,axiom,
sF33 = select(sF50,i3) ).
cnf(u3885,axiom,
sF12 = sF55 ).
cnf(u4668,axiom,
sF27 = select(sF62,i2) ).
cnf(u3183,axiom,
sF4 = select(sF40,i8) ).
cnf(u3606,axiom,
sF12 = sF16 ).
cnf(u4742,axiom,
sF33 = select(sF42,i3) ).
cnf(u3573,axiom,
( select(sF65,X0) = select(sF67,X0)
| i4 = X0 ) ).
cnf(u4025,axiom,
( select(sF58,X0) = select(sF62,X0)
| i5 = X0
| i4 = X0 ) ).
cnf(u4386,axiom,
sF14 = select(sF25,sF76) ).
cnf(u4524,axiom,
sF6 = select(sF60,i4) ).
cnf(u3886,axiom,
sF12 = select(sF52,i4) ).
cnf(u4818,axiom,
sF4 = select(sF62,i6) ).
cnf(u4743,axiom,
sF33 = select(sF39,i3) ).
cnf(u250,axiom,
( select(sF63,X0) = select(sF65,X0)
| i2 = X0 ) ).
cnf(u4672,axiom,
sF27 = select(sF46,i2) ).
cnf(u674,axiom,
( select(sF28,X0) = select(sF32,X0)
| i3 = X0
| i2 = X0 ) ).
cnf(u252,axiom,
( select(sF67,X0) = select(sF69,X0)
| i3 = X0 ) ).
cnf(u3943,axiom,
sF12 = select(sF50,sF76) ).
cnf(u246,axiom,
( select(sF56,X0) = select(sF58,X0)
| i4 = X0 ) ).
cnf(u245,axiom,
( select(sF54,X0) = select(sF56,X0)
| i7 = X0 ) ).
cnf(u3944,axiom,
sF12 = select(sF46,sF76) ).
cnf(u232,axiom,
( select(sF28,X0) = select(sF30,X0)
| i2 = X0 ) ).
cnf(u239,axiom,
( select(sF42,X0) = select(sF44,X0)
| i8 = X0 ) ).
cnf(u225,axiom,
( select(sF15,X0) = select(sF17,X0)
| i7 = X0 ) ).
cnf(u228,axiom,
( select(sF21,X0) = select(sF23,X0)
| i5 = X0 ) ).
cnf(u3850,axiom,
sF18 = select(sF46,i7) ).
cnf(u219,axiom,
( select(sF3,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u4035,axiom,
( select(sF69,X0) = select(sF73,X0)
| i6 = X0
| i4 = X0 ) ).
cnf(u184,axiom,
sF6 = select(sF7,i8) ).
cnf(u4061,axiom,
sF8 = select(sF48,i8) ).
cnf(u19,axiom,
store(sF5,i8,sF6) = sF7 ).
cnf(u3528,axiom,
( select(sF46,X0) = select(sF50,X0)
| i4 = X0
| i8 = X0 ) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u4674,axiom,
sF27 = select(sF39,i2) ).
cnf(u4673,axiom,
sF27 = select(sF42,i2) ).
cnf(u15,axiom,
store(sF3,i6,sF4) = sF5 ).
cnf(u4821,axiom,
sF4 = select(sF50,i6) ).
cnf(u3847,axiom,
sF18 = select(sF60,i5) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u4517,axiom,
sF6 = select(sF54,i5) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u3782,axiom,
sF18 = select(sF39,i8) ).
cnf(u3939,axiom,
( select(sF13,X0) = select(sF17,X0)
| sF76 = X0
| i7 = X0 ) ).
cnf(u4663,axiom,
sF27 = select(sF69,i3) ).
cnf(u4013,axiom,
sF33 = select(sF25,i3) ).
cnf(u3887,axiom,
sF56 = store(sF54,i7,sF12) ).
cnf(u3579,axiom,
sF33 = select(sF34,i4) ).
cnf(u3432,axiom,
( select(sF9,X0) = select(sF13,X0)
| i5 = X0
| i4 = X0 ) ).
cnf(u3582,axiom,
( select(sF25,X0) = select(sF26,X0)
| i4 = X0 ) ).
cnf(u3581,axiom,
( select(sF23,X0) = select(sF25,X0)
| i4 = X0 ) ).
cnf(u3311,axiom,
sF6 = select(sF40,i6) ).
cnf(u3777,axiom,
select(a1,i8) = sF18 ).
cnf(u3559,axiom,
sF19 = store(sF17,i4,sF18) ).
cnf(u4090,axiom,
sF52 = store(sF50,sF76,sF14) ).
cnf(u3916,axiom,
sF12 = select(sF11,sF76) ).
cnf(u3942,axiom,
sF12 = select(sF48,sF76) ).
cnf(u247,axiom,
( select(sF58,X0) = select(sF60,X0)
| i5 = X0 ) ).
cnf(u4518,axiom,
sF6 = sF64 ).
cnf(u4869,axiom,
sF14 = select(sF73,i6) ).
cnf(u222,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u4382,axiom,
sF14 = select(sF38,i5) ).
cnf(u4174,axiom,
sF6 = select(sF25,i4) ).
cnf(u4514,axiom,
sF58 = store(sF56,i4,sF6) ).
cnf(u4173,axiom,
sF26 = store(sF25,i4,sF6) ).
cnf(u2812,axiom,
( select(sF54,X0) = select(sF58,X0)
| i4 = X0
| i7 = X0 ) ).
cnf(u4014,axiom,
sF27 = select(sF25,i2) ).
cnf(u4093,axiom,
sF14 = select(sF39,i4) ).
cnf(u4871,axiom,
sF14 = select(sF73,sF76) ).
cnf(u3613,axiom,
sF17 = store(sF15,i7,sF12) ).
cnf(u3937,axiom,
sF12 = select(sF13,sF76) ).
cnf(u3932,axiom,
sF12 = select(sF9,sF76) ).
cnf(u3849,axiom,
sF18 = select(sF56,i4) ).
cnf(u4169,axiom,
sF6 = sF24 ).
cnf(u2137,axiom,
( select(sF5,X0) = select(sF9,X0)
| i8 = X0 ) ).
cnf(u4172,axiom,
sF25 = store(sF23,i4,sF6) ).
cnf(u3610,axiom,
sF12 = select(sF15,i4) ).
cnf(u4515,axiom,
sF6 = select(sF58,i4) ).
cnf(u4733,axiom,
sF33 = select(sF65,i3) ).
cnf(u3587,axiom,
i4 != i3 ).
cnf(u3927,axiom,
( select(sF13,X0) = select(sF15,X0)
| sF76 = X0 ) ).
cnf(u3560,axiom,
sF28 = store(sF26,i4,sF27) ).
cnf(u4661,axiom,
sF27 = select(sF63,i2) ).
cnf(u4874,axiom,
sF14 = select(sF62,sF76) ).
cnf(u4060,axiom,
sF48 = store(sF46,i8,sF8) ).
cnf(u3593,axiom,
sF27 = select(sF30,i4) ).
cnf(u4664,axiom,
sF69 = store(sF67,i3,sF27) ).
cnf(u3316,axiom,
sF46 = store(sF44,i5,sF6) ).
cnf(u3935,axiom,
sF12 = select(sF5,sF76) ).
cnf(u3843,axiom,
sF54 = store(sF52,i4,sF18) ).
cnf(u3184,axiom,
sF4 = select(sF1,i8) ).
cnf(u3483,axiom,
sF4 = select(sF42,i8) ).
cnf(u3844,axiom,
sF18 = select(sF54,i4) ).
cnf(u3778,axiom,
sF3 = store(sF1,i7,sF18) ).
cnf(u3577,axiom,
sF34 = store(sF32,i4,sF33) ).
cnf(u3404,axiom,
sF27 = sF31 ).
cnf(u3608,axiom,
( select(sF25,X0) = select(sF28,X0)
| i4 = X0 ) ).
cnf(u4516,axiom,
sF6 = select(sF58,i5) ).
cnf(u4042,axiom,
( select(sF62,X0) = select(sF65,X0)
| i2 = X0
| i4 = X0 ) ).
cnf(u3415,axiom,
sF27 = select(sF32,i3) ).
cnf(u254,axiom,
( select(sF71,X0) = select(sF73,X0)
| i6 = X0 ) ).
cnf(u3946,axiom,
sF12 = select(sF39,sF76) ).
cnf(u240,axiom,
( select(sF44,X0) = select(sF46,X0)
| i5 = X0 ) ).
cnf(u4822,axiom,
sF4 = select(sF46,i6) ).
cnf(u3585,axiom,
( select(sF62,X0) = select(sF63,X0)
| i4 = X0 ) ).
cnf(u4245,axiom,
sF18 = select(sF28,i5) ).
cnf(u233,axiom,
( select(sF30,X0) = select(sF32,X0)
| i3 = X0 ) ).
cnf(u3188,axiom,
sF4 = select(sF42,i6) ).
cnf(u4527,axiom,
sF6 = select(sF62,i4) ).
cnf(u236,axiom,
( select(sF36,X0) = select(sF38,X0)
| i5 = X0 ) ).
cnf(u227,axiom,
( select(sF19,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u33,axiom,
select(sF11,i4) = sF14 ).
cnf(u3917,axiom,
sF15 = store(sF13,sF76,sF14) ).
cnf(u71,axiom,
select(sF30,i3) = sF33 ).
cnf(u3941,axiom,
( select(sF50,X0) = select(sF54,X0)
| sF76 = X0
| i4 = X0 ) ).
cnf(u186,axiom,
sF11 = store(sF9,i5,sF6) ).
cnf(u4528,axiom,
sF6 = select(sF50,i5) ).
cnf(u216,axiom,
( select(a1,X0) = select(sF39,X0)
| i7 = X0 ) ).
cnf(u185,axiom,
sF6 = sF10 ).
cnf(u223,axiom,
( select(sF11,X0) = select(sF13,X0)
| i4 = X0 ) ).
cnf(u4523,axiom,
sF6 = select(sF65,i4) ).
cnf(u23,axiom,
store(sF7,i8,sF8) = sF9 ).
cnf(u3841,axiom,
sF18 = select(sF52,i7) ).
cnf(u4175,axiom,
sF6 = select(sF17,i5) ).
cnf(u4519,axiom,
sF65 = store(sF63,i2,sF6) ).
cnf(u3936,axiom,
sF12 = select(sF1,sF76) ).
cnf(u3309,axiom,
sF6 = sF43 ).
cnf(u4063,axiom,
sF8 = select(sF42,i5) ).
cnf(u4237,axiom,
sF18 = select(sF34,i5) ).
cnf(u3312,axiom,
sF44 = store(sF42,i8,sF6) ).
cnf(u4812,axiom,
sF75 = store(sF73,sF76,sF4) ).
cnf(u4819,axiom,
sF4 = select(sF58,i6) ).
cnf(u3888,axiom,
sF12 = select(sF56,i7) ).
cnf(u3929,axiom,
( select(sF50,X0) = select(sF52,X0)
| sF76 = X0 ) ).
cnf(u4240,axiom,
sF18 = select(sF36,sF76) ).
cnf(u3779,axiom,
sF39 = store(a1,i7,sF18) ).
cnf(u4241,axiom,
sF18 = sF77 ).
cnf(u3572,axiom,
( select(sF52,X0) = select(sF54,X0)
| i4 = X0 ) ).
cnf(u3924,axiom,
sF14 = select(sF15,sF76) ).
cnf(u3416,axiom,
sF32 = store(sF30,i3,sF27) ).
cnf(u3566,axiom,
sF27 = select(sF28,i4) ).
cnf(u4087,axiom,
sF14 = select(sF48,i4) ).
cnf(u238,axiom,
( select(sF40,X0) = select(sF42,X0)
| i6 = X0 ) ).
cnf(u4870,axiom,
sF14 = select(sF71,sF76) ).
cnf(u4167,axiom,
sF6 = select(sF30,i2) ).
cnf(u4732,axiom,
sF33 = select(sF67,i3) ).
cnf(u3842,axiom,
sF18 = select(sF54,i7) ).
cnf(u4089,axiom,
sF14 = select(sF42,i4) ).
cnf(u4820,axiom,
sF4 = select(sF54,i6) ).
cnf(u4811,axiom,
sF4 = select(sF71,i6) ).
cnf(u4665,axiom,
sF67 = store(sF65,i4,sF27) ).
cnf(u3190,axiom,
select(a1,i7) = sF4 ).
cnf(u2269,axiom,
( select(sF39,X0) = select(sF1,X0)
| i8 = X0
| i7 = X0 ) ).
cnf(u4666,axiom,
sF27 = select(sF67,i4) ).
cnf(u3185,axiom,
sF40 = store(sF39,i8,sF4) ).
cnf(u4164,axiom,
sF6 = select(sF21,i5) ).
cnf(u3612,axiom,
sF12 = select(sF17,i7) ).
cnf(u3851,axiom,
sF18 = select(sF42,i7) ).
cnf(u157,axiom,
sk(sF38,sF75) = sF76 ).
cnf(u3727,axiom,
( select(sF42,X0) = select(sF46,X0)
| i5 = X0
| i8 = X0 ) ).
cnf(u3882,axiom,
sF12 = select(sF50,i4) ).
cnf(u3586,axiom,
( select(sF69,X0) = select(sF71,X0)
| i4 = X0 ) ).
cnf(u4171,axiom,
sF6 = select(sF23,i4) ).
cnf(u4525,axiom,
sF62 = store(sF60,i4,sF6) ).
cnf(u3781,axiom,
sF18 = select(sF3,i7) ).
cnf(u3881,axiom,
sF50 = store(sF48,i4,sF12) ).
cnf(u4238,axiom,
sF18 = select(sF36,i5) ).
cnf(u59,axiom,
select(sF26,i2) = sF27 ).
cnf(u3187,axiom,
sF42 = store(sF40,i6,sF4) ).
cnf(u242,axiom,
( select(sF48,X0) = select(sF50,X0)
| i4 = X0 ) ).
cnf(u3780,axiom,
sF18 = select(sF39,i7) ).
cnf(u4242,axiom,
sF18 = select(sF38,sF76) ).
cnf(u170,axiom,
sF12 = select(sF13,i4) ).
cnf(u4667,axiom,
sF27 = select(sF69,i4) ).
cnf(u3605,axiom,
( select(sF17,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u3197,axiom,
sF27 = select(sF28,i2) ).
cnf(u4064,axiom,
sF8 = select(sF39,i5) ).
cnf(u41,axiom,
select(sF15,i7) = sF18 ).
cnf(u4737,axiom,
sF33 = select(sF62,i3) ).
cnf(u4385,axiom,
sF14 = select(sF28,sF76) ).
cnf(u3783,axiom,
sF18 = select(sF5,i7) ).
cnf(u4739,axiom,
sF33 = select(sF54,i3) ).
cnf(u3602,axiom,
( select(sF65,X0) = select(sF69,X0)
| i4 = X0
| i3 = X0 ) ).
cnf(u4868,axiom,
sF73 = store(sF71,i6,sF14) ).
cnf(u3194,axiom,
sF6 = select(sF1,i6) ).
cnf(u4088,axiom,
sF14 = select(sF46,i4) ).
cnf(u4381,axiom,
sF38 = store(sF36,i5,sF14) ).
cnf(u3615,axiom,
sF23 = store(sF21,i5,sF18) ).
cnf(u31,axiom,
store(sF11,i4,sF12) = sF13 ).
cnf(u4662,axiom,
sF27 = sF68 ).
cnf(u3848,axiom,
sF60 = store(sF58,i5,sF18) ).
cnf(u3314,axiom,
sF6 = sF45 ).
cnf(u17,axiom,
select(sF3,i6) = sF6 ).
cnf(u4059,axiom,
sF8 = select(sF44,i5) ).
cnf(u4817,axiom,
sF4 = select(sF65,i6) ).
cnf(u3584,axiom,
( select(sF60,X0) = select(sF62,X0)
| i4 = X0 ) ).
cnf(u4051,axiom,
( select(sF32,X0) = select(sF36,X0)
| sF76 = X0
| i4 = X0 ) ).
cnf(u3928,axiom,
( select(sF34,X0) = select(sF36,X0)
| sF76 = X0 ) ).
cnf(u4872,axiom,
sF14 = select(sF69,sF76) ).
cnf(u4814,axiom,
sF4 = sF78 ).
cnf(u4738,axiom,
sF33 = select(sF58,i3) ).
cnf(u4813,axiom,
sF4 = select(sF75,sF76) ).
cnf(u4816,negated_conjecture,
sF4 != sF18 ).
cnf(u3313,axiom,
sF6 = select(sF44,i8) ).
cnf(u4736,axiom,
sF33 = select(sF73,i4) ).
cnf(u3996,axiom,
sF27 = select(sF32,i4) ).
cnf(u4741,axiom,
sF33 = select(sF46,i3) ).
cnf(u4166,axiom,
sF30 = store(sF28,i2,sF6) ).
cnf(u4383,axiom,
sF14 = select(sF34,sF76) ).
cnf(u4520,axiom,
sF6 = select(sF65,i2) ).
cnf(u3189,axiom,
sF0 = sF4 ).
cnf(u237,axiom,
( select(sF39,X0) = select(sF40,X0)
| i8 = X0 ) ).
cnf(u3930,axiom,
( select(sF73,X0) = select(sF75,X0)
| sF76 = X0 ) ).
cnf(u3192,axiom,
sF4 = select(sF5,i8) ).
cnf(u4384,axiom,
sF14 = select(sF32,sF76) ).
cnf(u3186,axiom,
sF1 = store(a1,i8,sF4) ).
cnf(u218,axiom,
( select(sF1,X0) = select(sF3,X0)
| i7 = X0 ) ).
cnf(u187,axiom,
sF6 = select(sF11,i5) ).
cnf(u4521,axiom,
sF6 = sF61 ).
cnf(u217,axiom,
( select(a1,X0) = select(sF1,X0)
| i8 = X0 ) ).
cnf(u4670,axiom,
sF27 = select(sF54,i2) ).
cnf(u220,axiom,
( select(sF5,X0) = select(sF7,X0)
| i8 = X0 ) ).
cnf(u2284,axiom,
( select(sF1,X0) = select(sF5,X0)
| i6 = X0
| i7 = X0 ) ).
cnf(u4030,axiom,
( select(sF17,X0) = select(sF25,X0)
| i5 = X0
| i4 = X0 ) ).
cnf(u4161,axiom,
sF6 = select(sF19,i5) ).
cnf(u4170,axiom,
sF6 = select(sF26,i4) ).
cnf(u169,axiom,
sF8 = select(sF9,i8) ).
cnf(u4513,axiom,
sF6 = select(sF56,i5) ).
cnf(u13,axiom,
select(sF3,i8) = sF4 ).
cnf(u4526,axiom,
sF63 = store(sF62,i4,sF6) ).
cnf(u4163,axiom,
sF6 = select(sF21,i4) ).
cnf(u166,axiom,
sF4 = select(sF5,i6) ).
cnf(u4522,axiom,
sF6 = select(sF63,i4) ).
cnf(u3931,axiom,
i5 != sF76 ).
cnf(u4671,axiom,
sF27 = select(sF50,i2) ).
cnf(u3845,axiom,
sF18 = select(sF50,i7) ).
cnf(u4875,axiom,
sF14 = select(sF58,sF76) ).
cnf(u4162,axiom,
sF21 = store(sF19,i4,sF6) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV536-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.11 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.26 % Computer : n001.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.26 % CPULimit : 300
% 0.11/0.26 % WCLimit : 300
% 0.11/0.26 % DateTime : Mon Sep 28 11:41:48 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.34 Running first-order theorem proving
% 0.25/0.34 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.70/6.04 % (297759)Input is clausal, will run a generic CNF schedule.
% 13.70/6.04 % (297764)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=3099706007:i=140167_2960 on theBenchmark for (2960ds/140167Mi)
% 13.70/6.04 % (297769)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4041879232:s2a=on:i=180:gtg=position_2960 on theBenchmark for (2960ds/180Mi)
% 13.70/6.04 % (297765)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1075981620:i=132376:av=off_2960 on theBenchmark for (2960ds/132376Mi)
% 13.70/6.04 % (297766)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4074954868:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2960 on theBenchmark for (2960ds/137899Mi)
% 13.70/6.04 % (297768)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2712313945:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2960 on theBenchmark for (2960ds/114Mi)
% 13.70/6.04 % (297767)lrs+10_1_sil=8000:sp=occurrence:random_seed=4280454526:i=107:sd=3:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/107Mi)
% 13.70/6.04 % (297770)dis-21_1_sil=8000:lcm=predicate:random_seed=3359298997:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2960 on theBenchmark for (2960ds/117Mi)
% 13.70/6.04 % (297767)Instruction limit reached!
% 13.70/6.04 % (297767)------------------------------
% 13.70/6.04 % (297767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/6.04 % (297767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/6.04 % (297767)CaDiCaL version: 2.1.3
% 13.70/6.04 % (297767)Termination reason: Instruction limit
% 13.70/6.04 % (297767)Termination phase: SInE selection
% 13.70/6.04 % (297767)Time elapsed: 0.041 s
% 13.70/6.04 % (297767)Peak memory usage: 83 MB
% 13.70/6.04 % (297767)Instructions burned: 109 (million)
% 13.70/6.04 % (297768)Instruction limit reached!
% 13.70/6.04 % (297768)------------------------------
% 13.70/6.04 % (297768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/6.04 % (297768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/6.04 % (297768)CaDiCaL version: 2.1.3
% 13.70/6.04 % (297768)Termination reason: Instruction limit
% 13.70/6.04 % (297768)Termination phase: SInE selection
% 13.70/6.04 % (297768)Time elapsed: 0.043 s
% 13.70/6.04 % (297768)Peak memory usage: 83 MB
% 13.70/6.04 % (297768)Instructions burned: 115 (million)
% 13.70/6.04 % (297769)Instruction limit reached!
% 13.70/6.04 % (297769)------------------------------
% 13.70/6.04 % (297769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/6.04 % (297769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/6.04 % (297769)CaDiCaL version: 2.1.3
% 13.70/6.04 % (297769)Termination reason: Instruction limit
% 13.70/6.04 % (297769)Termination phase: Property scanning
% 13.70/6.04 % (297769)Time elapsed: 0.059 s
% 13.70/6.04 % (297769)Peak memory usage: 84 MB
% 13.70/6.04 % (297769)Instructions burned: 182 (million)
% 13.70/6.04 % (297770)Instruction limit reached!
% 13.70/6.04 % (297770)------------------------------
% 13.70/6.04 % (297770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/6.04 % (297770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/6.04 % (297770)CaDiCaL version: 2.1.3
% 13.70/6.04 % (297770)Termination reason: Instruction limit
% 13.70/6.04 % (297770)Termination phase: SInE selection
% 13.70/6.04 % (297770)Time elapsed: 0.044 s
% 13.70/6.04 % (297770)Peak memory usage: 83 MB
% 13.70/6.04 % (297770)Instructions burned: 117 (million)
% 13.70/6.04 % (297781)lrs+10_64_to=lpo:sil=8000:random_seed=490841547:i=126:bd=preordered_2958 on theBenchmark for (2958ds/126Mi)
% 13.70/6.04 % (297780)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1431575264:st=4:i=219:sd=3:ss=axioms_2958 on theBenchmark for (2958ds/219Mi)
% 13.70/6.04 % (297779)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=183549376:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2958 on theBenchmark for (2958ds/189Mi)
% 13.70/6.04 % (297778)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=3491431534:i=143:sd=2:aac=none:ss=axioms:sgt=16_2958 on theBenchmark for (2958ds/143Mi)
% 13.70/6.04 % (297778)Instruction limit reached!
% 13.70/6.04 % (297778)------------------------------
% 17.69/6.75 % (297778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297778)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297778)Termination reason: Instruction limit
% 17.69/6.75 % (297778)Termination phase: SInE selection
% 17.69/6.75 % (297778)Time elapsed: 0.054 s
% 17.69/6.75 % (297778)Peak memory usage: 83 MB
% 17.69/6.75 % (297778)Instructions burned: 145 (million)
% 17.69/6.75 % (297781)Instruction limit reached!
% 17.69/6.75 % (297781)------------------------------
% 17.69/6.75 % (297781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297781)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297781)Termination reason: Instruction limit
% 17.69/6.75 % (297781)Termination phase: Saturation
% 17.69/6.75 % (297781)Time elapsed: 0.058 s
% 17.69/6.75 % (297781)Peak memory usage: 99 MB
% 17.69/6.75 % (297781)Instructions burned: 128 (million)
% 17.69/6.75 % (297779)Instruction limit reached!
% 17.69/6.75 % (297779)------------------------------
% 17.69/6.75 % (297779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297779)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297779)Termination reason: Instruction limit
% 17.69/6.75 % (297779)Termination phase: SInE selection
% 17.69/6.75 % (297779)Time elapsed: 0.072 s
% 17.69/6.75 % (297779)Peak memory usage: 83 MB
% 17.69/6.75 % (297779)Instructions burned: 191 (million)
% 17.69/6.75 % (297780)Instruction limit reached!
% 17.69/6.75 % (297780)------------------------------
% 17.69/6.75 % (297780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297780)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297780)Termination reason: Instruction limit
% 17.69/6.75 % (297780)Termination phase: SInE selection
% 17.69/6.75 % (297780)Time elapsed: 0.083 s
% 17.69/6.75 % (297780)Peak memory usage: 83 MB
% 17.69/6.75 % (297780)Instructions burned: 220 (million)
% 17.69/6.75 % (297787)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1555239985:i=157:gtg=all_2956 on theBenchmark for (2956ds/157Mi)
% 17.69/6.75 % (297786)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=329803957:avsq=on:i=194:fgj=on:bd=preordered_2956 on theBenchmark for (2956ds/194Mi)
% 17.69/6.75 % (297788)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1104522142:i=3394:sd=4:ss=included:sgt=64_2956 on theBenchmark for (2956ds/3394Mi)
% 17.69/6.75 % (297789)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=1387568534:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2956 on theBenchmark for (2956ds/106Mi)
% 17.69/6.75 % (297787)Instruction limit reached!
% 17.69/6.75 % (297787)------------------------------
% 17.69/6.75 % (297787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297787)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297787)Termination reason: Instruction limit
% 17.69/6.75 % (297787)Termination phase: Property scanning
% 17.69/6.75 % (297787)Time elapsed: 0.051 s
% 17.69/6.75 % (297787)Peak memory usage: 84 MB
% 17.69/6.75 % (297787)Instructions burned: 159 (million)
% 17.69/6.75 % (297789)Instruction limit reached!
% 17.69/6.75 % (297789)------------------------------
% 17.69/6.75 % (297789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297789)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297789)Termination reason: Instruction limit
% 17.69/6.75 % (297789)Termination phase: SInE selection
% 17.69/6.75 % (297789)Time elapsed: 0.040 s
% 17.69/6.75 % (297789)Peak memory usage: 83 MB
% 17.69/6.75 % (297789)Instructions burned: 107 (million)
% 17.69/6.75 % (297786)Instruction limit reached!
% 17.69/6.75 % (297786)------------------------------
% 17.69/6.75 % (297786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/6.75 % (297786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/6.75 % (297786)CaDiCaL version: 2.1.3
% 17.69/6.75 % (297786)Termination reason: Instruction limit
% 17.69/6.75 % (297786)Termination phase: Saturation
% 25.43/7.83 % (297786)Time elapsed: 0.092 s
% 25.43/7.83 % (297786)Peak memory usage: 104 MB
% 25.43/7.83 % (297786)Instructions burned: 196 (million)
% 25.43/7.83 % (297794)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=43796509:i=107_2954 on theBenchmark for (2954ds/107Mi)
% 25.43/7.83 % (297795)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3428613264:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2954 on theBenchmark for (2954ds/242Mi)
% 25.43/7.83 % (297796)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=891708975:cond=fast:i=5208:av=off_2954 on theBenchmark for (2954ds/5208Mi)
% 25.43/7.83 % (297794)Instruction limit reached!
% 25.43/7.83 % (297794)------------------------------
% 25.43/7.83 % (297794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.43/7.83 % (297794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.43/7.83 % (297794)CaDiCaL version: 2.1.3
% 25.43/7.83 % (297794)Termination reason: Instruction limit
% 25.43/7.83 % (297794)Termination phase: Saturation
% 25.43/7.83 % (297794)Time elapsed: 0.067 s
% 25.43/7.83 % (297794)Peak memory usage: 114 MB
% 25.43/7.83 % (297794)Instructions burned: 108 (million)
% 25.43/7.83 % (297795)Instruction limit reached!
% 25.43/7.83 % (297795)------------------------------
% 25.43/7.83 % (297795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.43/7.83 % (297795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.43/7.83 % (297795)CaDiCaL version: 2.1.3
% 25.43/7.83 % (297795)Termination reason: Instruction limit
% 25.43/7.83 % (297795)Termination phase: Property scanning
% 25.43/7.83 % (297795)Time elapsed: 0.078 s
% 25.43/7.83 % (297795)Peak memory usage: 84 MB
% 25.43/7.83 % (297795)Instructions burned: 242 (million)
% 25.43/7.83 % (297800)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1699069574:i=134:sd=2:doe=on:ss=axioms:sgt=14_2952 on theBenchmark for (2952ds/134Mi)
% 25.43/7.83 % (297801)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2836736857:i=499:bd=all_2951 on theBenchmark for (2951ds/499Mi)
% 25.43/7.83 % (297800)Instruction limit reached!
% 25.43/7.83 % (297800)------------------------------
% 25.43/7.83 % (297800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.43/7.83 % (297800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.43/7.83 % (297800)CaDiCaL version: 2.1.3
% 25.43/7.83 % (297800)Termination reason: Instruction limit
% 25.43/7.83 % (297800)Termination phase: SInE selection
% 25.43/7.83 % (297800)Time elapsed: 0.050 s
% 25.43/7.83 % (297800)Peak memory usage: 83 MB
% 25.43/7.83 % (297800)Instructions burned: 134 (million)
% 25.43/7.83 % (297804)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3204474012:i=191:fgj=on:bd=all_2950 on theBenchmark for (2950ds/191Mi)
% 25.43/7.83 % (297764)Refutation not found, incomplete strategy
% 25.43/7.83 % (297764)------------------------------
% 25.43/7.83 % (297764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.43/7.83 % (297764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.43/7.83 % (297764)CaDiCaL version: 2.1.3
% 25.43/7.83 % (297764)Termination reason: Refutation not found, incomplete strategy
% 25.43/7.83 % (297764)Time elapsed: 1.081 s
% 25.43/7.83 % (297764)Peak memory usage: 143 MB
% 25.43/7.83 % (297764)Instructions burned: 4111 (million)
% 25.43/7.83 % (297801)Instruction limit reached!
% 25.43/7.83 % (297801)------------------------------
% 25.43/7.83 % (297801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.43/7.83 % (297801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.43/7.83 % (297801)CaDiCaL version: 2.1.3
% 25.43/7.83 % (297801)Termination reason: Instruction limit
% 25.43/7.83 % (297801)Termination phase: Saturation
% 25.43/7.83 % (297801)Time elapsed: 0.219 s
% 25.43/7.83 % (297801)Peak memory usage: 123 MB
% 25.43/7.83 % (297801)Instructions burned: 500 (million)
% 25.43/7.83 % (297804)Instruction limit reached!
% 25.43/7.83 % (297804)------------------------------
% 25.43/7.83 % (297804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.43/7.83 % (297804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.43/7.83 % (297804)CaDiCaL version: 2.1.3
% 25.43/7.83 % (297804)Termination reason: Instruction limit
% 32.69/8.87 % (297804)Termination phase: Saturation
% 32.69/8.87 % (297804)Time elapsed: 0.090 s
% 32.69/8.87 % (297804)Peak memory usage: 105 MB
% 32.69/8.87 % (297804)Instructions burned: 193 (million)
% 32.69/8.87 % (297806)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3534752338:i=264:kws=precedence:fsr=off_2948 on theBenchmark for (2948ds/264Mi)
% 32.69/8.87 % (297764)------------------------------
% 32.69/8.87 % (297764)------------------------------
% 32.69/8.87 % (297807)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2046884950:cond=on:i=156:bs=on:gtg=exists_all:er=known_2947 on theBenchmark for (2947ds/156Mi)
% 32.69/8.87 % (297807)Instruction limit reached!
% 32.69/8.87 % (297807)------------------------------
% 32.69/8.87 % (297807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.69/8.87 % (297807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.69/8.87 % (297807)CaDiCaL version: 2.1.3
% 32.69/8.87 % (297807)Termination reason: Instruction limit
% 32.69/8.87 % (297807)Termination phase: Property scanning
% 32.69/8.87 % (297807)Time elapsed: 0.050 s
% 32.69/8.87 % (297807)Peak memory usage: 84 MB
% 32.69/8.87 % (297807)Instructions burned: 156 (million)
% 32.69/8.87 % (297809)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=3221697329:i=3256:kws=precedence:bd=preordered:av=off_2946 on theBenchmark for (2946ds/3256Mi)
% 32.69/8.87 % (297806)Instruction limit reached!
% 32.69/8.87 % (297806)------------------------------
% 32.69/8.87 % (297806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.69/8.87 % (297806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.69/8.87 % (297806)CaDiCaL version: 2.1.3
% 32.69/8.87 % (297806)Termination reason: Instruction limit
% 32.69/8.87 % (297806)Termination phase: Saturation
% 32.69/8.87 % (297806)Time elapsed: 0.188 s
% 32.69/8.87 % (297806)Peak memory usage: 144 MB
% 32.69/8.87 % (297806)Instructions burned: 265 (million)
% 32.69/8.87 % (297811)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2529246895:i=537:av=off:ss=included_2945 on theBenchmark for (2945ds/537Mi)
% 32.69/8.87 % (297813)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2564725752:i=180:bd=preordered:av=off_2944 on theBenchmark for (2944ds/180Mi)
% 32.69/8.87 % (297813)Instruction limit reached!
% 32.69/8.87 % (297813)------------------------------
% 32.69/8.87 % (297813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.69/8.87 % (297813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.69/8.87 % (297813)CaDiCaL version: 2.1.3
% 32.69/8.87 % (297813)Termination reason: Instruction limit
% 32.69/8.87 % (297813)Termination phase: Saturation
% 32.69/8.87 % (297813)Time elapsed: 0.083 s
% 32.69/8.87 % (297813)Peak memory usage: 104 MB
% 32.69/8.87 % (297813)Instructions burned: 180 (million)
% 32.69/8.87 % (297811)Instruction limit reached!
% 32.69/8.87 % (297811)------------------------------
% 32.69/8.87 % (297811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.69/8.87 % (297811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.69/8.87 % (297811)CaDiCaL version: 2.1.3
% 32.69/8.87 % (297811)Termination reason: Instruction limit
% 32.69/8.87 % (297811)Termination phase: Property scanning
% 32.69/8.87 % (297811)Time elapsed: 0.191 s
% 32.69/8.87 % (297811)Peak memory usage: 84 MB
% 32.69/8.87 % (297811)Instructions burned: 540 (million)
% 32.69/8.87 % (297816)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=4034028193:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2942 on theBenchmark for (2942ds/10307Mi)
% 32.69/8.87 % (297817)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=3653215219:i=412:gtgl=4:gtg=exists_all_2942 on theBenchmark for (2942ds/412Mi)
% 32.69/8.87 % (297788)Instruction limit reached!
% 32.69/8.87 % (297788)------------------------------
% 32.69/8.87 % (297788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.69/8.87 % (297788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.69/8.87 % (297788)CaDiCaL version: 2.1.3
% 32.69/8.87 % (297788)Termination reason: Instruction limit
% 32.69/8.87 % (297788)Termination phase: Saturation
% 32.69/8.87 % (297788)Time elapsed: 1.431 s
% 32.69/8.87 % (297788)Peak memory usage: 119 MB
% 35.87/9.26 % (297788)Instructions burned: 3395 (million)
% 35.87/9.26 % (297817)Instruction limit reached!
% 35.87/9.26 % (297817)------------------------------
% 35.87/9.26 % (297817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297817)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297817)Termination reason: Instruction limit
% 35.87/9.26 % (297817)Termination phase: Property scanning
% 35.87/9.26 % (297817)Time elapsed: 0.133 s
% 35.87/9.26 % (297817)Peak memory usage: 84 MB
% 35.87/9.26 % (297817)Instructions burned: 414 (million)
% 35.87/9.26 % (297820)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=2418490695:s2pl=no:i=8478:s2at=4:nm=6_2940 on theBenchmark for (2940ds/8478Mi)
% 35.87/9.26 % (297809)Instruction limit reached!
% 35.87/9.26 % (297809)------------------------------
% 35.87/9.26 % (297809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297809)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297809)Termination reason: Instruction limit
% 35.87/9.26 % (297809)Termination phase: Saturation
% 35.87/9.26 % (297809)Time elapsed: 0.758 s
% 35.87/9.26 % (297809)Peak memory usage: 136 MB
% 35.87/9.26 % (297809)Instructions burned: 3256 (million)
% 35.87/9.26 % (297821)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=2492330644:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2939 on theBenchmark for (2939ds/303Mi)
% 35.87/9.26 % (297821)Instruction limit reached!
% 35.87/9.26 % (297821)------------------------------
% 35.87/9.26 % (297821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297821)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297821)Termination reason: Instruction limit
% 35.87/9.26 % (297821)Termination phase: SInE selection
% 35.87/9.26 % (297821)Time elapsed: 0.114 s
% 35.87/9.26 % (297821)Peak memory usage: 83 MB
% 35.87/9.26 % (297821)Instructions burned: 305 (million)
% 35.87/9.26 % (297823)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4022144870:st=4:i=720:sd=3:fsr=off:ss=axioms_2937 on theBenchmark for (2937ds/720Mi)
% 35.87/9.26 % (297823)Instruction limit reached!
% 35.87/9.26 % (297823)------------------------------
% 35.87/9.26 % (297823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297823)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297823)Termination reason: Instruction limit
% 35.87/9.26 % (297823)Termination phase: Property scanning
% 35.87/9.26 % (297823)Time elapsed: 0.134 s
% 35.87/9.26 % (297823)Peak memory usage: 84 MB
% 35.87/9.26 % (297823)Instructions burned: 725 (million)
% 35.87/9.26 % (297825)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3026766708:i=598:bs=on:bd=preordered:av=off:ss=axioms_2936 on theBenchmark for (2936ds/598Mi)
% 35.87/9.26 % (297827)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=206310598:i=2989:sd=3:ss=axioms:sgt=60_2935 on theBenchmark for (2935ds/2989Mi)
% 35.87/9.26 % (297825)Instruction limit reached!
% 35.87/9.26 % (297825)------------------------------
% 35.87/9.26 % (297825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297825)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297825)Termination reason: Instruction limit
% 35.87/9.26 % (297825)Termination phase: Property scanning
% 35.87/9.26 % (297825)Time elapsed: 0.210 s
% 35.87/9.26 % (297825)Peak memory usage: 84 MB
% 35.87/9.26 % (297825)Instructions burned: 599 (million)
% 35.87/9.26 % (297830)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=330470977:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2932 on theBenchmark for (2932ds/1997Mi)
% 35.87/9.26 % (297796)Instruction limit reached!
% 35.87/9.26 % (297796)------------------------------
% 35.87/9.26 % (297796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297796)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297796)Termination reason: Instruction limit
% 35.87/9.26 % (297796)Termination phase: Saturation
% 35.87/9.26 % (297796)Time elapsed: 2.278 s
% 35.87/9.26 % (297796)Peak memory usage: 142 MB
% 35.87/9.26 % (297796)Instructions burned: 5209 (million)
% 35.87/9.26 % (297832)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=3275925219:i=2088:bd=preordered:av=off_2929 on theBenchmark for (2929ds/2088Mi)
% 35.87/9.26 % (297827)Instruction limit reached!
% 35.87/9.26 % (297827)------------------------------
% 35.87/9.26 % (297827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297827)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297827)Termination reason: Instruction limit
% 35.87/9.26 % (297827)Termination phase: Saturation
% 35.87/9.26 % (297827)Time elapsed: 0.628 s
% 35.87/9.26 % (297827)Peak memory usage: 104 MB
% 35.87/9.26 % (297827)Instructions burned: 2991 (million)
% 35.87/9.26 % (297834)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=826494190:i=1098:nicw=on_2927 on theBenchmark for (2927ds/1098Mi)
% 35.87/9.26 % (297830)Instruction limit reached!
% 35.87/9.26 % (297830)------------------------------
% 35.87/9.26 % (297830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297830)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297830)Termination reason: Instruction limit
% 35.87/9.26 % (297830)Termination phase: Initialization
% 35.87/9.26 % (297830)Time elapsed: 0.635 s
% 35.87/9.26 % (297830)Peak memory usage: 84 MB
% 35.87/9.26 % (297830)Instructions burned: 1998 (million)
% 35.87/9.26 % (297834)Instruction limit reached!
% 35.87/9.26 % (297834)------------------------------
% 35.87/9.26 % (297834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297834)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297834)Termination reason: Instruction limit
% 35.87/9.26 % (297834)Termination phase: Saturation
% 35.87/9.26 % (297834)Time elapsed: 0.273 s
% 35.87/9.26 % (297834)Peak memory usage: 159 MB
% 35.87/9.26 % (297834)Instructions burned: 1103 (million)
% 35.87/9.26 % (297836)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3021504463:i=433:bd=preordered_2924 on theBenchmark for (2924ds/433Mi)
% 35.87/9.26 % (297837)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4273203376:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2923 on theBenchmark for (2923ds/2942Mi)
% 35.87/9.26 % (297836)Instruction limit reached!
% 35.87/9.26 % (297836)------------------------------
% 35.87/9.26 % (297836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297836)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297836)Termination reason: Instruction limit
% 35.87/9.26 % (297836)Termination phase: Twee Goal Transformation
% 35.87/9.26 % (297836)Time elapsed: 0.172 s
% 35.87/9.26 % (297836)Peak memory usage: 93 MB
% 35.87/9.26 % (297836)Instructions burned: 434 (million)
% 35.87/9.26 % (297832)Instruction limit reached!
% 35.87/9.26 % (297832)------------------------------
% 35.87/9.26 % (297832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297832)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297832)Termination reason: Instruction limit
% 35.87/9.26 % (297832)Termination phase: Property scanning
% 35.87/9.26 % (297832)Time elapsed: 0.694 s
% 35.87/9.26 % (297832)Peak memory usage: 84 MB
% 35.87/9.26 % (297832)Instructions burned: 2088 (million)
% 35.87/9.26 % (297840)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2968784728:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2921 on theBenchmark for (2921ds/6922Mi)
% 35.87/9.26 % (297841)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1108834991:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2920 on theBenchmark for (2920ds/596Mi)
% 35.87/9.26 % (297816)First to succeed.
% 35.87/9.26 % (297816)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-297759"
% 35.87/9.26 % (297837)Instruction limit reached!
% 35.87/9.26 % (297837)------------------------------
% 35.87/9.26 % (297837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297837)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297837)Termination reason: Instruction limit
% 35.87/9.26 % (297837)Termination phase: Property scanning
% 35.87/9.26 % (297837)Time elapsed: 0.498 s
% 35.87/9.26 % (297837)Peak memory usage: 84 MB
% 35.87/9.26 % (297837)Instructions burned: 2949 (million)
% 35.87/9.26 % (297841)Instruction limit reached!
% 35.87/9.26 % (297841)------------------------------
% 35.87/9.26 % (297841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297841)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297841)Termination reason: Instruction limit
% 35.87/9.26 % (297841)Termination phase: Property scanning
% 35.87/9.26 % (297841)Time elapsed: 0.192 s
% 35.87/9.26 % (297841)Peak memory usage: 84 MB
% 35.87/9.26 % (297841)Instructions burned: 599 (million)
% 35.87/9.26 % (297844)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2975100708:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2917 on theBenchmark for (2917ds/4123Mi)
% 35.87/9.26 % (297820)Refutation not found, incomplete strategy
% 35.87/9.26 % (297820)------------------------------
% 35.87/9.26 % (297820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/9.26 % (297820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/9.26 % (297820)CaDiCaL version: 2.1.3
% 35.87/9.26 % (297820)Termination reason: Refutation not found, incomplete strategy
% 35.87/9.26 % (297820)Time elapsed: 2.304 s
% 35.87/9.26 % (297820)Peak memory usage: 148 MB
% 35.87/9.26 % (297820)Instructions burned: 4653 (million)
% 35.87/9.26 % (297845)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2684037232:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2917 on theBenchmark for (2917ds/16411Mi)
% 35.87/9.26 % SZS status Satisfiable for theBenchmark
% 35.87/9.26 % SZS output start Saturation.
% See solution above
% 0.32/9.50 % SZS output start Definitions and Model Updates.
% 0.32/9.50 % SZS output end Definitions and Model Updates.
% 0.32/9.50 % (297816)------------------------------
% 0.32/9.50 % (297816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.32/9.50 % (297816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/9.50 % (297816)CaDiCaL version: 2.1.3
% 0.32/9.50 % (297816)Termination reason: Satisfiable
% 0.32/9.50 % (297816)Time elapsed: 2.236 s
% 0.32/9.50 % (297816)Peak memory usage: 146 MB
% 0.32/9.50 % (297816)Instructions burned: 4660 (million)
% 0.32/9.50 % (297816)------------------------------
% 0.32/9.50 % (297816)------------------------------
% 0.32/9.50 % (297759)Success in time 8.468 s
% 0.32/9.50 % Vampire exiting
%------------------------------------------------------------------------------