%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV532-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 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:24:55 PM UTC 2026
% Result : Satisfiable 6.13s 1.20s
% Output : Saturation 6.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u173,axiom,
sF0 = select(sF1,i3) ).
cnf(u182,axiom,
i3 != i1 ).
cnf(u187,axiom,
sF4 = select(sF1,i1) ).
cnf(u191,axiom,
i3 != i2 ).
cnf(u196,axiom,
sF6 = select(sF1,i2) ).
cnf(u266,axiom,
sF8 = select(sF5,i5) ).
cnf(u269,axiom,
i3 != i5 ).
cnf(u274,axiom,
sF10 != select(sF5,i0) ).
cnf(u278,axiom,
i3 != i0 ).
cnf(u291,axiom,
i1 = i0 ).
cnf(u402,axiom,
sF29 = select(sF27,i0) ).
cnf(u509,axiom,
sF46 = select(sF41,i6) ).
cnf(u520,axiom,
i2 != i1 ).
cnf(u525,axiom,
sF19 = select(sF17,i2) ).
cnf(u548,axiom,
sF37 = select(sF34,i1) ).
cnf(u554,axiom,
sF16 = select(sF11,i1) ).
cnf(u560,axiom,
sF40 = select(sF38,i2) ).
cnf(u568,axiom,
i2 = i6 ).
cnf(u627,axiom,
sF46 = select(sF39,i6) ).
cnf(u637,axiom,
i2 = i5 ).
cnf(u661,axiom,
sF19 = sF25 ).
cnf(u1035,axiom,
sF29 = sF33 ).
cnf(u1041,axiom,
sF29 = sF35 ).
cnf(u1120,axiom,
sF20 = store(sF18,i2,sF14) ).
cnf(u1233,axiom,
( select(sF39,X0) = select(sF41,X0)
| i2 = X0 ) ).
cnf(u75,axiom,
select(sF32,i5) = sF35 ).
cnf(u55,axiom,
select(sF22,i5) = sF25 ).
cnf(u135,axiom,
( select(sF13,X0) = select(sF15,X0)
| i5 = X0 ) ).
cnf(u1070,axiom,
sF16 = select(sF13,i1) ).
cnf(u710,axiom,
sF42 = sF46 ).
cnf(u138,axiom,
( select(sF18,X0) = select(sF20,X0)
| i5 = X0 ) ).
cnf(u37,axiom,
select(sF15,i1) = sF16 ).
cnf(u49,axiom,
store(sF20,i2,sF21) = sF22 ).
cnf(u81,axiom,
store(sF36,i1,sF37) = sF38 ).
cnf(u109,axiom,
sF14 = select(sF15,i5) ).
cnf(u1357,axiom,
sF22 = store(sF20,i2,sF6) ).
cnf(u1272,axiom,
sF4 = select(sF39,i1) ).
cnf(u112,axiom,
sF19 = select(sF20,i5) ).
cnf(u63,axiom,
select(sF28,i0) = sF29 ).
cnf(u7,axiom,
store(a1,i4,sF0) = sF1 ).
cnf(u1384,axiom,
sF6 = select(sF24,i2) ).
cnf(u1161,axiom,
sF4 = sF16 ).
cnf(u142,axiom,
( select(sF27,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u25,axiom,
select(sF7,i0) = sF10 ).
cnf(u1118,axiom,
sF26 = store(sF24,i2,sF14) ).
cnf(u85,axiom,
select(sF39,i2) = sF40 ).
cnf(u129,axiom,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0 ) ).
cnf(u157,axiom,
sF21 = sF23 ).
cnf(u1024,axiom,
sF33 = sF35 ).
cnf(u1107,axiom,
sF6 != select(sF5,i1) ).
cnf(u116,axiom,
sF4 = select(sF28,i2) ).
cnf(u148,axiom,
( select(sF38,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u160,axiom,
sF42 = sF44 ).
cnf(u51,axiom,
select(sF22,i2) = sF23 ).
cnf(u1191,axiom,
sF6 = select(sF36,i2) ).
cnf(u111,axiom,
sF16 = select(sF18,i1) ).
cnf(u1198,axiom,
sF6 = sF33 ).
cnf(u1194,axiom,
( select(sF28,X0) = select(sF30,X0)
| i2 = X0 ) ).
cnf(u1256,axiom,
sF6 = select(sF26,i2) ).
cnf(u785,axiom,
sF43 = store(sF41,i2,sF40) ).
cnf(u114,axiom,
sF23 = select(sF24,i5) ).
cnf(u730,axiom,
sF15 = store(sF13,i2,sF14) ).
cnf(u758,axiom,
sF19 = sF21 ).
cnf(u781,axiom,
sF9 = store(sF7,i0,sF4) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u29,axiom,
select(sF11,i5) = sF12 ).
cnf(u745,axiom,
sF29 = select(sF30,i2) ).
cnf(u73,axiom,
store(sF32,i5,sF33) = sF34 ).
cnf(u133,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u1065,axiom,
sF4 = select(sF7,i2) ).
cnf(u788,axiom,
sF32 = store(sF30,i0,sF4) ).
cnf(u136,axiom,
( select(sF15,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u792,axiom,
sF22 = store(sF20,i2,sF19) ).
cnf(u1241,axiom,
sF6 = select(sF47,i2) ).
cnf(u99,axiom,
store(sF45,i2,sF46) = sF47 ).
cnf(u1174,axiom,
( select(sF30,X0) = select(sF32,X0)
| i1 = X0 ) ).
cnf(u778,axiom,
sF47 = store(sF45,i2,sF40) ).
cnf(u1085,axiom,
sF4 = select(sF32,i1) ).
cnf(u747,axiom,
sF40 = select(sF41,i2) ).
cnf(u118,axiom,
sF31 = select(sF32,i0) ).
cnf(u743,axiom,
sF19 = select(sF20,i2) ).
cnf(u755,axiom,
sF4 = sF31 ).
cnf(u161,axiom,
sF45 = store(sF43,i6,sF42) ).
cnf(u978,axiom,
sF19 = select(sF26,i2) ).
cnf(u5,axiom,
select(a1,i3) = sF0 ).
cnf(u77,axiom,
store(sF34,i2,sF35) = sF36 ).
cnf(u1363,axiom,
sF6 = select(sF22,i2) ).
cnf(u1066,axiom,
sF24 = store(sF22,i2,sF19) ).
cnf(u1219,axiom,
( select(sF13,X0) = select(sF15,X0)
| i2 = X0 ) ).
cnf(u140,axiom,
( select(sF22,X0) = select(sF24,X0)
| i5 = X0 ) ).
cnf(u31,axiom,
store(sF11,i2,sF12) = sF13 ).
cnf(u43,axiom,
select(sF18,i2) = sF19 ).
cnf(u1116,axiom,
sF14 = sF19 ).
cnf(u103,axiom,
sF4 = select(sF5,i2) ).
cnf(u1096,axiom,
sF34 = store(sF32,i2,sF6) ).
cnf(u147,axiom,
( select(sF36,X0) = select(sF38,X0)
| i1 = X0 ) ).
cnf(u751,axiom,
sF21 = select(sF24,i2) ).
cnf(u1222,axiom,
( select(sF18,X0) = select(sF20,X0)
| i2 = X0 ) ).
cnf(u106,axiom,
sF8 = select(sF9,i0) ).
cnf(u731,axiom,
sF20 = store(sF18,i2,sF19) ).
cnf(u121,axiom,
sF37 = select(sF38,i1) ).
cnf(u737,axiom,
sF34 = store(sF32,i2,sF33) ).
cnf(u1144,axiom,
sF41 = store(sF39,i2,sF6) ).
cnf(u1089,axiom,
sF6 = sF10 ).
cnf(u128,axiom,
( select(sF1,X0) = select(sF3,X0)
| i3 = X0 ) ).
cnf(u19,axiom,
store(sF5,i1,sF6) = sF7 ).
cnf(u79,axiom,
select(sF36,i1) = sF37 ).
cnf(u91,axiom,
store(sF41,i2,sF42) = sF43 ).
cnf(u1216,axiom,
( select(sF9,X0) = select(sF11,X0)
| i2 = X0 ) ).
cnf(u151,axiom,
( select(sF43,X0) = select(sF45,X0)
| i6 = X0 ) ).
cnf(u110,axiom,
sF16 = select(sF17,i1) ).
cnf(u1238,axiom,
sF47 = store(sF45,i2,sF6) ).
cnf(u735,axiom,
sF30 = store(sF28,i2,sF29) ).
cnf(u154,axiom,
sF10 = sF12 ).
cnf(u53,axiom,
store(sF22,i5,sF23) = sF24 ).
cnf(u1247,axiom,
sF6 = select(sF11,i2) ).
cnf(u739,axiom,
sF41 = store(sF39,i2,sF40) ).
cnf(u97,axiom,
select(sF43,i6) = sF46 ).
cnf(u125,axiom,
sF44 = select(sF45,i6) ).
cnf(u741,axiom,
sF10 = select(sF11,i2) ).
cnf(u1348,axiom,
sF6 = sF44 ).
cnf(u933,axiom,
sF40 = sF46 ).
cnf(u1141,axiom,
sF6 = sF40 ).
cnf(u1090,axiom,
sF9 = store(sF7,i1,sF4) ).
cnf(u1251,axiom,
sF6 = sF42 ).
cnf(u23,axiom,
store(sF7,i0,sF8) = sF9 ).
cnf(u67,axiom,
select(sF28,i5) = sF31 ).
cnf(u139,axiom,
( select(sF20,X0) = select(sF22,X0)
| i2 = X0 ) ).
cnf(u1088,axiom,
sF6 = select(sF28,i1) ).
cnf(u130,axiom,
( select(sF3,X0) = select(sF27,X0)
| i1 = X0 ) ).
cnf(u158,axiom,
sF24 = store(sF22,i5,sF21) ).
cnf(u41,axiom,
store(sF17,i1,sF16) = sF18 ).
cnf(u101,axiom,
sF0 = select(sF1,i4) ).
cnf(u1258,axiom,
sF45 = store(sF43,i2,sF6) ).
cnf(u145,axiom,
( select(sF32,X0) = select(sF34,X0)
| i5 = X0 ) ).
cnf(u104,axiom,
sF6 = select(sF27,i1) ).
cnf(u1195,axiom,
sF6 = select(sF30,i2) ).
cnf(u127,axiom,
( select(a1,X0) = select(sF1,X0)
| i4 = X0 ) ).
cnf(u11,axiom,
store(sF1,i3,sF2) = sF3 ).
cnf(u71,axiom,
select(sF32,i2) = sF33 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u746,axiom,
sF33 = select(sF34,i2) ).
cnf(u1101,axiom,
sF13 = store(sF11,i2,sF6) ).
cnf(u134,axiom,
( select(sF11,X0) = select(sF13,X0)
| i2 = X0 ) ).
cnf(u17,axiom,
select(sF3,i2) = sF6 ).
cnf(u45,axiom,
store(sF18,i5,sF19) = sF20 ).
cnf(u89,axiom,
select(sF39,i5) = sF42 ).
cnf(u149,axiom,
( select(sF39,X0) = select(sF41,X0)
| i5 = X0 ) ).
cnf(u1243,axiom,
sF6 = select(sF13,i2) ).
cnf(u1289,axiom,
sF6 = sF25 ).
cnf(u47,axiom,
select(sF18,i5) = sF21 ).
cnf(u108,axiom,
sF12 = select(sF13,i2) ).
cnf(u152,axiom,
( select(sF45,X0) = select(sF47,X0)
| i2 = X0 ) ).
cnf(u1086,axiom,
sF4 = select(sF9,i1) ).
cnf(u115,axiom,
sF25 = select(sF26,i2) ).
cnf(u1185,axiom,
sF15 = store(sF13,i2,sF6) ).
cnf(u1201,axiom,
sF6 = sF35 ).
cnf(u750,axiom,
sF4 = sF8 ).
cnf(u1186,axiom,
( select(sF32,X0) = select(sF34,X0)
| i2 = X0 ) ).
cnf(u1111,axiom,
sF4 != sF6 ).
cnf(u1277,axiom,
sF4 = select(sF38,i1) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u33,axiom,
select(sF11,i2) = sF14 ).
cnf(u65,axiom,
store(sF28,i5,sF29) = sF30 ).
cnf(u93,axiom,
select(sF43,i2) = sF44 ).
cnf(u709,axiom,
sF42 = select(sF45,i2) ).
cnf(u137,axiom,
( select(sF17,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u767,axiom,
sF26 = store(sF24,i2,sF19) ).
cnf(u1129,axiom,
sF39 = store(sF38,i1,sF4) ).
cnf(u83,axiom,
store(sF38,i1,sF37) = sF39 ).
cnf(u59,axiom,
store(sF3,i1,sF6) = sF27 ).
cnf(u119,axiom,
sF33 = select(sF34,i5) ).
cnf(u1373,axiom,
sF24 = store(sF22,i2,sF6) ).
cnf(u163,axiom,
sF10 = select(sF13,i2) ).
cnf(u1285,axiom,
sF6 = select(sF41,i2) ).
cnf(u1077,axiom,
sF6 = sF29 ).
cnf(u960,axiom,
sF45 = store(sF43,i2,sF40) ).
cnf(u122,axiom,
sF37 = select(sF39,i1) ).
cnf(u1253,axiom,
sF26 = store(sF24,i2,sF6) ).
cnf(u1164,axiom,
sF17 = store(sF15,i1,sF4) ).
cnf(u9,axiom,
select(a1,i4) = sF2 ).
cnf(u961,axiom,
( select(sF43,X0) = select(sF45,X0)
| i2 = X0 ) ).
cnf(u753,axiom,
sF40 = sF42 ).
cnf(u69,axiom,
store(sF30,i0,sF31) = sF32 ).
cnf(u141,axiom,
( select(sF24,X0) = select(sF26,X0)
| i2 = X0 ) ).
cnf(u100,negated_conjecture,
sF26 != sF47 ).
cnf(u1422,axiom,
sF6 = select(sF15,i2) ).
cnf(u132,axiom,
( select(sF7,X0) = select(sF9,X0)
| i0 = X0 ) ).
cnf(u144,axiom,
( select(sF30,X0) = select(sF32,X0)
| i0 = X0 ) ).
cnf(u35,axiom,
store(sF13,i5,sF14) = sF15 ).
cnf(u1103,axiom,
sF11 = store(sF9,i2,sF6) ).
cnf(u95,axiom,
store(sF43,i6,sF44) = sF45 ).
cnf(u107,axiom,
sF10 = select(sF11,i5) ).
cnf(u1182,axiom,
( select(sF7,X0) = select(sF9,X0)
| i1 = X0 ) ).
cnf(u1087,axiom,
sF32 = store(sF30,i1,sF4) ).
cnf(u1261,axiom,
sF43 = store(sF41,i2,sF6) ).
cnf(u1367,axiom,
sF6 = sF23 ).
cnf(u126,axiom,
sF46 = select(sF47,i2) ).
cnf(u742,axiom,
sF14 = select(sF15,i2) ).
cnf(u1100,axiom,
sF30 = store(sF28,i2,sF6) ).
cnf(u1263,axiom,
sF20 = store(sF18,i2,sF6) ).
cnf(u113,axiom,
sF21 = select(sF22,i2) ).
cnf(u13,axiom,
select(sF3,i1) = sF4 ).
cnf(u1127,axiom,
sF4 = sF37 ).
cnf(u757,axiom,
sF24 = store(sF22,i2,sF21) ).
cnf(u1266,axiom,
sF6 = select(sF20,i2) ).
cnf(u1130,axiom,
sF38 = store(sF36,i1,sF4) ).
cnf(u1371,axiom,
sF6 = select(sF45,i2) ).
cnf(u1344,axiom,
sF6 = select(sF43,i2) ).
cnf(u1396,axiom,
sF4 = select(sF17,i1) ).
cnf(u39,axiom,
store(sF15,i1,sF16) = sF17 ).
cnf(u1288,axiom,
sF6 = sF19 ).
cnf(u143,axiom,
( select(sF28,X0) = select(sF30,X0)
| i5 = X0 ) ).
cnf(u155,axiom,
sF13 = store(sF11,i2,sF10) ).
cnf(u102,axiom,
sF2 = select(sF3,i3) ).
cnf(u146,axiom,
( select(sF34,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u57,axiom,
store(sF24,i2,sF25) = sF26 ).
cnf(u1245,axiom,
sF6 = sF46 ).
cnf(u117,axiom,
sF29 = select(sF30,i5) ).
cnf(u15,axiom,
store(sF3,i2,sF4) = sF5 ).
cnf(u1236,axiom,
( select(sF22,X0) = select(sF24,X0)
| i2 = X0 ) ).
cnf(u120,axiom,
sF35 = select(sF36,i2) ).
cnf(u1163,axiom,
sF18 = store(sF17,i1,sF4) ).
cnf(u123,axiom,
sF40 = select(sF41,i5) ).
cnf(u728,axiom,
sF11 = store(sF9,i2,sF10) ).
cnf(u27,axiom,
store(sF9,i5,sF10) = sF11 ).
cnf(u1390,axiom,
sF4 = select(sF18,i1) ).
cnf(u87,axiom,
store(sF39,i5,sF40) = sF41 ).
cnf(u708,axiom,
sF45 = store(sF43,i2,sF42) ).
cnf(u131,axiom,
( select(sF5,X0) = select(sF7,X0)
| i1 = X0 ) ).
cnf(u1366,axiom,
sF6 = sF21 ).
cnf(u150,axiom,
( select(sF41,X0) = select(sF43,X0)
| i2 = X0 ) ).
cnf(u61,axiom,
store(sF27,i2,sF4) = sF28 ).
cnf(u1098,axiom,
sF36 = store(sF34,i2,sF6) ).
cnf(u105,axiom,
sF6 = select(sF7,i1) ).
cnf(u1180,axiom,
sF6 = sF14 ).
cnf(u1270,axiom,
sF6 = sF12 ).
cnf(u124,axiom,
sF42 = select(sF43,i2) ).
cnf(u1187,axiom,
sF6 = select(sF34,i2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV532-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.25 % Computer : n015.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.26 % DateTime : Mon Sep 28 11:38:02 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.30 Running first-order model finding
% 0.25/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.05/1.20 % (2564887)Will run a generic schedule for satisfiability detection.
% 5.05/1.20 % (2564894)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=392606782:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.05/1.20 % (2564893)% WARNING: option uhcvi not known.
% 5.05/1.20 % (2564898)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4142651889:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.05/1.20 % (2564895)dis+10_1_sil=32000:sp=arity:random_seed=2431469992:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.05/1.20 % (2564892)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2940382767_2999 on theBenchmark for (2999ds/0Mi)
% 5.05/1.20 % (2564897)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2997835345:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.05/1.20 % (2564896)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3743614652:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.05/1.20 % (2564893)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2222363439:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.05/1.20 % TRYING [1]
% 5.05/1.20 % TRYING [2]
% 5.05/1.20 % TRYING [3]
% 5.05/1.20 % TRYING [4]
% 5.05/1.20 % TRYING [5]
% 5.05/1.20 % (2564897)Instruction limit reached!
% 5.05/1.20 % (2564897)------------------------------
% 5.05/1.20 % (2564897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564897)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564897)Termination reason: Instruction limit
% 5.05/1.20 % (2564897)Termination phase: Saturation
% 5.05/1.20 % (2564897)Time elapsed: 0.086 s
% 5.05/1.20 % (2564897)Peak memory usage: 14 MB
% 5.05/1.20 % (2564897)Instructions burned: 131 (million)
% 5.05/1.20 % (2564896)Instruction limit reached!
% 5.05/1.20 % (2564896)------------------------------
% 5.05/1.20 % (2564896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564896)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564896)Termination reason: Instruction limit
% 5.05/1.20 % (2564896)Termination phase: Saturation
% 5.05/1.20 % (2564896)Time elapsed: 0.091 s
% 5.05/1.20 % (2564896)Peak memory usage: 14 MB
% 5.05/1.20 % (2564896)Instructions burned: 120 (million)
% 5.05/1.20 % TRYING [6]
% 5.05/1.20 % (2564898)Instruction limit reached!
% 5.05/1.20 % (2564898)------------------------------
% 5.05/1.20 % (2564898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564898)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564898)Termination reason: Instruction limit
% 5.05/1.20 % (2564898)Termination phase: Saturation
% 5.05/1.20 % (2564898)Time elapsed: 0.106 s
% 5.05/1.20 % (2564898)Peak memory usage: 14 MB
% 5.05/1.20 % (2564898)Instructions burned: 160 (million)
% 5.05/1.20 % (2564895)Instruction limit reached!
% 5.05/1.20 % (2564895)------------------------------
% 5.05/1.20 % (2564895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564895)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564895)Termination reason: Instruction limit
% 5.05/1.20 % (2564895)Termination phase: Saturation
% 5.05/1.20 % (2564895)Time elapsed: 0.108 s
% 5.05/1.20 % (2564895)Peak memory usage: 13 MB
% 5.05/1.20 % (2564895)Instructions burned: 104 (million)
% 5.05/1.20 % (2564907)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=719354375:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.05/1.20 % (2564906)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=879730266:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 5.05/1.20 % TRYING [1]
% 5.05/1.20 % TRYING [2]
% 5.05/1.20 % TRYING [3]
% 5.05/1.20 % (2564908)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1675615158:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 5.05/1.20 % (2564909)ott-21_1_sil=16000:fs=off:random_seed=353672607:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 5.05/1.20 % TRYING [4]
% 5.05/1.20 % TRYING [5]
% 5.05/1.20 % (2564907)Instruction limit reached!
% 5.05/1.20 % (2564907)------------------------------
% 5.05/1.20 % (2564907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564907)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564907)Termination reason: Instruction limit
% 5.05/1.20 % (2564907)Termination phase: Saturation
% 5.05/1.20 % (2564907)Time elapsed: 0.112 s
% 5.05/1.20 % (2564907)Peak memory usage: 14 MB
% 5.05/1.20 % (2564907)Instructions burned: 133 (million)
% 5.05/1.20 % TRYING [7]
% 5.05/1.20 % (2564909)Instruction limit reached!
% 5.05/1.20 % (2564909)------------------------------
% 5.05/1.20 % (2564909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564909)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564909)Termination reason: Instruction limit
% 5.05/1.20 % (2564909)Termination phase: Saturation
% 5.05/1.20 % (2564909)Time elapsed: 0.115 s
% 5.05/1.20 % (2564909)Peak memory usage: 13 MB
% 5.05/1.20 % (2564909)Instructions burned: 181 (million)
% 5.05/1.20 % (2564914)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1119578915:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 5.05/1.20 % (2564916)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3719558433:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 5.05/1.20 % TRYING [1]
% 5.05/1.20 % TRYING [2]
% 5.05/1.20 % TRYING [6]
% 5.05/1.20 % TRYING [3]
% 5.05/1.20 % TRYING [4]
% 5.05/1.20 % TRYING [5]
% 5.05/1.20 % TRYING [6]
% 5.05/1.20 % (2564906)Instruction limit reached!
% 5.05/1.20 % (2564906)------------------------------
% 5.05/1.20 % (2564906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.20 % (2564906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.20 % (2564906)CaDiCaL version: 2.1.3
% 5.05/1.20 % (2564906)Termination reason: Instruction limit
% 5.05/1.20 % (2564906)Termination phase: Finite model building SAT solving
% 5.05/1.20 % (2564906)Time elapsed: 0.567 s
% 5.05/1.20 % (2564906)Peak memory usage: 24 MB
% 5.05/1.20 % (2564906)Instructions burned: 714 (million)
% 5.05/1.20 % TRYING [8]
% 5.05/1.20 % (2564918)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1529595264:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 5.05/1.20 % (2564908)Instruction limit reached!
% 5.05/1.20 % (2564908)------------------------------
% 6.13/1.20 % (2564908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.20 % (2564908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.20 % (2564908)CaDiCaL version: 2.1.3
% 6.13/1.20 % (2564908)Termination reason: Instruction limit
% 6.13/1.20 % (2564908)Termination phase: Saturation
% 6.13/1.20 % (2564908)Time elapsed: 0.584 s
% 6.13/1.20 % (2564908)Peak memory usage: 19 MB
% 6.13/1.20 % (2564908)Instructions burned: 684 (million)
% 6.13/1.20 % (2564914)Instruction limit reached!
% 6.13/1.20 % (2564914)------------------------------
% 6.13/1.20 % (2564914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.20 % (2564914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.20 % (2564914)CaDiCaL version: 2.1.3
% 6.13/1.20 % (2564914)Termination reason: Instruction limit
% 6.13/1.20 % (2564914)Termination phase: Saturation
% 6.13/1.20 % (2564914)Time elapsed: 0.475 s
% 6.13/1.20 % (2564914)Peak memory usage: 25 MB
% 6.13/1.20 % (2564914)Instructions burned: 478 (million)
% 6.13/1.20 % (2564920)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3586120644:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 6.13/1.20 % (2564918) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2564887-2564918"...
% 6.13/1.20 % (2564918)...printing done.
% 6.13/1.20 % SZS status Satisfiable for theBenchmark
% 6.13/1.20 % SZS output start Saturation.
% See solution above
% 6.13/1.21 % SZS output start Definitions and Model Updates.
% 6.13/1.21 % SZS output end Definitions and Model Updates.
% 6.13/1.21 % (2564918)------------------------------
% 6.13/1.21 % (2564918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.21 % (2564918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.21 % (2564918)CaDiCaL version: 2.1.3
% 6.13/1.21 % (2564918)Termination reason: Satisfiable
% 6.13/1.21 % (2564918)Time elapsed: 0.063 s
% 6.13/1.21 % (2564918)Peak memory usage: 12 MB
% 6.13/1.21 % (2564918)Instructions burned: 64 (million)
% 6.13/1.21 % (2564887)Success in time 0.892 s
% 6.13/1.21 % Vampire exiting
%------------------------------------------------------------------------------