%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV531-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:54 PM UTC 2026
% Result : Satisfiable 5.64s 1.19s
% Output : Saturation 5.64s
% 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(u192,axiom,
i3 = i2 ).
cnf(u266,axiom,
sF8 = select(sF5,i5) ).
cnf(u270,axiom,
i3 = i5 ).
cnf(u275,axiom,
sF10 = select(sF5,i0) ).
cnf(u279,axiom,
i3 = i0 ).
cnf(u804,axiom,
sF4 = select(sF41,i3) ).
cnf(u295,axiom,
sF27 = store(sF3,i1,sF2) ).
cnf(u228,axiom,
sF43 = store(sF41,i3,sF42) ).
cnf(u339,axiom,
sF4 = sF31 ).
cnf(u75,axiom,
select(sF32,i5) = sF35 ).
cnf(u524,axiom,
sF33 = sF40 ).
cnf(u135,axiom,
( select(sF13,X0) = select(sF15,X0)
| i5 = X0 ) ).
cnf(u983,axiom,
sF2 = select(sF39,i1) ).
cnf(u370,axiom,
sF19 = select(sF17,i3) ).
cnf(u313,axiom,
sF20 = store(sF18,i3,sF19) ).
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(u502,axiom,
sF14 = sF19 ).
cnf(u81,axiom,
store(sF36,i1,sF37) = sF38 ).
cnf(u109,axiom,
sF14 = select(sF15,i5) ).
cnf(u809,axiom,
sF4 = sF19 ).
cnf(u112,axiom,
sF19 = select(sF20,i5) ).
cnf(u63,axiom,
select(sF28,i0) = sF29 ).
cnf(u216,axiom,
sF5 = store(sF3,i3,sF4) ).
cnf(u7,axiom,
store(a1,i4,sF0) = sF1 ).
cnf(u452,axiom,
sF30 = store(sF28,i3,sF4) ).
cnf(u814,axiom,
sF4 = select(sF24,i3) ).
cnf(u239,axiom,
sF13 = store(sF11,i3,sF10) ).
cnf(u582,axiom,
sF4 = sF33 ).
cnf(u754,axiom,
sF26 = store(sF24,i3,sF4) ).
cnf(u374,axiom,
sF32 = store(sF30,i0,sF4) ).
cnf(u317,axiom,
sF30 = store(sF28,i3,sF29) ).
cnf(u142,axiom,
( select(sF27,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u25,axiom,
select(sF7,i0) = sF10 ).
cnf(u977,axiom,
sF2 = select(sF17,i1) ).
cnf(u85,axiom,
select(sF39,i2) = sF40 ).
cnf(u106,axiom,
sF8 = select(sF9,i0) ).
cnf(u129,axiom,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0 ) ).
cnf(u157,axiom,
sF21 = sF23 ).
cnf(u116,axiom,
sF4 = select(sF28,i2) ).
cnf(u715,axiom,
sF47 = store(sF45,i3,sF4) ).
cnf(u148,axiom,
( select(sF38,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u160,axiom,
sF42 = sF44 ).
cnf(u336,axiom,
sF45 = store(sF43,i3,sF42) ).
cnf(u51,axiom,
select(sF22,i2) = sF23 ).
cnf(u220,axiom,
sF19 = select(sF18,i3) ).
cnf(u331,axiom,
sF40 = select(sF41,i3) ).
cnf(u123,axiom,
sF40 = select(sF41,i5) ).
cnf(u732,axiom,
sF4 = select(sF36,i3) ).
cnf(u391,axiom,
sF4 = sF8 ).
cnf(u790,axiom,
sF4 = sF25 ).
cnf(u227,axiom,
sF40 = select(sF39,i3) ).
cnf(u686,axiom,
( select(sF39,X0) = select(sF41,X0)
| i3 = X0 ) ).
cnf(u114,axiom,
sF23 = select(sF24,i5) ).
cnf(u975,axiom,
sF2 = select(sF18,i1) ).
cnf(u767,axiom,
sF22 = store(sF20,i3,sF4) ).
cnf(u422,axiom,
sF4 = select(sF32,i3) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u29,axiom,
select(sF11,i5) = sF12 ).
cnf(u585,axiom,
sF34 = store(sF32,i3,sF4) ).
cnf(u73,axiom,
store(sF32,i5,sF33) = sF34 ).
cnf(u133,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u689,axiom,
( select(sF43,X0) = select(sF45,X0)
| i3 = X0 ) ).
cnf(u136,axiom,
( select(sF15,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u337,axiom,
sF40 = sF42 ).
cnf(u780,axiom,
sF4 = select(sF11,i3) ).
cnf(u55,axiom,
select(sF22,i5) = sF25 ).
cnf(u99,axiom,
store(sF45,i2,sF46) = sF47 ).
cnf(u787,axiom,
sF4 = select(sF13,i3) ).
cnf(u351,axiom,
sF16 = select(sF13,i1) ).
cnf(u630,axiom,
sF17 = store(sF15,i1,sF2) ).
cnf(u667,axiom,
( select(sF45,X0) = select(sF47,X0)
| i3 = X0 ) ).
cnf(u231,axiom,
sF4 = select(sF5,i3) ).
cnf(u674,axiom,
( select(sF13,X0) = select(sF15,X0)
| i3 = X0 ) ).
cnf(u118,axiom,
sF31 = select(sF32,i0) ).
cnf(u755,axiom,
sF4 = select(sF26,i3) ).
cnf(u338,axiom,
sF33 = sF35 ).
cnf(u774,axiom,
sF4 = select(sF30,i3) ).
cnf(u309,axiom,
sF8 = select(sF7,i3) ).
cnf(u234,axiom,
sF25 = select(sF26,i3) ).
cnf(u341,axiom,
sF24 = store(sF22,i3,sF21) ).
cnf(u5,axiom,
select(a1,i3) = sF0 ).
cnf(u77,axiom,
store(sF34,i2,sF35) = sF36 ).
cnf(u661,axiom,
( select(sF34,X0) = select(sF36,X0)
| i3 = X0 ) ).
cnf(u249,axiom,
sF2 = sF6 ).
cnf(u312,axiom,
sF15 = store(sF13,i3,sF14) ).
cnf(u140,axiom,
( select(sF22,X0) = select(sF24,X0)
| i5 = X0 ) ).
cnf(u592,axiom,
sF16 = select(sF9,i1) ).
cnf(u31,axiom,
store(sF11,i2,sF12) = sF13 ).
cnf(u43,axiom,
select(sF18,i2) = sF19 ).
cnf(u664,axiom,
( select(sF41,X0) = select(sF43,X0)
| i3 = X0 ) ).
cnf(u103,axiom,
sF4 = select(sF5,i2) ).
cnf(u724,axiom,
sF4 = select(sF43,i3) ).
cnf(u147,axiom,
( select(sF36,X0) = select(sF38,X0)
| i1 = X0 ) ).
cnf(u650,axiom,
sF2 = sF37 ).
cnf(u342,axiom,
sF19 = sF21 ).
cnf(u238,axiom,
sF46 = select(sF47,i3) ).
cnf(u329,axiom,
sF29 = select(sF30,i3) ).
cnf(u121,axiom,
sF37 = select(sF38,i1) ).
cnf(u680,axiom,
( select(sF28,X0) = select(sF30,X0)
| i3 = X0 ) ).
cnf(u225,axiom,
sF33 = select(sF32,i3) ).
cnf(u128,axiom,
( select(sF1,X0) = select(sF3,X0)
| i3 = X0 ) ).
cnf(u19,axiom,
store(sF5,i1,sF6) = sF7 ).
cnf(u640,axiom,
( select(sF20,X0) = select(sF22,X0)
| i3 = X0 ) ).
cnf(u79,axiom,
select(sF36,i1) = sF37 ).
cnf(u91,axiom,
store(sF41,i2,sF42) = sF43 ).
cnf(u795,axiom,
sF4 = select(sF20,i3) ).
cnf(u151,axiom,
( select(sF43,X0) = select(sF45,X0)
| i5 = X0 ) ).
cnf(u110,axiom,
sF16 = select(sF17,i1) ).
cnf(u735,axiom,
sF4 = sF42 ).
cnf(u154,axiom,
sF10 = sF12 ).
cnf(u330,axiom,
sF33 = select(sF34,i3) ).
cnf(u53,axiom,
store(sF22,i5,sF23) = sF24 ).
cnf(u97,axiom,
select(sF43,i5) = sF46 ).
cnf(u125,axiom,
sF44 = select(sF45,i5) ).
cnf(u505,axiom,
sF20 = store(sF18,i3,sF14) ).
cnf(u727,axiom,
sF4 = sF46 ).
cnf(u461,axiom,
sF37 = select(sF34,i1) ).
cnf(u23,axiom,
store(sF7,i0,sF8) = sF9 ).
cnf(u823,axiom,
sF4 = select(sF45,i3) ).
cnf(u67,axiom,
select(sF28,i5) = sF31 ).
cnf(u653,axiom,
( select(sF24,X0) = select(sF26,X0)
| i3 = X0 ) ).
cnf(u139,axiom,
( select(sF20,X0) = select(sF22,X0)
| i2 = X0 ) ).
cnf(u598,axiom,
sF37 = select(sF30,i1) ).
cnf(u656,axiom,
sF39 = store(sF38,i1,sF2) ).
cnf(u45,axiom,
store(sF18,i5,sF19) = sF20 ).
cnf(u130,axiom,
( select(sF3,X0) = select(sF27,X0)
| i1 = X0 ) ).
cnf(u158,axiom,
sF24 = store(sF22,i5,sF21) ).
cnf(u377,axiom,
sF26 = store(sF24,i3,sF19) ).
cnf(u41,axiom,
store(sF17,i1,sF16) = sF18 ).
cnf(u494,axiom,
sF40 = select(sF38,i3) ).
cnf(u657,axiom,
sF38 = store(sF36,i1,sF2) ).
cnf(u101,axiom,
sF0 = select(sF1,i4) ).
cnf(u145,axiom,
( select(sF32,X0) = select(sF34,X0)
| i5 = X0 ) ).
cnf(u516,axiom,
sF37 = select(sF32,i1) ).
cnf(u104,axiom,
sF6 = select(sF27,i1) ).
cnf(u340,axiom,
sF21 = sF25 ).
cnf(u236,axiom,
sF35 = select(sF36,i3) ).
cnf(u127,axiom,
( select(a1,X0) = select(sF1,X0)
| i4 = X0 ) ).
cnf(u11,axiom,
store(sF1,i3,sF2) = sF3 ).
cnf(u456,axiom,
sF13 = store(sF11,i3,sF4) ).
cnf(u71,axiom,
select(sF32,i2) = sF33 ).
cnf(u427,axiom,
sF9 = store(sF7,i3,sF4) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u746,axiom,
sF4 = sF40 ).
cnf(u703,axiom,
( select(sF11,X0) = select(sF13,X0)
| i3 = X0 ) ).
cnf(u134,axiom,
( select(sF11,X0) = select(sF13,X0)
| i2 = X0 ) ).
cnf(u17,axiom,
select(sF3,i2) = sF6 ).
cnf(u335,axiom,
sF42 = sF46 ).
cnf(u425,axiom,
sF4 = sF29 ).
cnf(u89,axiom,
select(sF39,i5) = sF42 ).
cnf(u610,axiom,
sF24 = store(sF22,i3,sF4) ).
cnf(u149,axiom,
( select(sF39,X0) = select(sF41,X0)
| i5 = X0 ) ).
cnf(u221,axiom,
sF22 = store(sF20,i3,sF21) ).
cnf(u108,axiom,
sF12 = select(sF13,i2) ).
cnf(u152,axiom,
( select(sF45,X0) = select(sF47,X0)
| i2 = X0 ) ).
cnf(u224,axiom,
sF28 = store(sF27,i3,sF4) ).
cnf(u115,axiom,
sF25 = select(sF26,i2) ).
cnf(u527,axiom,
sF41 = store(sF39,i3,sF33) ).
cnf(u219,axiom,
sF14 = select(sF11,i3) ).
cnf(u907,axiom,
sF4 = select(sF15,i3) ).
cnf(u310,axiom,
sF11 = store(sF9,i3,sF10) ).
cnf(u919,axiom,
sF4 = select(sF34,i3) ).
cnf(u354,axiom,
sF43 = store(sF41,i3,sF40) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u33,axiom,
select(sF11,i2) = sF14 ).
cnf(u985,axiom,
sF2 = select(sF38,i1) ).
cnf(u65,axiom,
store(sF28,i5,sF29) = sF30 ).
cnf(u93,axiom,
select(sF43,i2) = sF44 ).
cnf(u137,axiom,
( select(sF17,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u792,axiom,
sF20 = store(sF18,i3,sF4) ).
cnf(u759,axiom,
sF41 = store(sF39,i3,sF4) ).
cnf(u47,axiom,
select(sF18,i5) = sF21 ).
cnf(u59,axiom,
store(sF3,i1,sF6) = sF27 ).
cnf(u327,axiom,
sF19 = select(sF20,i3) ).
cnf(u119,axiom,
sF33 = select(sF34,i5) ).
cnf(u562,axiom,
sF4 = sF14 ).
cnf(u163,axiom,
sF10 = select(sF13,i2) ).
cnf(u631,axiom,
( select(sF3,X0) = select(sF5,X0)
| i3 = X0 ) ).
cnf(u798,axiom,
sF4 = sF21 ).
cnf(u223,axiom,
sF26 = store(sF24,i3,sF25) ).
cnf(u235,axiom,
sF4 = select(sF28,i3) ).
cnf(u694,axiom,
( select(sF22,X0) = select(sF24,X0)
| i3 = X0 ) ).
cnf(u122,axiom,
sF37 = select(sF39,i1) ).
cnf(u637,axiom,
sF37 = select(sF28,i1) ).
cnf(u226,axiom,
sF36 = store(sF34,i3,sF35) ).
cnf(u9,axiom,
select(a1,i4) = sF2 ).
cnf(u698,axiom,
( select(sF30,X0) = select(sF32,X0)
| i3 = X0 ) ).
cnf(u455,axiom,
sF11 = store(sF9,i3,sF4) ).
cnf(u69,axiom,
store(sF30,i0,sF31) = sF32 ).
cnf(u241,axiom,
sF10 = select(sF13,i3) ).
cnf(u141,axiom,
( select(sF24,X0) = select(sF26,X0)
| i2 = X0 ) ).
cnf(u100,negated_conjecture,
sF26 != sF47 ).
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(u333,axiom,
sF42 = select(sF45,i3) ).
cnf(u95,axiom,
store(sF43,i5,sF44) = sF45 ).
cnf(u107,axiom,
sF10 = select(sF11,i5) ).
cnf(u716,axiom,
sF4 = select(sF47,i3) ).
cnf(u700,axiom,
( select(sF7,X0) = select(sF9,X0)
| i3 = X0 ) ).
cnf(u619,axiom,
sF2 = sF16 ).
cnf(u126,axiom,
sF46 = select(sF47,i2) ).
cnf(u723,axiom,
sF43 = store(sF41,i3,sF4) ).
cnf(u768,axiom,
sF4 = select(sF22,i3) ).
cnf(u334,axiom,
sF21 = select(sF24,i3) ).
cnf(u346,axiom,
sF47 = store(sF45,i3,sF40) ).
cnf(u230,axiom,
sF47 = store(sF45,i3,sF46) ).
cnf(u113,axiom,
sF21 = select(sF22,i2) ).
cnf(u13,axiom,
select(sF3,i1) = sF4 ).
cnf(u729,axiom,
sF36 = store(sF34,i3,sF4) ).
cnf(u424,axiom,
sF32 = store(sF30,i3,sF4) ).
cnf(u39,axiom,
store(sF15,i1,sF16) = sF17 ).
cnf(u83,axiom,
store(sF38,i1,sF37) = sF39 ).
cnf(u479,axiom,
sF16 = select(sF11,i1) ).
cnf(u143,axiom,
( select(sF28,X0) = select(sF30,X0)
| i5 = X0 ) ).
cnf(u155,axiom,
sF13 = store(sF11,i2,sF10) ).
cnf(u658,axiom,
( select(sF27,X0) = select(sF28,X0)
| i3 = X0 ) ).
cnf(u102,axiom,
sF2 = select(sF3,i3) ).
cnf(u777,axiom,
sF4 = sF35 ).
cnf(u321,axiom,
sF41 = store(sF39,i3,sF40) ).
cnf(u146,axiom,
( select(sF34,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u629,axiom,
sF18 = store(sF17,i1,sF2) ).
cnf(u57,axiom,
store(sF24,i2,sF25) = sF26 ).
cnf(u325,axiom,
sF10 = select(sF11,i3) ).
cnf(u117,axiom,
sF29 = select(sF30,i5) ).
cnf(u161,axiom,
sF45 = store(sF43,i5,sF42) ).
cnf(u567,axiom,
sF15 = store(sF13,i3,sF4) ).
cnf(u233,axiom,
sF21 = select(sF22,i3) ).
cnf(u120,axiom,
sF35 = select(sF36,i2) ).
cnf(u296,axiom,
sF7 = store(sF5,i1,sF2) ).
cnf(u683,axiom,
( select(sF32,X0) = select(sF34,X0)
| i3 = X0 ) ).
cnf(u356,axiom,
sF36 = store(sF34,i3,sF33) ).
cnf(u628,axiom,
sF45 = store(sF43,i3,sF4) ).
cnf(u319,axiom,
sF34 = store(sF32,i3,sF33) ).
cnf(u428,axiom,
sF4 = sF10 ).
cnf(u15,axiom,
store(sF3,i2,sF4) = sF5 ).
cnf(u27,axiom,
store(sF9,i5,sF10) = sF11 ).
cnf(u423,axiom,
sF4 = select(sF9,i3) ).
cnf(u87,axiom,
store(sF39,i5,sF40) = sF41 ).
cnf(u708,axiom,
sF2 = select(sF7,i1) ).
cnf(u131,axiom,
( select(sF5,X0) = select(sF7,X0)
| i1 = X0 ) ).
cnf(u111,axiom,
sF16 = select(sF18,i1) ).
cnf(u671,axiom,
( select(sF9,X0) = select(sF11,X0)
| i3 = X0 ) ).
cnf(u706,axiom,
sF2 = select(sF27,i1) ).
cnf(u150,axiom,
( select(sF41,X0) = select(sF43,X0)
| i2 = X0 ) ).
cnf(u326,axiom,
sF14 = select(sF15,i3) ).
cnf(u61,axiom,
store(sF27,i2,sF4) = sF28 ).
cnf(u677,axiom,
( select(sF18,X0) = select(sF20,X0)
| i3 = X0 ) ).
cnf(u105,axiom,
sF6 = select(sF7,i1) ).
cnf(u385,axiom,
sF22 = store(sF20,i3,sF19) ).
cnf(u237,axiom,
sF42 = select(sF43,i3) ).
cnf(u124,axiom,
sF42 = select(sF43,i2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV531-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.26 % Computer : n015.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Mon Sep 28 11:37:47 UTC 2026
% 0.09/0.26 % CPUTime :
% 0.09/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.26/0.31 Running first-order model finding
% 0.26/0.31 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.64/1.19 % (2564435)Will run a generic schedule for satisfiability detection.
% 5.64/1.19 % (2564440)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3183976941_2999 on theBenchmark for (2999ds/0Mi)
% 5.64/1.19 % TRYING [1]
% 5.64/1.19 % TRYING [2]
% 5.64/1.19 % TRYING [3]
% 5.64/1.19 % (2564441)% WARNING: option uhcvi not known.
% 5.64/1.19 % TRYING [4]
% 5.64/1.19 % (2564446)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=105754129:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.64/1.19 % (2564442)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2231881456:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.64/1.19 % (2564444)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1872098181:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.64/1.19 % (2564443)dis+10_1_sil=32000:sp=arity:random_seed=1301312949:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.64/1.19 % (2564441)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3454345757:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.64/1.19 % (2564445)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=744243843:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.64/1.19 % TRYING [5]
% 5.64/1.19 % TRYING [6]
% 5.64/1.19 % (2564445)Instruction limit reached!
% 5.64/1.19 % (2564445)------------------------------
% 5.64/1.19 % (2564445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564445)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564445)Termination reason: Instruction limit
% 5.64/1.19 % (2564445)Termination phase: Saturation
% 5.64/1.19 % (2564445)Time elapsed: 0.073 s
% 5.64/1.19 % (2564445)Peak memory usage: 11 MB
% 5.64/1.19 % (2564445)Instructions burned: 132 (million)
% 5.64/1.19 % (2564444)Instruction limit reached!
% 5.64/1.19 % (2564444)------------------------------
% 5.64/1.19 % (2564444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564444)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564444)Termination reason: Instruction limit
% 5.64/1.19 % (2564444)Termination phase: Saturation
% 5.64/1.19 % (2564444)Time elapsed: 0.087 s
% 5.64/1.19 % (2564444)Peak memory usage: 14 MB
% 5.64/1.19 % (2564444)Instructions burned: 116 (million)
% 5.64/1.19 % (2564446)Instruction limit reached!
% 5.64/1.19 % (2564446)------------------------------
% 5.64/1.19 % (2564446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564446)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564446)Termination reason: Instruction limit
% 5.64/1.19 % (2564446)Termination phase: Saturation
% 5.64/1.19 % (2564446)Time elapsed: 0.106 s
% 5.64/1.19 % (2564446)Peak memory usage: 14 MB
% 5.64/1.19 % (2564446)Instructions burned: 159 (million)
% 5.64/1.19 % (2564443)Instruction limit reached!
% 5.64/1.19 % (2564443)------------------------------
% 5.64/1.19 % (2564443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564443)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564443)Termination reason: Instruction limit
% 5.64/1.19 % (2564443)Termination phase: Saturation
% 5.64/1.19 % (2564443)Time elapsed: 0.109 s
% 5.64/1.19 % (2564443)Peak memory usage: 13 MB
% 5.64/1.19 % (2564443)Instructions burned: 105 (million)
% 5.64/1.19 % (2564455)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3717470425:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.64/1.19 % (2564454)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=783712229:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 5.64/1.19 % TRYING [1]
% 5.64/1.19 % TRYING [7]
% 5.64/1.19 % TRYING [2]
% 5.64/1.19 % TRYING [3]
% 5.64/1.19 % TRYING [4]
% 5.64/1.19 % (2564456)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=3496071890:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.64/1.19 % (2564457)ott-21_1_sil=16000:fs=off:random_seed=447713626:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.64/1.19 % TRYING [5]
% 5.64/1.19 % (2564455)Instruction limit reached!
% 5.64/1.19 % (2564455)------------------------------
% 5.64/1.19 % (2564455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564455)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564455)Termination reason: Instruction limit
% 5.64/1.19 % (2564455)Termination phase: Saturation
% 5.64/1.19 % (2564455)Time elapsed: 0.106 s
% 5.64/1.19 % (2564455)Peak memory usage: 15 MB
% 5.64/1.19 % (2564455)Instructions burned: 131 (million)
% 5.64/1.19 % (2564462)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4075903103:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 5.64/1.19 % (2564457)Instruction limit reached!
% 5.64/1.19 % (2564457)------------------------------
% 5.64/1.19 % (2564457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564457)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564457)Termination reason: Instruction limit
% 5.64/1.19 % (2564457)Termination phase: Saturation
% 5.64/1.19 % (2564457)Time elapsed: 0.114 s
% 5.64/1.19 % (2564457)Peak memory usage: 12 MB
% 5.64/1.19 % (2564457)Instructions burned: 180 (million)
% 5.64/1.19 % (2564464)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3467775264:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 5.64/1.19 % TRYING [1]
% 5.64/1.19 % TRYING [6]
% 5.64/1.19 % TRYING [2]
% 5.64/1.19 % TRYING [3]
% 5.64/1.19 % TRYING [4]
% 5.64/1.19 % TRYING [8]
% 5.64/1.19 % TRYING [5]
% 5.64/1.19 % TRYING [6]
% 5.64/1.19 % (2564456)Instruction limit reached!
% 5.64/1.19 % (2564456)------------------------------
% 5.64/1.19 % (2564456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564456)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564456)Termination reason: Instruction limit
% 5.64/1.19 % (2564456)Termination phase: Saturation
% 5.64/1.19 % (2564456)Time elapsed: 0.545 s
% 5.64/1.19 % (2564456)Peak memory usage: 19 MB
% 5.64/1.19 % (2564456)Instructions burned: 684 (million)
% 5.64/1.19 % (2564454)Instruction limit reached!
% 5.64/1.19 % (2564454)------------------------------
% 5.64/1.19 % (2564454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564454)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564454)Termination reason: Instruction limit
% 5.64/1.19 % (2564454)Termination phase: Finite model building SAT solving
% 5.64/1.19 % (2564454)Time elapsed: 0.574 s
% 5.64/1.19 % (2564454)Peak memory usage: 24 MB
% 5.64/1.19 % (2564454)Instructions burned: 714 (million)
% 5.64/1.19 % (2564467)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2159509472:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 5.64/1.19 % (2564466)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2032491492:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 5.64/1.19 % (2564462)Instruction limit reached!
% 5.64/1.19 % (2564462)------------------------------
% 5.64/1.19 % (2564462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564462)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564462)Termination reason: Instruction limit
% 5.64/1.19 % (2564462)Termination phase: Saturation
% 5.64/1.19 % (2564462)Time elapsed: 0.478 s
% 5.64/1.19 % (2564462)Peak memory usage: 23 MB
% 5.64/1.19 % (2564462)Instructions burned: 478 (million)
% 5.64/1.19 % (2564466) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2564435-2564466"...
% 5.64/1.19 % (2564466)...printing done.
% 5.64/1.19 % SZS status Satisfiable for theBenchmark
% 5.64/1.19 % SZS output start Saturation.
% See solution above
% 5.64/1.19 % SZS output start Definitions and Model Updates.
% 5.64/1.19 % SZS output end Definitions and Model Updates.
% 5.64/1.19 % (2564466)------------------------------
% 5.64/1.19 % (2564466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.19 % (2564466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.19 % (2564466)CaDiCaL version: 2.1.3
% 5.64/1.19 % (2564466)Termination reason: Satisfiable
% 5.64/1.19 % (2564466)Time elapsed: 0.046 s
% 5.64/1.19 % (2564466)Peak memory usage: 12 MB
% 5.64/1.19 % (2564466)Instructions burned: 51 (million)
% 5.64/1.19 % (2564435)Success in time 0.866 s
% 5.64/1.19 % Vampire exiting
%------------------------------------------------------------------------------