%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV504-1.050 : 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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:16:09 PM UTC 2026
% Result : Satisfiable 20.74s 3.68s
% Output : Saturation 21.78s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u417,axiom,
n1 != sF100 ).
cnf(u422,axiom,
sF102 = select(sF98,sF100) ).
cnf(u454,axiom,
n31 = sF100 ).
cnf(u480,axiom,
sF101 = select(sF47,n31) ).
cnf(u491,axiom,
n31 = n48 ).
cnf(u344,axiom,
( select(sF31,X0) = select(sF32,X0)
| n33 = X0 ) ).
cnf(u295,axiom,
e9 = select(sF8,n9) ).
cnf(u228,axiom,
e2 = select(sF86,n2) ).
cnf(u240,axiom,
e24 = select(sF96,n24) ).
cnf(u339,axiom,
( select(sF26,X0) = select(sF27,X0)
| n28 = X0 ) ).
cnf(u367,axiom,
( select(sF55,X0) = select(sF56,X0)
| n22 = X0 ) ).
cnf(u191,axiom,
store(sF92,n5,e5) = sF93 ).
cnf(u75,axiom,
store(sF34,n36,e36) = sF35 ).
cnf(u135,axiom,
store(sF64,n6,e6) = sF65 ).
cnf(u376,axiom,
( select(sF64,X0) = select(sF65,X0)
| n6 = X0 ) ).
cnf(u361,axiom,
( select(sF48,X0) = select(sF49,X0)
| n1 = X0 ) ).
cnf(u368,axiom,
( select(sF56,X0) = select(sF57,X0)
| n39 = X0 ) ).
cnf(u218,axiom,
e49 = select(sF48,n49) ).
cnf(u313,axiom,
( select(sF0,X0) = select(sF1,X0)
| n2 = X0 ) ).
cnf(u373,axiom,
( select(sF61,X0) = select(sF62,X0)
| n49 = X0 ) ).
cnf(u257,axiom,
e43 = select(sF42,n43) ).
cnf(u49,axiom,
store(sF21,n23,e23) = sF22 ).
cnf(u502,axiom,
( select(sF87,X0) = select(sF88,X0)
| n31 = X0 ) ).
cnf(u81,axiom,
store(sF37,n39,e39) = sF38 ).
cnf(u109,axiom,
store(sF51,n45,e45) = sF52 ).
cnf(u153,axiom,
store(sF73,n18,e18) = sF74 ).
cnf(u213,axiom,
e1 = select(sF99,n1) ).
cnf(u276,axiom,
e6 = select(sF65,n6) ).
cnf(u288,axiom,
e25 = select(sF24,n25) ).
cnf(u348,axiom,
( select(sF35,X0) = select(sF36,X0)
| n37 = X0 ) ).
cnf(u63,axiom,
store(sF28,n30,e30) = sF29 ).
cnf(u216,axiom,
e2 = select(sF1,n2) ).
cnf(u392,axiom,
( select(sF80,X0) = select(sF81,X0)
| n23 = X0 ) ).
cnf(u343,axiom,
( select(sF30,X0) = select(sF31,X0)
| n32 = X0 ) ).
cnf(u7,axiom,
store(sF0,n2,e2) = sF1 ).
cnf(u387,axiom,
( select(sF75,X0) = select(sF76,X0)
| n34 = X0 ) ).
cnf(u179,axiom,
store(sF86,n10,e10) = sF87 ).
cnf(u388,axiom,
( select(sF76,X0) = select(sF77,X0)
| n11 = X0 ) ).
cnf(u239,axiom,
e34 = select(sF33,n34) ).
cnf(u251,axiom,
e28 = select(sF54,n28) ).
cnf(u302,axiom,
e7 = select(sF68,n7) ).
cnf(u314,axiom,
( select(sF1,X0) = select(sF2,X0)
| n3 = X0 ) ).
cnf(u374,axiom,
( select(sF62,X0) = select(sF63,X0)
| n14 = X0 ) ).
cnf(u317,axiom,
( select(sF4,X0) = select(sF5,X0)
| n6 = X0 ) ).
cnf(u242,axiom,
e38 = select(sF37,n38) ).
cnf(u394,axiom,
( select(sF82,X0) = select(sF83,X0)
| n46 = X0 ) ).
cnf(u397,axiom,
( select(sF85,X0) = select(sF86,X0)
| n2 = X0 ) ).
cnf(u25,axiom,
store(sF9,n11,e11) = sF10 ).
cnf(u85,axiom,
store(sF39,n41,e41) = sF40 ).
cnf(u349,axiom,
( select(sF36,X0) = select(sF37,X0)
| n38 = X0 ) ).
cnf(u129,axiom,
store(sF61,n49,e49) = sF62 ).
cnf(u157,axiom,
store(sF75,n34,e34) = sF76 ).
cnf(u400,axiom,
( select(sF88,X0) = select(sF89,X0)
| n29 = X0 ) ).
cnf(u201,axiom,
store(sF97,n31,e31) = sF98 ).
cnf(u264,axiom,
e42 = select(sF72,n42) ).
cnf(u324,axiom,
( select(sF11,X0) = select(sF12,X0)
| n13 = X0 ) ).
cnf(u259,axiom,
e19 = select(sF18,n19) ).
cnf(u287,axiom,
e17 = select(sF16,n17) ).
cnf(u396,axiom,
( select(sF84,X0) = select(sF85,X0)
| n50 = X0 ) ).
cnf(u111,axiom,
store(sF52,n43,e43) = sF53 ).
cnf(u123,axiom,
store(sF58,n40,e40) = sF59 ).
cnf(u391,axiom,
( select(sF79,X0) = select(sF80,X0)
| n38 = X0 ) ).
cnf(u183,axiom,
store(sF88,n29,e29) = sF89 ).
cnf(u336,axiom,
( select(sF23,X0) = select(sF24,X0)
| n25 = X0 ) ).
cnf(u271,axiom,
e25 = select(sF82,n25) ).
cnf(u290,axiom,
e12 = select(sF92,n12) ).
cnf(u350,axiom,
( select(sF37,X0) = select(sF38,X0)
| n39 = X0 ) ).
cnf(u293,axiom,
e30 = select(sF51,n30) ).
cnf(u305,axiom,
e13 = select(sF12,n13) ).
cnf(u246,axiom,
e26 = select(sF25,n26) ).
cnf(u353,axiom,
( select(sF40,X0) = select(sF41,X0)
| n42 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u29,axiom,
store(sF11,n13,e13) = sF12 ).
cnf(u409,axiom,
( select(sF97,X0) = select(sF98,X0)
| n31 = X0 ) ).
cnf(u73,axiom,
store(sF33,n35,e35) = sF34 ).
cnf(u404,axiom,
( select(sF92,X0) = select(sF93,X0)
| n5 = X0 ) ).
cnf(u133,axiom,
store(sF63,n13,e13) = sF64 ).
cnf(u363,axiom,
( select(sF51,X0) = select(sF52,X0)
| n45 = X0 ) ).
cnf(u385,axiom,
( select(sF73,X0) = select(sF74,X0)
| n18 = X0 ) ).
cnf(u268,axiom,
e29 = select(sF89,n29) ).
cnf(u337,axiom,
( select(sF24,X0) = select(sF25,X0)
| n26 = X0 ) ).
cnf(u263,axiom,
e26 = select(sF75,n26) ).
cnf(u55,axiom,
store(sF24,n26,e26) = sF25 ).
cnf(u500,axiom,
e48 = select(sF88,n31) ).
cnf(u352,axiom,
( select(sF39,X0) = select(sF40,X0)
| n41 = X0 ) ).
cnf(u159,axiom,
store(sF76,n11,e11) = sF77 ).
cnf(u171,axiom,
store(sF82,n46,e46) = sF83 ).
cnf(u203,axiom,
store(sF98,n1,e1) = sF99 ).
cnf(u231,axiom,
e32 = select(sF31,n32) ).
cnf(u294,axiom,
e37 = select(sF36,n37) ).
cnf(u335,axiom,
( select(sF22,X0) = select(sF23,X0)
| n24 = X0 ) ).
cnf(u281,axiom,
e28 = select(sF27,n28) ).
cnf(u309,axiom,
e21 = select(sF97,n21) ).
cnf(u234,axiom,
e44 = select(sF43,n44) ).
cnf(u410,axiom,
( select(sF98,X0) = select(sF99,X0)
| n1 = X0 ) ).
cnf(u5,axiom,
store(a1,n1,e1) = sF0 ).
cnf(u384,axiom,
( select(sF72,X0) = select(sF73,X0)
| n47 = X0 ) ).
cnf(u177,axiom,
store(sF85,n2,e2) = sF86 ).
cnf(u77,axiom,
store(sF35,n37,e37) = sF36 ).
cnf(u469,axiom,
e31 = select(sF99,n31) ).
cnf(u249,axiom,
e35 = select(sF84,n35) ).
cnf(u312,axiom,
( select(a1,X0) = select(sF0,X0)
| n1 = X0 ) ).
cnf(u372,axiom,
( select(sF60,X0) = select(sF61,X0)
| n8 = X0 ) ).
cnf(u307,axiom,
e5 = select(sF93,n5) ).
cnf(u370,axiom,
( select(sF58,X0) = select(sF59,X0)
| n40 = X0 ) ).
cnf(u31,axiom,
store(sF12,n14,e14) = sF13 ).
cnf(u43,axiom,
store(sF18,n20,e20) = sF19 ).
cnf(u103,axiom,
store(sF48,n1,e1) = sF49 ).
cnf(u147,axiom,
store(sF70,n17,e17) = sF71 ).
cnf(u270,axiom,
e22 = select(sF56,n22) ).
cnf(u282,axiom,
e11 = select(sF77,n11) ).
cnf(u342,axiom,
( select(sF29,X0) = select(sF30,X0)
| n31 = X0 ) ).
cnf(u285,axiom,
e10 = select(sF87,n10) ).
cnf(u238,axiom,
e4 = select(sF3,n4) ).
cnf(u329,axiom,
( select(sF16,X0) = select(sF17,X0)
| n18 = X0 ) ).
cnf(u121,axiom,
store(sF57,n20,e20) = sF58 ).
cnf(u389,axiom,
( select(sF77,X0) = select(sF78,X0)
| n36 = X0 ) ).
cnf(u225,axiom,
e47 = select(sF73,n47) ).
cnf(u253,axiom,
e35 = select(sF34,n35) ).
cnf(u316,axiom,
( select(sF3,X0) = select(sF4,X0)
| n5 = X0 ) ).
cnf(u360,axiom,
( select(sF47,X0) = select(sF48,X0)
| n49 = X0 ) ).
cnf(u311,axiom,
( select(a1,X0) = select(sF50,X0)
| n41 = X0 ) ).
cnf(u244,axiom,
e33 = select(sF69,n33) ).
cnf(u355,axiom,
( select(sF42,X0) = select(sF43,X0)
| n44 = X0 ) ).
cnf(u19,axiom,
store(sF6,n8,e8) = sF7 ).
cnf(u79,axiom,
store(sF36,n38,e38) = sF37 ).
cnf(u91,axiom,
store(sF42,n44,e44) = sF43 ).
cnf(u151,axiom,
store(sF72,n47,e47) = sF73 ).
cnf(u195,axiom,
store(sF94,n4,e4) = sF95 ).
cnf(u258,axiom,
e39 = select(sF57,n39) ).
cnf(u47,axiom,
store(sF20,n22,e22) = sF21 ).
cnf(u261,axiom,
e38 = select(sF80,n38) ).
cnf(u53,axiom,
store(sF23,n25,e25) = sF24 ).
cnf(u214,axiom,
e41 = select(sF40,n41) ).
cnf(u390,axiom,
( select(sF78,X0) = select(sF79,X0)
| n44 = X0 ) ).
cnf(u97,axiom,
store(sF45,n47,e47) = sF46 ).
cnf(u125,axiom,
store(sF59,n16,e16) = sF60 ).
cnf(u505,axiom,
e48 = select(sF49,n31) ).
cnf(u169,axiom,
store(sF81,n25,e25) = sF82 ).
cnf(u229,axiom,
e46 = select(sF45,n46) ).
cnf(u346,axiom,
( select(sF33,X0) = select(sF34,X0)
| n35 = X0 ) ).
cnf(u292,axiom,
e8 = select(sF7,n8) ).
cnf(u304,axiom,
e3 = select(sF90,n3) ).
cnf(u364,axiom,
( select(sF52,X0) = select(sF53,X0)
| n43 = X0 ) ).
cnf(u299,axiom,
e16 = select(sF60,n16) ).
cnf(u232,axiom,
e31 = select(sF30,n31) ).
cnf(u408,axiom,
( select(sF96,X0) = select(sF97,X0)
| n21 = X0 ) ).
cnf(u23,axiom,
store(sF8,n10,e10) = sF9 ).
cnf(u468,axiom,
e31 = sF102 ).
cnf(u403,axiom,
( select(sF91,X0) = select(sF92,X0)
| n12 = X0 ) ).
cnf(u67,axiom,
store(sF30,n32,e32) = sF31 ).
cnf(u362,axiom,
( select(sF50,X0) = select(sF51,X0)
| n30 = X0 ) ).
cnf(u255,axiom,
e24 = select(sF23,n24) ).
cnf(u139,axiom,
store(sF66,n15,e15) = sF67 ).
cnf(u369,axiom,
( select(sF57,X0) = select(sF58,X0)
| n20 = X0 ) ).
cnf(u318,axiom,
( select(sF5,X0) = select(sF6,X0)
| n7 = X0 ) ).
cnf(u199,axiom,
store(sF96,n21,e21) = sF97 ).
cnf(u398,axiom,
( select(sF86,X0) = select(sF87,X0)
| n10 = X0 ) ).
cnf(u262,axiom,
e42 = select(sF41,n42) ).
cnf(u347,axiom,
( select(sF34,X0) = select(sF35,X0)
| n36 = X0 ) ).
cnf(u377,axiom,
( select(sF65,X0) = select(sF66,X0)
| n27 = X0 ) ).
cnf(u41,axiom,
store(sF17,n19,e19) = sF18 ).
cnf(u506,axiom,
e48 = select(sF48,n31) ).
cnf(u101,axiom,
store(sF47,n49,e49) = sF48 ).
cnf(u331,axiom,
( select(sF18,X0) = select(sF19,X0)
| n20 = X0 ) ).
cnf(u145,axiom,
store(sF69,n9,e9) = sF70 ).
cnf(u173,axiom,
store(sF83,n35,e35) = sF84 ).
cnf(u283,axiom,
e45 = select(sF44,n45) ).
cnf(u217,axiom,
e49 = select(sF62,n49) ).
cnf(u280,axiom,
e20 = select(sF58,n20) ).
cnf(u340,axiom,
( select(sF27,X0) = select(sF28,X0)
| n29 = X0 ) ).
cnf(u275,axiom,
e23 = select(sF22,n23) ).
cnf(u303,axiom,
e8 = select(sF61,n8) ).
cnf(u236,axiom,
e40 = select(sF39,n40) ).
cnf(u127,axiom,
store(sF60,n8,e8) = sF61 ).
cnf(u11,axiom,
store(sF2,n4,e4) = sF3 ).
cnf(u407,axiom,
( select(sF95,X0) = select(sF96,X0)
| n24 = X0 ) ).
cnf(u71,axiom,
store(sF32,n34,e34) = sF33 ).
cnf(u243,axiom,
e22 = select(sF21,n22) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u306,axiom,
e5 = select(sF4,n5) ).
cnf(u379,axiom,
( select(sF67,X0) = select(sF68,X0)
| n7 = X0 ) ).
cnf(u463,axiom,
n1 != n31 ).
cnf(u366,axiom,
( select(sF54,X0) = select(sF55,X0)
| n19 = X0 ) ).
cnf(u401,axiom,
( select(sF89,X0) = select(sF90,X0)
| n3 = X0 ) ).
cnf(u17,axiom,
store(sF5,n7,e7) = sF6 ).
cnf(u45,axiom,
store(sF19,n21,e21) = sF20 ).
cnf(u371,axiom,
( select(sF59,X0) = select(sF60,X0)
| n16 = X0 ) ).
cnf(u89,axiom,
store(sF41,n43,e43) = sF42 ).
cnf(u386,axiom,
( select(sF74,X0) = select(sF75,X0)
| n26 = X0 ) ).
cnf(u149,axiom,
store(sF71,n42,e42) = sF72 ).
cnf(u193,axiom,
store(sF93,n32,e32) = sF94 ).
cnf(u221,axiom,
e31 = select(sF98,n31) ).
cnf(u341,axiom,
( select(sF28,X0) = select(sF29,X0)
| n30 = X0 ) ).
cnf(u284,axiom,
e13 = select(sF64,n13) ).
cnf(u328,axiom,
( select(sF15,X0) = select(sF16,X0)
| n17 = X0 ) ).
cnf(u279,axiom,
e9 = select(sF70,n9) ).
cnf(u212,axiom,
e1 = select(sF0,n1) ).
cnf(u224,axiom,
e47 = select(sF46,n47) ).
cnf(u323,axiom,
( select(sF10,X0) = select(sF11,X0)
| n12 = X0 ) ).
cnf(u115,axiom,
store(sF54,n19,e19) = sF55 ).
cnf(u383,axiom,
( select(sF71,X0) = select(sF72,X0)
| n42 = X0 ) ).
cnf(u175,axiom,
store(sF84,n50,e50) = sF85 ).
cnf(u187,axiom,
store(sF90,n37,e37) = sF91 ).
cnf(u219,axiom,
e30 = select(sF29,n30) ).
cnf(u247,axiom,
e34 = select(sF76,n34) ).
cnf(u497,axiom,
sF47 = store(sF46,n31,e48) ).
cnf(u310,axiom,
e50 = select(sF85,n50) ).
cnf(u354,axiom,
( select(sF41,X0) = select(sF42,X0)
| n43 = X0 ) ).
cnf(u297,axiom,
e12 = select(sF11,n12) ).
cnf(u250,axiom,
e36 = select(sF35,n36) ).
cnf(u357,axiom,
( select(sF44,X0) = select(sF45,X0)
| n46 = X0 ) ).
cnf(u21,axiom,
store(sF7,n9,e9) = sF8 ).
cnf(u33,axiom,
store(sF13,n15,e15) = sF14 ).
cnf(u65,axiom,
store(sF29,n31,e31) = sF30 ).
cnf(u93,axiom,
store(sF43,n45,e45) = sF44 ).
cnf(u137,axiom,
store(sF65,n27,e27) = sF66 ).
cnf(u197,axiom,
store(sF95,n24,e24) = sF96 ).
cnf(u260,axiom,
e33 = select(sF32,n33) ).
cnf(u272,axiom,
e14 = select(sF63,n14) ).
cnf(u332,axiom,
( select(sF19,X0) = select(sF20,X0)
| n21 = X0 ) ).
cnf(u267,axiom,
e19 = select(sF55,n19) ).
cnf(u59,axiom,
store(sF26,n28,e28) = sF27 ).
cnf(u504,negated_conjecture,
e31 != e48 ).
cnf(u327,axiom,
( select(sF14,X0) = select(sF15,X0)
| n16 = X0 ) ).
cnf(u119,axiom,
store(sF56,n39,e39) = sF57 ).
cnf(u499,axiom,
e48 = select(sF47,n31) ).
cnf(u163,axiom,
store(sF78,n44,e44) = sF79 ).
cnf(u223,axiom,
e6 = select(sF5,n6) ).
cnf(u235,axiom,
e44 = select(sF79,n44) ).
cnf(u286,axiom,
e16 = select(sF15,n16) ).
cnf(u298,axiom,
e27 = select(sF26,n27) ).
cnf(u460,axiom,
n31 = sk(sF49,sF99) ).
cnf(u358,axiom,
( select(sF45,X0) = select(sF46,X0)
| n47 = X0 ) ).
cnf(u301,axiom,
e15 = select(sF67,n15) ).
cnf(u226,axiom,
e32 = select(sF94,n32) ).
cnf(u254,axiom,
e39 = select(sF38,n39) ).
cnf(u345,axiom,
( select(sF32,X0) = select(sF33,X0)
| n34 = X0 ) ).
cnf(u9,axiom,
store(sF1,n3,e3) = sF2 ).
cnf(u405,axiom,
( select(sF93,X0) = select(sF94,X0)
| n32 = X0 ) ).
cnf(u69,axiom,
store(sF31,n33,e33) = sF32 ).
cnf(u241,axiom,
e10 = select(sF9,n10) ).
cnf(u141,axiom,
store(sF67,n7,e7) = sF68 ).
cnf(u365,axiom,
( select(sF53,X0) = select(sF54,X0)
| n28 = X0 ) ).
cnf(u320,axiom,
( select(sF7,X0) = select(sF8,X0)
| n9 = X0 ) ).
cnf(u35,axiom,
store(sF14,n16,e16) = sF15 ).
cnf(u330,axiom,
( select(sF17,X0) = select(sF18,X0)
| n19 = X0 ) ).
cnf(u333,axiom,
( select(sF20,X0) = select(sF21,X0)
| n22 = X0 ) ).
cnf(u95,axiom,
store(sF44,n46,e46) = sF45 ).
cnf(u107,axiom,
store(sF50,n30,e30) = sF51 ).
cnf(u503,axiom,
e48 = sF101 ).
cnf(u167,axiom,
store(sF80,n23,e23) = sF81 ).
cnf(u211,axiom,
e41 = select(sF50,n41) ).
cnf(u274,axiom,
e23 = select(sF81,n23) ).
cnf(u256,axiom,
e43 = select(sF53,n43) ).
cnf(u334,axiom,
( select(sF21,X0) = select(sF22,X0)
| n23 = X0 ) ).
cnf(u277,axiom,
e18 = select(sF74,n18) ).
cnf(u289,axiom,
e15 = select(sF14,n15) ).
cnf(u230,axiom,
e46 = select(sF83,n46) ).
cnf(u406,axiom,
( select(sF94,X0) = select(sF95,X0)
| n4 = X0 ) ).
cnf(u113,axiom,
store(sF53,n28,e28) = sF54 ).
cnf(u13,axiom,
store(sF3,n5,e5) = sF4 ).
cnf(u393,axiom,
( select(sF81,X0) = select(sF82,X0)
| n25 = X0 ) ).
cnf(u185,axiom,
store(sF89,n3,e3) = sF90 ).
cnf(u245,axiom,
e18 = select(sF17,n18) ).
cnf(u378,axiom,
( select(sF66,X0) = select(sF67,X0)
| n15 = X0 ) ).
cnf(u381,axiom,
( select(sF69,X0) = select(sF70,X0)
| n9 = X0 ) ).
cnf(u308,axiom,
e29 = select(sF28,n29) ).
cnf(u227,axiom,
e14 = select(sF13,n14) ).
cnf(u380,axiom,
( select(sF68,X0) = select(sF69,X0)
| n33 = X0 ) ).
cnf(u315,axiom,
( select(sF2,X0) = select(sF3,X0)
| n4 = X0 ) ).
cnf(u248,axiom,
e45 = select(sF52,n45) ).
cnf(u375,axiom,
( select(sF63,X0) = select(sF64,X0)
| n13 = X0 ) ).
cnf(u39,axiom,
store(sF16,n18,e18) = sF17 ).
cnf(u395,axiom,
( select(sF83,X0) = select(sF84,X0)
| n35 = X0 ) ).
cnf(u51,axiom,
store(sF22,n24,e24) = sF23 ).
cnf(u83,axiom,
store(sF38,n40,e40) = sF39 ).
cnf(u143,axiom,
store(sF68,n33,e33) = sF69 ).
cnf(u155,axiom,
store(sF74,n26,e26) = sF75 ).
cnf(u215,axiom,
e1 = select(sF49,n1) ).
cnf(u278,axiom,
e27 = select(sF66,n27) ).
cnf(u321,axiom,
( select(sF8,X0) = select(sF9,X0)
| n10 = X0 ) ).
cnf(u322,axiom,
( select(sF9,X0) = select(sF10,X0)
| n11 = X0 ) ).
cnf(u265,axiom,
e37 = select(sF91,n37) ).
cnf(u57,axiom,
store(sF25,n27,e27) = sF26 ).
cnf(u273,axiom,
e17 = select(sF71,n17) ).
cnf(u325,axiom,
( select(sF12,X0) = select(sF13,X0)
| n14 = X0 ) ).
cnf(u117,axiom,
store(sF55,n22,e22) = sF56 ).
cnf(u161,axiom,
store(sF77,n36,e36) = sF78 ).
cnf(u189,axiom,
store(sF91,n12,e12) = sF92 ).
cnf(u233,axiom,
e3 = select(sF2,n3) ).
cnf(u296,axiom,
e21 = select(sF20,n21) ).
cnf(u356,axiom,
( select(sF43,X0) = select(sF44,X0)
| n45 = X0 ) ).
cnf(u291,axiom,
e11 = select(sF10,n11) ).
cnf(u319,axiom,
( select(sF6,X0) = select(sF7,X0)
| n8 = X0 ) ).
cnf(u252,axiom,
e36 = select(sF78,n36) ).
cnf(u15,axiom,
store(sF4,n6,e6) = sF5 ).
cnf(u27,axiom,
store(sF10,n12,e12) = sF11 ).
cnf(u351,axiom,
( select(sF38,X0) = select(sF39,X0)
| n40 = X0 ) ).
cnf(u87,axiom,
store(sF40,n42,e42) = sF41 ).
cnf(u338,axiom,
( select(sF25,X0) = select(sF26,X0)
| n27 = X0 ) ).
cnf(u131,axiom,
store(sF62,n14,e14) = sF63 ).
cnf(u402,axiom,
( select(sF90,X0) = select(sF91,X0)
| n37 = X0 ) ).
cnf(u382,axiom,
( select(sF70,X0) = select(sF71,X0)
| n17 = X0 ) ).
cnf(u266,axiom,
e7 = select(sF6,n7) ).
cnf(u326,axiom,
( select(sF13,X0) = select(sF14,X0)
| n15 = X0 ) ).
cnf(u269,axiom,
e20 = select(sF19,n20) ).
cnf(u61,axiom,
store(sF27,n29,e29) = sF28 ).
cnf(u37,axiom,
store(sF15,n17,e17) = sF16 ).
cnf(u105,axiom,
store(a1,n41,e41) = sF50 ).
cnf(u501,axiom,
( select(sF46,X0) = select(sF47,X0)
| n31 = X0 ) ).
cnf(u165,axiom,
store(sF79,n38,e38) = sF80 ).
cnf(u237,axiom,
e40 = select(sF59,n40) ).
cnf(u498,axiom,
sF88 = store(sF87,n31,e48) ).
cnf(u300,axiom,
e4 = select(sF95,n4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV504-1.050 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n016.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 11:26:33 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 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
% 9.74/2.12 % (3565950)Input is clausal, will run a generic CNF schedule.
% 9.74/2.12 % (3566005)lrs+10_1_sil=8000:sp=occurrence:random_seed=3590154009:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.74/2.12 % (3566005)Instruction limit reached!
% 9.74/2.12 % (3566005)------------------------------
% 9.74/2.12 % (3566005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.12 % (3566005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.12 % (3566005)CaDiCaL version: 2.1.3
% 9.74/2.12 % (3566005)Termination reason: Instruction limit
% 9.74/2.12 % (3566005)Termination phase: Saturation
% 9.74/2.12 % (3566005)Time elapsed: 0.025 s
% 9.74/2.12 % (3566005)Peak memory usage: 89 MB
% 9.74/2.12 % (3566005)Instructions burned: 109 (million)
% 9.74/2.12 % (3566003)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3395968560:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.74/2.12 % (3566001)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=2468753546:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.74/2.12 % (3566004)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=373406792:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.74/2.12 % (3566007)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=33542534:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.74/2.12 % (3566008)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3437182740:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.74/2.12 % (3566009)dis-21_1_sil=8000:lcm=predicate:random_seed=1365805681:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 9.74/2.12 % (3566009)Refutation not found, incomplete strategy
% 9.74/2.12 % (3566009)------------------------------
% 9.74/2.12 % (3566009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.12 % (3566009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.12 % (3566009)CaDiCaL version: 2.1.3
% 9.74/2.12 % (3566009)Termination reason: Refutation not found, incomplete strategy
% 9.74/2.12 % (3566009)Time elapsed: 0.003 s
% 9.74/2.12 % (3566009)Peak memory usage: 88 MB
% 9.74/2.12 % (3566009)Instructions burned: 4 (million)
% 9.74/2.12 % (3566007)Instruction limit reached!
% 9.74/2.12 % (3566007)------------------------------
% 9.74/2.12 % (3566007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.12 % (3566007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.12 % (3566007)CaDiCaL version: 2.1.3
% 9.74/2.12 % (3566007)Termination reason: Instruction limit
% 9.74/2.12 % (3566007)Termination phase: Saturation
% 9.74/2.12 % (3566007)Time elapsed: 0.046 s
% 9.74/2.12 % (3566007)Peak memory usage: 88 MB
% 9.74/2.12 % (3566007)Instructions burned: 115 (million)
% 9.74/2.12 % (3566008)Instruction limit reached!
% 9.74/2.12 % (3566008)------------------------------
% 9.74/2.12 % (3566008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.12 % (3566008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.12 % (3566008)CaDiCaL version: 2.1.3
% 9.74/2.12 % (3566008)Termination reason: Instruction limit
% 9.74/2.12 % (3566008)Termination phase: Saturation
% 9.74/2.12 % (3566008)Time elapsed: 0.073 s
% 9.74/2.12 % (3566008)Peak memory usage: 89 MB
% 9.74/2.12 % (3566008)Instructions burned: 182 (million)
% 9.74/2.12 % (3566047)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=3451897286:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.74/2.12 % (3566073)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3479649911:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 9.74/2.12 % (3566073)Instruction limit reached!
% 9.74/2.12 % (3566073)------------------------------
% 9.74/2.12 % (3566073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.12 % (3566073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.12 % (3566073)CaDiCaL version: 2.1.3
% 13.45/2.66 % (3566073)Termination reason: Instruction limit
% 13.45/2.66 % (3566073)Termination phase: Saturation
% 13.45/2.66 % (3566073)Time elapsed: 0.041 s
% 13.45/2.66 % (3566073)Peak memory usage: 90 MB
% 13.45/2.66 % (3566073)Instructions burned: 191 (million)
% 13.45/2.66 % (3566047)Instruction limit reached!
% 13.45/2.66 % (3566047)------------------------------
% 13.45/2.66 % (3566047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.45/2.66 % (3566047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.45/2.66 % (3566047)CaDiCaL version: 2.1.3
% 13.45/2.66 % (3566047)Termination reason: Instruction limit
% 13.45/2.66 % (3566047)Termination phase: Saturation
% 13.45/2.66 % (3566047)Time elapsed: 0.086 s
% 13.45/2.66 % (3566047)Peak memory usage: 89 MB
% 13.45/2.66 % (3566047)Instructions burned: 144 (million)
% 13.45/2.66 % (3566077)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1371868147:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.45/2.66 % (3566009)------------------------------
% 13.45/2.66 % (3566009)------------------------------
% 13.45/2.66 % (3566077)Instruction limit reached!
% 13.45/2.66 % (3566077)------------------------------
% 13.45/2.66 % (3566077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.45/2.66 % (3566077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.45/2.66 % (3566077)CaDiCaL version: 2.1.3
% 13.45/2.66 % (3566077)Termination reason: Instruction limit
% 13.45/2.66 % (3566077)Termination phase: Saturation
% 13.45/2.66 % (3566077)Time elapsed: 0.158 s
% 13.45/2.66 % (3566077)Peak memory usage: 89 MB
% 13.45/2.66 % (3566077)Instructions burned: 220 (million)
% 13.45/2.66 % (3566119)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4294276197:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 13.45/2.66 % (3566112)lrs+10_64_to=lpo:sil=8000:random_seed=2510496217:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 13.45/2.66 % (3566119)Instruction limit reached!
% 13.45/2.66 % (3566119)------------------------------
% 13.45/2.66 % (3566119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.45/2.66 % (3566119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.45/2.66 % (3566119)CaDiCaL version: 2.1.3
% 13.45/2.66 % (3566119)Termination reason: Instruction limit
% 13.45/2.66 % (3566119)Termination phase: Saturation
% 13.45/2.66 % (3566119)Time elapsed: 0.081 s
% 13.45/2.66 % (3566119)Peak memory usage: 89 MB
% 13.45/2.66 % (3566119)Instructions burned: 196 (million)
% 13.45/2.66 % (3566112)Instruction limit reached!
% 13.45/2.66 % (3566112)------------------------------
% 13.45/2.66 % (3566112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.45/2.66 % (3566112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.45/2.66 % (3566112)CaDiCaL version: 2.1.3
% 13.45/2.66 % (3566112)Termination reason: Instruction limit
% 13.45/2.66 % (3566112)Termination phase: Saturation
% 13.45/2.66 % (3566112)Time elapsed: 0.084 s
% 13.45/2.66 % (3566112)Peak memory usage: 88 MB
% 13.45/2.66 % (3566112)Instructions burned: 126 (million)
% 13.45/2.66 % (3566123)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3638548259:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 13.45/2.66 % (3566131)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1361246256:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 13.45/2.66 % (3566123)Instruction limit reached!
% 13.45/2.66 % (3566123)------------------------------
% 13.45/2.66 % (3566123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.45/2.66 % (3566123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.45/2.66 % (3566123)CaDiCaL version: 2.1.3
% 13.45/2.66 % (3566123)Termination reason: Instruction limit
% 13.45/2.66 % (3566123)Termination phase: Saturation
% 13.45/2.66 % (3566123)Time elapsed: 0.092 s
% 13.45/2.66 % (3566123)Peak memory usage: 91 MB
% 13.45/2.66 % (3566123)Instructions burned: 157 (million)
% 13.45/2.66 % (3566134)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3538421658:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 13.45/2.66 % (3566133)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=27502111:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 13.45/2.66 % (3566134)Instruction limit reached!
% 13.45/2.66 % (3566134)------------------------------
% 19.76/3.54 % (3566134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.54 % (3566134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.54 % (3566134)CaDiCaL version: 2.1.3
% 19.76/3.54 % (3566134)Termination reason: Instruction limit
% 19.76/3.54 % (3566134)Termination phase: Saturation
% 19.76/3.54 % (3566134)Time elapsed: 0.023 s
% 19.76/3.54 % (3566134)Peak memory usage: 88 MB
% 19.76/3.54 % (3566134)Instructions burned: 111 (million)
% 19.76/3.54 % (3566133)Instruction limit reached!
% 19.76/3.54 % (3566133)------------------------------
% 19.76/3.54 % (3566133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.54 % (3566133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.54 % (3566133)CaDiCaL version: 2.1.3
% 19.76/3.54 % (3566133)Termination reason: Instruction limit
% 19.76/3.54 % (3566133)Termination phase: Saturation
% 19.76/3.54 % (3566133)Time elapsed: 0.043 s
% 19.76/3.54 % (3566133)Peak memory usage: 89 MB
% 19.76/3.54 % (3566133)Instructions burned: 108 (million)
% 19.76/3.54 % (3566141)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1886880419:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 19.76/3.54 % (3566138)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3793504489:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 19.76/3.54 % (3566004)Refutation not found, incomplete strategy
% 19.76/3.54 % (3566004)------------------------------
% 19.76/3.54 % (3566004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.54 % (3566004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.54 % (3566004)CaDiCaL version: 2.1.3
% 19.76/3.54 % (3566004)Termination reason: Refutation not found, incomplete strategy
% 19.76/3.54 % (3566004)Time elapsed: 0.886 s
% 19.76/3.54 % (3566004)Peak memory usage: 130 MB
% 19.76/3.54 % (3566004)Instructions burned: 1137 (million)
% 19.76/3.54 % (3566142)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3270850293:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 19.76/3.54 % (3566138)Instruction limit reached!
% 19.76/3.54 % (3566138)------------------------------
% 19.76/3.54 % (3566138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.54 % (3566138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.54 % (3566138)CaDiCaL version: 2.1.3
% 19.76/3.54 % (3566138)Termination reason: Instruction limit
% 19.76/3.54 % (3566138)Termination phase: Saturation
% 19.76/3.54 % (3566138)Time elapsed: 0.105 s
% 19.76/3.54 % (3566138)Peak memory usage: 89 MB
% 19.76/3.54 % (3566138)Instructions burned: 244 (million)
% 19.76/3.54 % (3566142)Instruction limit reached!
% 19.76/3.54 % (3566142)------------------------------
% 19.76/3.54 % (3566142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.54 % (3566142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.54 % (3566142)CaDiCaL version: 2.1.3
% 19.76/3.54 % (3566142)Termination reason: Instruction limit
% 19.76/3.54 % (3566142)Termination phase: Saturation
% 19.76/3.54 % (3566142)Time elapsed: 0.053 s
% 19.76/3.54 % (3566142)Peak memory usage: 89 MB
% 19.76/3.54 % (3566142)Instructions burned: 135 (million)
% 19.76/3.54 % (3566185)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4065275064:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 19.76/3.54 % (3566004)------------------------------
% 19.76/3.54 % (3566004)------------------------------
% 19.76/3.54 % (3566186)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3467410544:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 19.76/3.54 % (3566186)Instruction limit reached!
% 19.76/3.54 % (3566186)------------------------------
% 19.76/3.54 % (3566186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/3.54 % (3566186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/3.54 % (3566186)CaDiCaL version: 2.1.3
% 19.76/3.54 % (3566186)Termination reason: Instruction limit
% 19.76/3.54 % (3566186)Termination phase: Saturation
% 19.76/3.54 % (3566186)Time elapsed: 0.073 s
% 19.76/3.54 % (3566186)Peak memory usage: 88 MB
% 19.76/3.54 % (3566186)Instructions burned: 193 (million)
% 19.76/3.54 % (3566189)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3600935252:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 20.74/3.68 % (3566185)Instruction limit reached!
% 20.74/3.68 % (3566185)------------------------------
% 20.74/3.68 % (3566185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566185)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566185)Termination reason: Instruction limit
% 20.74/3.68 % (3566185)Termination phase: Saturation
% 20.74/3.68 % (3566185)Time elapsed: 0.192 s
% 20.74/3.68 % (3566185)Peak memory usage: 90 MB
% 20.74/3.68 % (3566185)Instructions burned: 501 (million)
% 20.74/3.68 % (3566190)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2738002103:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 20.74/3.68 % (3566189)Instruction limit reached!
% 20.74/3.68 % (3566189)------------------------------
% 20.74/3.68 % (3566189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566189)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566189)Termination reason: Instruction limit
% 20.74/3.68 % (3566189)Termination phase: Saturation
% 20.74/3.68 % (3566189)Time elapsed: 0.099 s
% 20.74/3.68 % (3566189)Peak memory usage: 89 MB
% 20.74/3.68 % (3566189)Instructions burned: 265 (million)
% 20.74/3.68 % (3566190)Instruction limit reached!
% 20.74/3.68 % (3566190)------------------------------
% 20.74/3.68 % (3566190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566190)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566190)Termination reason: Instruction limit
% 20.74/3.68 % (3566190)Termination phase: Saturation
% 20.74/3.68 % (3566190)Time elapsed: 0.065 s
% 20.74/3.68 % (3566190)Peak memory usage: 89 MB
% 20.74/3.68 % (3566190)Instructions burned: 157 (million)
% 20.74/3.68 % (3566192)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=1363060273:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 20.74/3.68 % (3566194)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1753475069:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 20.74/3.68 % (3566195)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=957990382:i=180:bd=preordered:av=off_2984 on theBenchmark for (2984ds/180Mi)
% 20.74/3.68 % (3566195)Instruction limit reached!
% 20.74/3.68 % (3566195)------------------------------
% 20.74/3.68 % (3566195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566195)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566195)Termination reason: Instruction limit
% 20.74/3.68 % (3566195)Termination phase: Saturation
% 20.74/3.68 % (3566195)Time elapsed: 0.064 s
% 20.74/3.68 % (3566195)Peak memory usage: 88 MB
% 20.74/3.68 % (3566195)Instructions burned: 182 (million)
% 20.74/3.68 % (3566194)Instruction limit reached!
% 20.74/3.68 % (3566194)------------------------------
% 20.74/3.68 % (3566194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566194)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566194)Termination reason: Instruction limit
% 20.74/3.68 % (3566194)Termination phase: Saturation
% 20.74/3.68 % (3566194)Time elapsed: 0.207 s
% 20.74/3.68 % (3566194)Peak memory usage: 89 MB
% 20.74/3.68 % (3566194)Instructions burned: 540 (million)
% 20.74/3.68 % (3566141)Refutation not found, incomplete strategy
% 20.74/3.68 % (3566141)------------------------------
% 20.74/3.68 % (3566141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566141)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566141)Termination reason: Refutation not found, incomplete strategy
% 20.74/3.68 % (3566141)Time elapsed: 0.970 s
% 20.74/3.68 % (3566141)Peak memory usage: 134 MB
% 20.74/3.68 % (3566141)Instructions burned: 2152 (million)
% 20.74/3.68 % (3566199)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=3820056001:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi)
% 20.74/3.68 % (3566131)Instruction limit reached!
% 20.74/3.68 % (3566131)------------------------------
% 20.74/3.68 % (3566131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566131)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566131)Termination reason: Instruction limit
% 20.74/3.68 % (3566131)Termination phase: Saturation
% 20.74/3.68 % (3566131)Time elapsed: 1.190 s
% 20.74/3.68 % (3566131)Peak memory usage: 143 MB
% 20.74/3.68 % (3566131)Instructions burned: 3396 (million)
% 20.74/3.68 % (3566200)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=3567340209:i=412:gtgl=4:gtg=exists_all_2980 on theBenchmark for (2980ds/412Mi)
% 20.74/3.68 % (3566202)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=2764094659:s2pl=no:i=8478:s2at=4:nm=6_2980 on theBenchmark for (2980ds/8478Mi)
% 20.74/3.68 % (3566200)Refutation not found, incomplete strategy
% 20.74/3.68 % (3566200)------------------------------
% 20.74/3.68 % (3566200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566200)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566200)Termination reason: Refutation not found, incomplete strategy
% 20.74/3.68 % (3566200)Time elapsed: 0.069 s
% 20.74/3.68 % (3566200)Peak memory usage: 90 MB
% 20.74/3.68 % (3566200)Instructions burned: 116 (million)
% 20.74/3.68 % (3566141)------------------------------
% 20.74/3.68 % (3566141)------------------------------
% 20.74/3.68 % (3566205)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=3874881096:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2977 on theBenchmark for (2977ds/303Mi)
% 20.74/3.68 % (3566200)------------------------------
% 20.74/3.68 % (3566200)------------------------------
% 20.74/3.68 % (3566205)Refutation not found, incomplete strategy
% 20.74/3.68 % (3566205)------------------------------
% 20.74/3.68 % (3566205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566205)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566205)Termination reason: Refutation not found, incomplete strategy
% 20.74/3.68 % (3566205)Time elapsed: 0.011 s
% 20.74/3.68 % (3566205)Peak memory usage: 88 MB
% 20.74/3.68 % (3566205)Instructions burned: 21 (million)
% 20.74/3.68 % (3566207)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=816441072:st=4:i=720:sd=3:fsr=off:ss=axioms_2975 on theBenchmark for (2975ds/720Mi)
% 20.74/3.68 % (3566205)------------------------------
% 20.74/3.68 % (3566205)------------------------------
% 20.74/3.68 % (3566199)First to succeed.
% 20.74/3.68 % (3566199)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3565950"
% 20.74/3.68 % (3566001)Refutation not found, incomplete strategy
% 20.74/3.68 % (3566001)------------------------------
% 20.74/3.68 % (3566001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566001)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566001)Termination reason: Refutation not found, incomplete strategy
% 20.74/3.68 % (3566001)Time elapsed: 2.633 s
% 20.74/3.68 % (3566001)Peak memory usage: 152 MB
% 20.74/3.68 % (3566001)Instructions burned: 3899 (million)
% 20.74/3.68 % (3566209)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1080322188:i=598:bs=on:bd=preordered:av=off:ss=axioms_2973 on theBenchmark for (2973ds/598Mi)
% 20.74/3.68 % (3566207)Instruction limit reached!
% 20.74/3.68 % (3566207)------------------------------
% 20.74/3.68 % (3566207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.68 % (3566207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.68 % (3566207)CaDiCaL version: 2.1.3
% 20.74/3.68 % (3566207)Termination reason: Instruction limit
% 20.74/3.68 % (3566207)Termination phase: Saturation
% 20.74/3.68 % (3566207)Time elapsed: 0.303 s
% 20.74/3.68 % (3566207)Peak memory usage: 93 MB
% 20.74/3.68 % (3566207)Instructions burned: 720 (million)
% 20.74/3.68 % SZS status Satisfiable for theBenchmark
% 20.74/3.68 % SZS output start Saturation.
% See solution above
% 21.78/3.88 % SZS output start Definitions and Model Updates.
% 21.78/3.88 % SZS output end Definitions and Model Updates.
% 21.78/3.88 % (3566199)------------------------------
% 21.78/3.88 % (3566199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/3.88 % (3566199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/3.88 % (3566199)CaDiCaL version: 2.1.3
% 21.78/3.88 % (3566199)Termination reason: Satisfiable
% 21.78/3.88 % (3566199)Time elapsed: 0.754 s
% 21.78/3.88 % (3566199)Peak memory usage: 131 MB
% 21.78/3.88 % (3566199)Instructions burned: 1118 (million)
% 21.78/3.88 % (3566199)------------------------------
% 21.78/3.88 % (3566199)------------------------------
% 21.78/3.88 % (3565950)Success in time 3.01 s
% 21.78/3.88 % Vampire exiting
%------------------------------------------------------------------------------