%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV503-1.040 : 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 : n014.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.10s 2.10s
% Output : Saturation 9.96s
% 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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19))) != 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(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19))) ).
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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19))) != 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(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19))) ).
cnf(u33,negated_conjecture,
n40 = 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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n40,e40),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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19)) ).
cnf(u62,negated_conjecture,
e40 != 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(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n40) ).
cnf(u77,negated_conjecture,
e40 != 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(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n40) ).
cnf(u93,negated_conjecture,
e40 != 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(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n40) ).
cnf(u106,negated_conjecture,
e40 != 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(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n40) ).
cnf(u119,negated_conjecture,
e40 != 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(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n40) ).
cnf(u131,negated_conjecture,
e40 != 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(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n40) ).
cnf(u145,negated_conjecture,
e40 != 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(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n9,e9),n40) ).
cnf(u158,negated_conjecture,
e40 != 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n1,e1),n40) ).
cnf(u171,negated_conjecture,
e40 != 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n39,e39),n40) ).
cnf(u184,negated_conjecture,
e40 != 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n40,e40),n38,e38),n40) ).
cnf(u223,negated_conjecture,
e40 != 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n38) ).
cnf(u217,negated_conjecture,
e40 != 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(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n38) ).
cnf(u209,negated_conjecture,
select(store(X0,e40,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(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n38)) = 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(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n38)) ).
cnf(u211,negated_conjecture,
e40 != 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(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n38) ).
cnf(u225,negated_conjecture,
select(X0,e40) = 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n38),X1),e40) ).
cnf(u221,negated_conjecture,
select(store(X0,e40,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(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n38)) = 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(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n38)) ).
cnf(u203,negated_conjecture,
select(store(X0,e40,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(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n38)) = 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(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n38)) ).
cnf(u213,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n38),X1),e40) ).
cnf(u215,negated_conjecture,
select(store(X0,e40,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(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n38)) = 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(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n38)) ).
cnf(u207,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n38),X1),e40) ).
cnf(u201,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n38),X1),e40) ).
cnf(u193,negated_conjecture,
e40 != 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(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n38) ).
cnf(u195,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(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n38)) = select(store(X0,e40,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(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n38)) ).
cnf(u232,negated_conjecture,
select(X0,e40) = select(store(X0,e38,X1),e40) ).
cnf(u205,negated_conjecture,
e40 != 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(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n38) ).
cnf(u234,negated_conjecture,
e38 != e40 ).
cnf(u197,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19),n38),X1),e40) ).
cnf(u226,negated_conjecture,
e40 != 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n38) ).
cnf(u199,negated_conjecture,
e40 != 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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19),n38) ).
cnf(u228,negated_conjecture,
select(X0,e40) = 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n38),X1),e40) ).
cnf(u224,negated_conjecture,
select(store(X0,e40,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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n38)) = 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n38)) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u216,negated_conjecture,
select(X0,e40) = 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(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n38),X1),e40) ).
cnf(u218,negated_conjecture,
select(store(X0,e40,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(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n38)) = 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(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n38)) ).
cnf(u210,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n38),X1),e40) ).
cnf(u220,negated_conjecture,
e40 != 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(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n38) ).
cnf(u222,negated_conjecture,
select(X0,e40) = 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(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n38),X1),e40) ).
cnf(u212,negated_conjecture,
select(store(X0,e40,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(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n38)) = 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(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n38)) ).
cnf(u214,negated_conjecture,
e40 != 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(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n38) ).
cnf(u208,negated_conjecture,
e40 != 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(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n38) ).
cnf(u200,negated_conjecture,
select(store(X0,e40,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(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n38)) = 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(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n38)) ).
cnf(u202,negated_conjecture,
e40 != 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(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n38) ).
cnf(u194,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n38),X1),e40) ).
cnf(u204,negated_conjecture,
select(X0,e40) = 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(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n38),X1),e40) ).
cnf(u206,negated_conjecture,
select(store(X0,e40,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(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n38)) = 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(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n38)) ).
cnf(u196,negated_conjecture,
e40 != 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(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n38) ).
cnf(u198,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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19),n38)) = select(store(X0,e40,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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19),n38)) ).
cnf(u192,negated_conjecture,
n38 = 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(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),n30,e30),n31,e31),n32,e32),n33,e33),n34,e34),n35,e35),n36,e36),n37,e37),n38,e38),n39,e39),n38,e40),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(store(store(store(store(store(store(store(store(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n5,e5),n4,e4),n30,e30),n15,e15),n34,e34),n28,e28),n29,e29),n19,e19)) ).
cnf(u233,negated_conjecture,
select(store(X0,e40,X1),e38) = select(X0,e38) ).
cnf(u191,negated_conjecture,
n38 = n40 ).
cnf(u227,negated_conjecture,
select(store(X0,e40,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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n38)) = 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,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n38)) ).
cnf(u219,negated_conjecture,
select(X0,e40) = 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(store(store(a1,n16,e16),n14,e14),n24,e24),n11,e11),n25,e25),n17,e17),n7,e7),n32,e32),n6,e6),n18,e18),n37,e37),n31,e31),n13,e13),n12,e12),n36,e36),n20,e20),n35,e35),n23,e23),n26,e26),n21,e21),n27,e27),n10,e10),n22,e22),n8,e8),n33,e33),n2,e2),n38,e40),n38,e38),n39,e39),n1,e1),n9,e9),n3,e3),n38),X1),e40) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV503-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 % Computer : n014.cluster.edu
% 0.10/0.24 % Model : x86_64 x86_64
% 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24 % Memory : 8046.5625MB
% 0.10/0.24 % OS : Linux 6.8.0-71-generic
% 0.10/0.24 % CPULimit : 300
% 0.10/0.24 % WCLimit : 300
% 0.10/0.24 % DateTime : Mon Sep 28 11:21:16 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.30 Running first-order theorem proving
% 0.24/0.30 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
% 6.78/1.90 % (1717659)Input is clausal, will run a generic CNF schedule.
% 6.78/1.90 % (1717732)dis-21_1_sil=8000:lcm=predicate:random_seed=60142436: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)
% 6.78/1.90 % (1717732)Refutation not found, incomplete strategy
% 6.78/1.90 % (1717732)------------------------------
% 6.78/1.90 % (1717732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/1.90 % (1717732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/1.90 % (1717732)CaDiCaL version: 2.1.3
% 6.78/1.90 % (1717732)Termination reason: Refutation not found, incomplete strategy
% 6.78/1.90 % (1717732)Time elapsed: 0.001 s
% 6.78/1.90 % (1717732)Peak memory usage: 88 MB
% 6.78/1.90 % (1717732)Instructions burned: 3 (million)
% 6.78/1.90 % (1717730)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3979592904:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.78/1.90 % (1717729)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=331253267:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.78/1.90 % (1717722)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=1854405722:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.78/1.90 % (1717724)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2618086805:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.78/1.90 % (1717727)lrs+10_1_sil=8000:sp=occurrence:random_seed=2906845754:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.78/1.90 % (1717725)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1317466179:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.78/1.90 % (1717727)Instruction limit reached!
% 6.78/1.90 % (1717727)------------------------------
% 6.78/1.90 % (1717727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/1.90 % (1717727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/1.90 % (1717727)CaDiCaL version: 2.1.3
% 6.78/1.90 % (1717727)Termination reason: Instruction limit
% 6.78/1.90 % (1717727)Termination phase: Saturation
% 6.78/1.90 % (1717727)Time elapsed: 0.045 s
% 6.78/1.90 % (1717727)Peak memory usage: 88 MB
% 6.78/1.90 % (1717727)Instructions burned: 108 (million)
% 6.78/1.90 % (1717729)Instruction limit reached!
% 6.78/1.90 % (1717729)------------------------------
% 6.78/1.90 % (1717729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/1.90 % (1717729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/1.90 % (1717729)CaDiCaL version: 2.1.3
% 6.78/1.90 % (1717729)Termination reason: Instruction limit
% 6.78/1.90 % (1717729)Termination phase: Saturation
% 6.78/1.90 % (1717729)Time elapsed: 0.047 s
% 6.78/1.90 % (1717729)Peak memory usage: 88 MB
% 6.78/1.90 % (1717729)Instructions burned: 114 (million)
% 6.78/1.90 % (1717730)Instruction limit reached!
% 6.78/1.90 % (1717730)------------------------------
% 6.78/1.90 % (1717730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/1.90 % (1717730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/1.90 % (1717730)CaDiCaL version: 2.1.3
% 6.78/1.90 % (1717730)Termination reason: Instruction limit
% 6.78/1.90 % (1717730)Termination phase: Saturation
% 6.78/1.90 % (1717730)Time elapsed: 0.075 s
% 6.78/1.90 % (1717730)Peak memory usage: 89 MB
% 6.78/1.90 % (1717730)Instructions burned: 183 (million)
% 6.78/1.90 % (1717732)------------------------------
% 6.78/1.90 % (1717732)------------------------------
% 6.78/1.90 % (1717787)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1179756646:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 6.78/1.90 % (1717786)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=2011499134:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.78/1.90 % (1717789)lrs+10_64_to=lpo:sil=8000:random_seed=1194797053:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 6.78/1.90 % (1717788)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=441825720:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.10/2.10 % (1717789)Instruction limit reached!
% 9.10/2.10 % (1717789)------------------------------
% 9.10/2.10 % (1717789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717789)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717789)Termination reason: Instruction limit
% 9.10/2.10 % (1717789)Termination phase: Saturation
% 9.10/2.10 % (1717789)Time elapsed: 0.026 s
% 9.10/2.10 % (1717789)Peak memory usage: 88 MB
% 9.10/2.10 % (1717789)Instructions burned: 131 (million)
% 9.10/2.10 % (1717786)Instruction limit reached!
% 9.10/2.10 % (1717786)------------------------------
% 9.10/2.10 % (1717786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717786)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717786)Termination reason: Instruction limit
% 9.10/2.10 % (1717786)Termination phase: Saturation
% 9.10/2.10 % (1717786)Time elapsed: 0.059 s
% 9.10/2.10 % (1717786)Peak memory usage: 89 MB
% 9.10/2.10 % (1717786)Instructions burned: 146 (million)
% 9.10/2.10 % (1717787)Instruction limit reached!
% 9.10/2.10 % (1717787)------------------------------
% 9.10/2.10 % (1717787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717787)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717787)Termination reason: Instruction limit
% 9.10/2.10 % (1717787)Termination phase: Saturation
% 9.10/2.10 % (1717787)Time elapsed: 0.071 s
% 9.10/2.10 % (1717787)Peak memory usage: 89 MB
% 9.10/2.10 % (1717787)Instructions burned: 192 (million)
% 9.10/2.10 % (1717788)Instruction limit reached!
% 9.10/2.10 % (1717788)------------------------------
% 9.10/2.10 % (1717788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717788)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717788)Termination reason: Instruction limit
% 9.10/2.10 % (1717788)Termination phase: Saturation
% 9.10/2.10 % (1717788)Time elapsed: 0.088 s
% 9.10/2.10 % (1717788)Peak memory usage: 89 MB
% 9.10/2.10 % (1717788)Instructions burned: 221 (million)
% 9.10/2.10 % (1717831)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4075009231:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 9.10/2.10 % (1717831)Instruction limit reached!
% 9.10/2.10 % (1717831)------------------------------
% 9.10/2.10 % (1717831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717831)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717831)Termination reason: Instruction limit
% 9.10/2.10 % (1717831)Termination phase: Saturation
% 9.10/2.10 % (1717831)Time elapsed: 0.039 s
% 9.10/2.10 % (1717831)Peak memory usage: 89 MB
% 9.10/2.10 % (1717831)Instructions burned: 199 (million)
% 9.10/2.10 % (1717835)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1621442726:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 9.10/2.10 % (1717839)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1094908124:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi)
% 9.10/2.10 % (1717844)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=2427709488:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 9.10/2.10 % (1717847)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1661440659:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 9.10/2.10 % (1717835)Instruction limit reached!
% 9.10/2.10 % (1717835)------------------------------
% 9.10/2.10 % (1717835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717835)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717835)Termination reason: Instruction limit
% 9.10/2.10 % (1717835)Termination phase: Saturation
% 9.10/2.10 % (1717835)Time elapsed: 0.089 s
% 9.10/2.10 % (1717835)Peak memory usage: 91 MB
% 9.10/2.10 % (1717835)Instructions burned: 157 (million)
% 9.10/2.10 % (1717847)Instruction limit reached!
% 9.10/2.10 % (1717847)------------------------------
% 9.10/2.10 % (1717847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717847)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717847)Termination reason: Instruction limit
% 9.10/2.10 % (1717847)Termination phase: Saturation
% 9.10/2.10 % (1717847)Time elapsed: 0.024 s
% 9.10/2.10 % (1717847)Peak memory usage: 88 MB
% 9.10/2.10 % (1717847)Instructions burned: 110 (million)
% 9.10/2.10 % (1717844)Instruction limit reached!
% 9.10/2.10 % (1717844)------------------------------
% 9.10/2.10 % (1717844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717844)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717844)Termination reason: Instruction limit
% 9.10/2.10 % (1717844)Termination phase: Saturation
% 9.10/2.10 % (1717844)Time elapsed: 0.044 s
% 9.10/2.10 % (1717844)Peak memory usage: 89 MB
% 9.10/2.10 % (1717844)Instructions burned: 107 (million)
% 9.10/2.10 % (1717852)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1617173217:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 9.10/2.10 % (1717851)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2101440553:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 9.10/2.10 % (1717853)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3944679776:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 9.10/2.10 % (1717853)Instruction limit reached!
% 9.10/2.10 % (1717853)------------------------------
% 9.10/2.10 % (1717853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717853)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717853)Termination reason: Instruction limit
% 9.10/2.10 % (1717853)Termination phase: Saturation
% 9.10/2.10 % (1717853)Time elapsed: 0.055 s
% 9.10/2.10 % (1717853)Peak memory usage: 89 MB
% 9.10/2.10 % (1717853)Instructions burned: 137 (million)
% 9.10/2.10 % (1717851)Instruction limit reached!
% 9.10/2.10 % (1717851)------------------------------
% 9.10/2.10 % (1717851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717851)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717851)Termination reason: Instruction limit
% 9.10/2.10 % (1717851)Termination phase: Saturation
% 9.10/2.10 % (1717851)Time elapsed: 0.101 s
% 9.10/2.10 % (1717851)Peak memory usage: 89 MB
% 9.10/2.10 % (1717851)Instructions burned: 242 (million)
% 9.10/2.10 % (1717725)Refutation not found, incomplete strategy
% 9.10/2.10 % (1717725)------------------------------
% 9.10/2.10 % (1717725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717725)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717725)Termination reason: Refutation not found, incomplete strategy
% 9.10/2.10 % (1717725)Time elapsed: 0.724 s
% 9.10/2.10 % (1717725)Peak memory usage: 130 MB
% 9.10/2.10 % (1717725)Instructions burned: 1079 (million)
% 9.10/2.10 % (1717857)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2436798161:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 9.10/2.10 % (1717858)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4130709249:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 9.10/2.10 % (1717858)Instruction limit reached!
% 9.10/2.10 % (1717858)------------------------------
% 9.10/2.10 % (1717858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717858)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717858)Termination reason: Instruction limit
% 9.10/2.10 % (1717858)Termination phase: Saturation
% 9.10/2.10 % (1717858)Time elapsed: 0.075 s
% 9.10/2.10 % (1717858)Peak memory usage: 88 MB
% 9.10/2.10 % (1717858)Instructions burned: 192 (million)
% 9.10/2.10 % (1717857)First to succeed.
% 9.10/2.10 % (1717857)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1717659"
% 9.10/2.10 % (1717725)------------------------------
% 9.10/2.10 % (1717725)------------------------------
% 9.10/2.10 % (1717861)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1988490859:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 9.10/2.10 % (1717861)Instruction limit reached!
% 9.10/2.10 % (1717861)------------------------------
% 9.10/2.10 % (1717861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.10 % (1717861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.10 % (1717861)CaDiCaL version: 2.1.3
% 9.10/2.10 % (1717861)Termination reason: Instruction limit
% 9.10/2.10 % (1717861)Termination phase: Saturation
% 9.10/2.10 % (1717861)Time elapsed: 0.105 s
% 9.10/2.10 % (1717861)Peak memory usage: 89 MB
% 9.10/2.10 % (1717861)Instructions burned: 266 (million)
% 9.10/2.10 % (1717862)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3553206911:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 9.10/2.10 % SZS status Satisfiable for theBenchmark
% 9.10/2.10 % SZS output start Saturation.
% See solution above
% 9.96/2.29 % SZS output start Definitions and Model Updates.
% 9.96/2.29 % SZS output end Definitions and Model Updates.
% 9.96/2.29 % (1717857)------------------------------
% 9.96/2.29 % (1717857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.96/2.29 % (1717857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.96/2.29 % (1717857)CaDiCaL version: 2.1.3
% 9.96/2.29 % (1717857)Termination reason: Satisfiable
% 9.96/2.29 % (1717857)Time elapsed: 0.145 s
% 9.96/2.29 % (1717857)Peak memory usage: 90 MB
% 9.96/2.29 % (1717857)Instructions burned: 344 (million)
% 9.96/2.29 % (1717857)------------------------------
% 9.96/2.29 % (1717857)------------------------------
% 9.96/2.29 % (1717659)Success in time 1.305 s
% 9.96/2.29 % Vampire exiting
%------------------------------------------------------------------------------