%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV504-1.030 : 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:16:09 PM UTC 2026
% Result : Satisfiable 9.96s 1.98s
% Output : Saturation 11.25s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u14,negated_conjecture,
select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10))) != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10))) ).
cnf(u26,negated_conjecture,
select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10))) != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10))) ).
cnf(u33,negated_conjecture,
n1 = sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n19,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10)) ).
cnf(u62,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n1) ).
cnf(u77,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n1) ).
cnf(u93,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n1) ).
cnf(u106,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n1) ).
cnf(u119,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n1) ).
cnf(u131,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n1) ).
cnf(u145,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n1) ).
cnf(u158,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n1) ).
cnf(u171,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n1) ).
cnf(u184,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n1) ).
cnf(u198,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n1) ).
cnf(u211,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n1) ).
cnf(u224,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n1) ).
cnf(u237,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n1) ).
cnf(u251,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n1) ).
cnf(u264,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n1) ).
cnf(u277,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n1) ).
cnf(u290,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n1) ).
cnf(u304,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n1) ).
cnf(u317,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n1) ).
cnf(u330,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n2,e2),n1) ).
cnf(u343,negated_conjecture,
e1 != select(store(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n30,e30),n1) ).
cnf(u357,negated_conjecture,
e1 != select(store(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n9,e9),n1) ).
cnf(u370,negated_conjecture,
e1 != select(store(store(store(store(a1,n13,e13),n1,e1),n19,e19),n4,e4),n1) ).
cnf(u383,negated_conjecture,
e1 != select(store(store(store(a1,n13,e13),n1,e1),n19,e19),n1) ).
cnf(u441,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n1),X1),e1) ).
cnf(u395,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10),n1),X1),e1) ).
cnf(u413,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n1)) ).
cnf(u423,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n1),X1),e1) ).
cnf(u451,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n1) ).
cnf(u425,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n1)) ).
cnf(u469,negated_conjecture,
e1 != select(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n1) ).
cnf(u396,negated_conjecture,
select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10),n1)) = select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10),n1)) ).
cnf(u406,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n1) ).
cnf(u408,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n1),X1),e1) ).
cnf(u452,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n1)) ).
cnf(u418,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n1) ).
cnf(u462,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n1),X1),e1) ).
cnf(u436,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n1) ).
cnf(u464,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n1)) = select(X0,select(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n1)) ).
cnf(u446,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n1)) ).
cnf(u449,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n1)) ).
cnf(u431,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n1)) ).
cnf(u459,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n1),X1),e1) ).
cnf(u433,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n1) ).
cnf(u477,negated_conjecture,
e1 != e19 ).
cnf(u443,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n1)) ).
cnf(u460,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n1) ).
cnf(u426,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n1),X1),e1) ).
cnf(u389,negated_conjecture,
n1 = n19 ).
cnf(u444,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n1),X1),e1) ).
cnf(u458,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n1)) = select(X0,select(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n1)) ).
cnf(u397,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10),n1) ).
cnf(u407,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n1)) ).
cnf(u435,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n1),X1),e1) ).
cnf(u409,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n1) ).
cnf(u453,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n1),X1),e1) ).
cnf(u419,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n1)) ).
cnf(u463,negated_conjecture,
e1 != select(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n1) ).
cnf(u390,negated_conjecture,
n1 = sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n1,e1),n2,e2),n3,e3),n4,e4),n5,e5),n6,e6),n7,e7),n8,e8),n9,e9),n10,e10),n11,e11),n12,e12),n13,e13),n14,e14),n15,e15),n16,e16),n17,e17),n18,e18),n1,e19),n20,e20),n21,e21),n22,e22),n23,e23),n24,e24),n25,e25),n26,e26),n27,e27),n28,e28),n29,e29),n1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n10,e10)) ).
cnf(u392,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n1),X1),e1) ).
cnf(u402,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n1),X1),e1) ).
cnf(u420,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n1),X1),e1) ).
cnf(u448,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n1) ).
cnf(u430,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n1) ).
cnf(u432,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n1),X1),e1) ).
cnf(u415,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n1) ).
cnf(u417,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n1),X1),e1) ).
cnf(u461,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n1)) = select(X0,select(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n1)) ).
cnf(u427,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n1) ).
cnf(u471,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n1),X1),e1) ).
cnf(u470,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n1)) = select(X0,select(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n1)) ).
cnf(u410,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n1)) ).
cnf(u454,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n1) ).
cnf(u428,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n1)) ).
cnf(u456,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n1),X1),e1) ).
cnf(u438,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n1),X1),e1) ).
cnf(u466,negated_conjecture,
e1 != select(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n1) ).
cnf(u440,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n1)) ).
cnf(u391,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n1) ).
cnf(u393,negated_conjecture,
select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n1)) = select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n1)) ).
cnf(u403,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n1) ).
cnf(u421,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n1) ).
cnf(u404,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n1)) ).
cnf(u414,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n1),X1),e1) ).
cnf(u416,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n1)) ).
cnf(u399,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n1),X1),e1) ).
cnf(u401,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n1)) ).
cnf(u411,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n1),X1),e1) ).
cnf(u455,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n1)) ).
cnf(u429,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n1),X1),e1) ).
cnf(u457,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n1) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u439,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n1) ).
cnf(u467,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n1)) = select(X0,select(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n1)) ).
cnf(u394,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n7,e7),n1) ).
cnf(u412,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n1) ).
cnf(u422,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n1)) ).
cnf(u450,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n1),X1),e1) ).
cnf(u424,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n1) ).
cnf(u468,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n1),X1),e1) ).
cnf(u434,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n1)) ).
cnf(u465,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n1),X1),e1) ).
cnf(u447,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n1),X1),e1) ).
cnf(u475,negated_conjecture,
select(X0,e1) = select(store(X0,e19,X1),e1) ).
cnf(u437,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n1)) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u476,negated_conjecture,
select(store(X0,e1,X1),e19) = select(X0,e19) ).
cnf(u445,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n1) ).
cnf(u442,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n1) ).
cnf(u405,negated_conjecture,
select(X0,e1) = select(store(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n1),X1),e1) ).
cnf(u398,negated_conjecture,
select(store(X0,e1,X1),select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n1)) = select(X0,select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n24,e24),n1)) ).
cnf(u400,negated_conjecture,
e1 != select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,n13,e13),n1,e1),n1,e19),n4,e4),n9,e9),n30,e30),n2,e2),n15,e15),n25,e25),n18,e18),n20,e20),n8,e8),n21,e21),n6,e6),n11,e11),n14,e14),n29,e29),n5,e5),n26,e26),n22,e22),n27,e27),n3,e3),n12,e12),n16,e16),n28,e28),n17,e17),n23,e23),n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV504-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n001.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 11:25:03 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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
% 8.13/1.74 % (291194)Input is clausal, will run a generic CNF schedule.
% 8.13/1.74 % (291205)dis-21_1_sil=8000:lcm=predicate:random_seed=3985012615: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)
% 8.13/1.74 % (291205)Refutation not found, incomplete strategy
% 8.13/1.74 % (291205)------------------------------
% 8.13/1.74 % (291205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/1.74 % (291205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.74 % (291205)CaDiCaL version: 2.1.3
% 8.13/1.74 % (291205)Termination reason: Refutation not found, incomplete strategy
% 8.13/1.74 % (291205)Time elapsed: 0.001 s
% 8.13/1.74 % (291205)Peak memory usage: 88 MB
% 8.13/1.74 % (291205)Instructions burned: 2 (million)
% 8.13/1.74 % (291203)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=135299490:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.13/1.74 % (291204)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2050861190:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.13/1.74 % (291202)lrs+10_1_sil=8000:sp=occurrence:random_seed=2541591156:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.13/1.74 % (291200)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3870821024:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.13/1.74 % (291199)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=667889517:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.13/1.74 % (291201)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1471998264:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.13/1.74 % (291202)Instruction limit reached!
% 8.13/1.74 % (291202)------------------------------
% 8.13/1.74 % (291202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/1.74 % (291202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.74 % (291202)CaDiCaL version: 2.1.3
% 8.13/1.74 % (291202)Termination reason: Instruction limit
% 8.13/1.74 % (291202)Termination phase: Saturation
% 8.13/1.74 % (291202)Time elapsed: 0.045 s
% 8.13/1.74 % (291202)Peak memory usage: 88 MB
% 8.13/1.74 % (291202)Instructions burned: 109 (million)
% 8.13/1.74 % (291203)Instruction limit reached!
% 8.13/1.74 % (291203)------------------------------
% 8.13/1.74 % (291203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/1.74 % (291203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.74 % (291203)CaDiCaL version: 2.1.3
% 8.13/1.74 % (291203)Termination reason: Instruction limit
% 8.13/1.74 % (291203)Termination phase: Saturation
% 8.13/1.74 % (291203)Time elapsed: 0.050 s
% 8.13/1.74 % (291203)Peak memory usage: 88 MB
% 8.13/1.74 % (291203)Instructions burned: 114 (million)
% 8.13/1.74 % (291204)Instruction limit reached!
% 8.13/1.74 % (291204)------------------------------
% 8.13/1.74 % (291204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/1.74 % (291204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.74 % (291204)CaDiCaL version: 2.1.3
% 8.13/1.74 % (291204)Termination reason: Instruction limit
% 8.13/1.74 % (291204)Termination phase: Saturation
% 8.13/1.74 % (291204)Time elapsed: 0.074 s
% 8.13/1.74 % (291204)Peak memory usage: 89 MB
% 8.13/1.74 % (291204)Instructions burned: 180 (million)
% 8.13/1.74 % (291205)------------------------------
% 8.13/1.74 % (291205)------------------------------
% 8.13/1.74 % (291213)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=4149451238:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.13/1.74 % (291214)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2440526198: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)
% 8.13/1.74 % (291216)lrs+10_64_to=lpo:sil=8000:random_seed=1202939743:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 8.13/1.74 % (291215)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=114031961:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.13/1.74 % (291216)Instruction limit reached!
% 9.96/1.98 % (291216)------------------------------
% 9.96/1.98 % (291216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291216)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291216)Termination reason: Instruction limit
% 9.96/1.98 % (291216)Termination phase: Saturation
% 9.96/1.98 % (291216)Time elapsed: 0.026 s
% 9.96/1.98 % (291216)Peak memory usage: 88 MB
% 9.96/1.98 % (291216)Instructions burned: 132 (million)
% 9.96/1.98 % (291213)Instruction limit reached!
% 9.96/1.98 % (291213)------------------------------
% 9.96/1.98 % (291213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291213)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291213)Termination reason: Instruction limit
% 9.96/1.98 % (291213)Termination phase: Saturation
% 9.96/1.98 % (291213)Time elapsed: 0.059 s
% 9.96/1.98 % (291213)Peak memory usage: 88 MB
% 9.96/1.98 % (291213)Instructions burned: 143 (million)
% 9.96/1.98 % (291214)Instruction limit reached!
% 9.96/1.98 % (291214)------------------------------
% 9.96/1.98 % (291214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291214)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291214)Termination reason: Instruction limit
% 9.96/1.98 % (291214)Termination phase: Saturation
% 9.96/1.98 % (291214)Time elapsed: 0.072 s
% 9.96/1.98 % (291214)Peak memory usage: 88 MB
% 9.96/1.98 % (291214)Instructions burned: 192 (million)
% 9.96/1.98 % (291215)Instruction limit reached!
% 9.96/1.98 % (291215)------------------------------
% 9.96/1.98 % (291215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291215)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291215)Termination reason: Instruction limit
% 9.96/1.98 % (291215)Termination phase: Saturation
% 9.96/1.98 % (291215)Time elapsed: 0.090 s
% 9.96/1.98 % (291215)Peak memory usage: 89 MB
% 9.96/1.98 % (291215)Instructions burned: 221 (million)
% 9.96/1.98 % (291221)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1976204375:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 9.96/1.98 % (291221)Instruction limit reached!
% 9.96/1.98 % (291221)------------------------------
% 9.96/1.98 % (291221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291221)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291221)Termination reason: Instruction limit
% 9.96/1.98 % (291221)Termination phase: Saturation
% 9.96/1.98 % (291221)Time elapsed: 0.041 s
% 9.96/1.98 % (291221)Peak memory usage: 89 MB
% 9.96/1.98 % (291221)Instructions burned: 198 (million)
% 9.96/1.98 % (291222)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=783712833:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 9.96/1.98 % (291223)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=813037557:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 9.96/1.98 % (291224)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=2748299704:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 9.96/1.98 % (291224)Refutation not found, incomplete strategy
% 9.96/1.98 % (291224)------------------------------
% 9.96/1.98 % (291224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291224)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291224)Termination reason: Refutation not found, incomplete strategy
% 9.96/1.98 % (291224)Time elapsed: 0.024 s
% 9.96/1.98 % (291224)Peak memory usage: 89 MB
% 9.96/1.98 % (291224)Instructions burned: 52 (million)
% 9.96/1.98 % (291222)Instruction limit reached!
% 9.96/1.98 % (291222)------------------------------
% 9.96/1.98 % (291222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291222)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291222)Termination reason: Instruction limit
% 9.96/1.98 % (291222)Termination phase: Saturation
% 9.96/1.98 % (291222)Time elapsed: 0.099 s
% 9.96/1.98 % (291222)Peak memory usage: 90 MB
% 9.96/1.98 % (291222)Instructions burned: 158 (million)
% 9.96/1.98 % (291226)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3482143221:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 9.96/1.98 % (291226)Instruction limit reached!
% 9.96/1.98 % (291226)------------------------------
% 9.96/1.98 % (291226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291226)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291226)Termination reason: Instruction limit
% 9.96/1.98 % (291226)Termination phase: Saturation
% 9.96/1.98 % (291226)Time elapsed: 0.024 s
% 9.96/1.98 % (291226)Peak memory usage: 88 MB
% 9.96/1.98 % (291226)Instructions burned: 108 (million)
% 9.96/1.98 % (291232)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3971588785:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 9.96/1.98 % (291230)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=729463191:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 9.96/1.98 % (291224)------------------------------
% 9.96/1.98 % (291224)------------------------------
% 9.96/1.98 % (291201)Refutation not found, incomplete strategy
% 9.96/1.98 % (291201)------------------------------
% 9.96/1.98 % (291201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291201)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291201)Termination reason: Refutation not found, incomplete strategy
% 9.96/1.98 % (291201)Time elapsed: 0.736 s
% 9.96/1.98 % (291201)Peak memory usage: 128 MB
% 9.96/1.98 % (291201)Instructions burned: 1074 (million)
% 9.96/1.98 % (291230)Instruction limit reached!
% 9.96/1.98 % (291230)------------------------------
% 9.96/1.98 % (291230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291230)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291230)Termination reason: Instruction limit
% 9.96/1.98 % (291230)Termination phase: Saturation
% 9.96/1.98 % (291230)Time elapsed: 0.103 s
% 9.96/1.98 % (291230)Peak memory usage: 88 MB
% 9.96/1.98 % (291230)Instructions burned: 245 (million)
% 9.96/1.98 % (291235)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4033356804:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 9.96/1.98 % (291236)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3514679990:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 9.96/1.98 % (291235)Instruction limit reached!
% 9.96/1.98 % (291235)------------------------------
% 9.96/1.98 % (291235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291235)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291235)Termination reason: Instruction limit
% 9.96/1.98 % (291235)Termination phase: Saturation
% 9.96/1.98 % (291235)Time elapsed: 0.057 s
% 9.96/1.98 % (291235)Peak memory usage: 89 MB
% 9.96/1.98 % (291235)Instructions burned: 134 (million)
% 9.96/1.98 % (291201)------------------------------
% 9.96/1.98 % (291201)------------------------------
% 9.96/1.98 % (291236)First to succeed.
% 9.96/1.98 % (291236)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-291194"
% 9.96/1.98 % (291239)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1842926886:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 9.96/1.98 % (291232)Refutation not found, incomplete strategy
% 9.96/1.98 % (291232)------------------------------
% 9.96/1.98 % (291232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291232)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291232)Termination reason: Refutation not found, incomplete strategy
% 9.96/1.98 % (291232)Time elapsed: 0.451 s
% 9.96/1.98 % (291232)Peak memory usage: 130 MB
% 9.96/1.98 % (291232)Instructions burned: 1275 (million)
% 9.96/1.98 % (291240)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4103983095:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 9.96/1.98 % (291239)Instruction limit reached!
% 9.96/1.98 % (291239)------------------------------
% 9.96/1.98 % (291239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291239)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291239)Termination reason: Instruction limit
% 9.96/1.98 % (291239)Termination phase: Saturation
% 9.96/1.98 % (291239)Time elapsed: 0.078 s
% 9.96/1.98 % (291239)Peak memory usage: 88 MB
% 9.96/1.98 % (291239)Instructions burned: 191 (million)
% 9.96/1.98 % (291240)Instruction limit reached!
% 9.96/1.98 % (291240)------------------------------
% 9.96/1.98 % (291240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/1.98 % (291240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/1.98 % (291240)CaDiCaL version: 2.1.3
% 9.96/1.98 % (291240)Termination reason: Instruction limit
% 9.96/1.98 % (291240)Termination phase: Saturation
% 9.96/1.98 % (291240)Time elapsed: 0.109 s
% 9.96/1.98 % (291240)Peak memory usage: 89 MB
% 9.96/1.98 % (291240)Instructions burned: 264 (million)
% 9.96/1.98 % (291232)------------------------------
% 9.96/1.98 % (291232)------------------------------
% 9.96/1.98 % (291243)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4030320969:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 9.96/1.98 % SZS status Satisfiable for theBenchmark
% 9.96/1.98 % SZS output start Saturation.
% See solution above
% 11.25/2.09 % SZS output start Definitions and Model Updates.
% 11.25/2.09 % SZS output end Definitions and Model Updates.
% 11.25/2.09 % (291236)------------------------------
% 11.25/2.09 % (291236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.09 % (291236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.09 % (291236)CaDiCaL version: 2.1.3
% 11.25/2.09 % (291236)Termination reason: Satisfiable
% 11.25/2.09 % (291236)Time elapsed: 0.154 s
% 11.25/2.09 % (291236)Peak memory usage: 90 MB
% 11.25/2.09 % (291236)Instructions burned: 337 (million)
% 11.25/2.09 % (291236)------------------------------
% 11.25/2.09 % (291236)------------------------------
% 11.25/2.09 % (291194)Success in time 1.556 s
% 11.25/2.09 % Vampire exiting
%------------------------------------------------------------------------------