%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV504-1.030 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:30:53 PM UTC 2025 % Result : Satisfiable 12.96s 4.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SWV504-1.030 : TPTP v9.0.0. Released v4.0.0. % 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.08/0.28 % Computer : n024.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Wed Apr 9 03:38:21 EDT 2025 % 0.08/0.28 % CPUTime : % 12.96/4.53 % 12.96/4.53 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.96/4.53 % 12.96/4.53 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.96/4.54 %$ store > sk > select > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n30 > n3 > n29 > n28 > n27 > n26 > n25 > n24 > n23 > n22 > n21 > n20 > n2 > n19 > n18 > n17 > n16 > n15 > n14 > n13 > n12 > n11 > n10 > n1 > e9 > e8 > e7 > e6 > e5 > e4 > e30 > e3 > e29 > e28 > e27 > e26 > e25 > e24 > e23 > e22 > e21 > e20 > e2 > e19 > e18 > e17 > e16 > e15 > e14 > e13 > e12 > e11 > e10 > e1 > a1 % 12.96/4.54 % 12.96/4.54 %Foreground sorts: % 12.96/4.54 % 12.96/4.54 % 12.96/4.54 %Background operators: % 12.96/4.54 % 12.96/4.54 % 12.96/4.54 %Foreground operators: % 12.96/4.54 tff(e29, type, e29: $i). % 12.96/4.54 tff(a1, type, a1: $i). % 12.96/4.54 tff(n22, type, n22: $i). % 12.96/4.54 tff(n27, type, n27: $i). % 12.96/4.54 tff(n16, type, n16: $i). % 12.96/4.54 tff(n12, type, n12: $i). % 12.96/4.54 tff(e1, type, e1: $i). % 12.96/4.54 tff(e8, type, e8: $i). % 12.96/4.54 tff(e21, type, e21: $i). % 12.96/4.54 tff(n24, type, n24: $i). % 12.96/4.54 tff(e15, type, e15: $i). % 12.96/4.54 tff(e18, type, e18: $i). % 12.96/4.54 tff(e24, type, e24: $i). % 12.96/4.54 tff(store, type, store: ($i * $i * $i) > $i). % 12.96/4.54 tff(n23, type, n23: $i). % 12.96/4.54 tff(n8, type, n8: $i). % 12.96/4.54 tff(e20, type, e20: $i). % 12.96/4.54 tff(e19, type, e19: $i). % 12.96/4.54 tff(e16, type, e16: $i). % 12.96/4.54 tff(n30, type, n30: $i). % 12.96/4.54 tff(e2, type, e2: $i). % 12.96/4.54 tff(n28, type, n28: $i). % 12.96/4.54 tff(n9, type, n9: $i). % 12.96/4.54 tff(e13, type, e13: $i). % 12.96/4.54 tff(n3, type, n3: $i). % 12.96/4.54 tff(e22, type, e22: $i). % 12.96/4.54 tff(n1, type, n1: $i). % 12.96/4.54 tff(n29, type, n29: $i). % 12.96/4.54 tff(e9, type, e9: $i). % 12.96/4.54 tff(n7, type, n7: $i). % 12.96/4.54 tff(e25, type, e25: $i). % 12.96/4.54 tff(e26, type, e26: $i). % 12.96/4.54 tff(n6, type, n6: $i). % 12.96/4.54 tff(e17, type, e17: $i). % 12.96/4.54 tff(n26, type, n26: $i). % 12.96/4.54 tff(e27, type, e27: $i). % 12.96/4.54 tff(e10, type, e10: $i). % 12.96/4.54 tff(e7, type, e7: $i). % 12.96/4.54 tff(n13, type, n13: $i). % 12.96/4.54 tff(sk, type, sk: ($i * $i) > $i). % 12.96/4.54 tff(n4, type, n4: $i). % 12.96/4.54 tff(n10, type, n10: $i). % 12.96/4.54 tff(n14, type, n14: $i). % 12.96/4.54 tff(n15, type, n15: $i). % 12.96/4.54 tff(n17, type, n17: $i). % 12.96/4.54 tff(e30, type, e30: $i). % 12.96/4.54 tff(select, type, select: ($i * $i) > $i). % 12.96/4.54 tff(n20, type, n20: $i). % 12.96/4.54 tff(e23, type, e23: $i). % 12.96/4.54 tff(n18, type, n18: $i). % 12.96/4.54 tff(e14, type, e14: $i). % 12.96/4.54 tff(n11, type, n11: $i). % 12.96/4.54 tff(e12, type, e12: $i). % 12.96/4.54 tff(e4, type, e4: $i). % 12.96/4.54 tff(e6, type, e6: $i). % 12.96/4.54 tff(n19, type, n19: $i). % 12.96/4.54 tff(n2, type, n2: $i). % 12.96/4.54 tff(e11, type, e11: $i). % 12.96/4.54 tff(e28, type, e28: $i). % 12.96/4.54 tff(n5, type, n5: $i). % 12.96/4.54 tff(e3, type, e3: $i). % 12.96/4.54 tff(n25, type, n25: $i). % 12.96/4.54 tff(e5, type, e5: $i). % 12.96/4.54 tff(n21, type, n21: $i). % 12.96/4.54 % 12.96/4.54 %Saturated clause set: % 12.96/4.54 tff(c_2439, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n24, e24), n1))). % 12.96/4.54 tff(c_2435, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n24, e24), n1)!=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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 12.96/4.54 tff(c_2021, plain, (select(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), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1))). % 12.96/4.54 tff(c_2425, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n1))). % 12.96/4.54 tff(c_2415, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1))). % 12.96/4.55 tff(c_2411, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1))). % 12.96/4.55 tff(c_2407, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n1))). % 13.08/4.55 tff(c_2402, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1))). % 13.08/4.55 tff(c_2398, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n1))). % 13.08/4.55 tff(c_2393, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1))). % 13.08/4.55 tff(c_2388, plain, (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), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n24, e24), n1, e7), n10, e10), n1)!=e1)). % 13.08/4.55 tff(c_2384, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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)!=e7)). % 13.08/4.55 tff(c_2380, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n24, e24), n1)!=e1)). % 13.08/4.55 tff(c_2376, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.55 tff(c_2372, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1))). % 13.08/4.55 tff(c_2368, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n1))). % 13.08/4.55 tff(c_2364, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n1)!=e1)). % 13.08/4.55 tff(c_2360, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.55 tff(c_2355, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n1))). % 13.08/4.55 tff(c_2351, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n1)!=e1)). % 13.08/4.55 tff(c_2347, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.55 tff(c_2307, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1))). % 13.08/4.55 tff(c_2339, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n1)!=e1)). % 13.08/4.55 tff(c_2335, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.55 tff(c_2331, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n1)!=e1)). % 13.08/4.55 tff(c_2326, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n1)!=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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 13.08/4.55 tff(c_2322, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.55 tff(c_2318, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1))). % 13.08/4.55 tff(c_2313, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e3)). % 13.08/4.55 tff(c_2308, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n1)!=e1)). % 13.08/4.55 tff(c_2303, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.55 tff(c_2299, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1))). % 13.08/4.56 tff(c_2295, plain, (select(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), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e3)). % 13.08/4.56 tff(c_2291, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n1)!=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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 13.08/4.56 tff(c_2287, plain, (select(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), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.56 tff(c_2283, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1)!=select(store(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n1))). % 13.08/4.56 tff(c_2279, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e3)). % 13.08/4.56 tff(c_2275, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=e7)). % 13.08/4.56 tff(c_2271, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n1)!=select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1))). % 13.08/4.56 tff(c_2230, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n1))). % 13.08/4.56 tff(c_2264, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e3)). % 13.08/4.56 tff(c_2260, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e7)). % 13.08/4.56 tff(c_2255, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1)!=select(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n1))). % 13.08/4.56 tff(c_2251, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n1))). % 13.08/4.56 tff(c_2247, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e3)). % 13.08/4.56 tff(c_2243, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e5)). % 13.08/4.56 tff(c_2239, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e7)). % 13.08/4.56 tff(c_2235, plain, (select(store(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n1)!=e9)). % 13.08/4.56 tff(c_2231, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e3)). % 13.08/4.56 tff(c_2226, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e5)). % 13.08/4.56 tff(c_2222, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e7)). % 13.08/4.56 tff(c_2217, plain, (e9!=e2)). % 13.08/4.56 tff(c_2218, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n1)!=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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 13.08/4.56 tff(c_2212, plain, (select(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n1)!=e9)). % 13.08/4.56 tff(c_2208, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e3)). % 13.08/4.56 tff(c_2204, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e5)). % 13.08/4.56 tff(c_2200, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e7)). % 13.08/4.56 tff(c_2160, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1))). % 13.08/4.56 tff(c_2193, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e3)). % 13.08/4.56 tff(c_2189, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e5)). % 13.08/4.56 tff(c_2185, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e7)). % 13.08/4.56 tff(c_2181, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n1))). % 13.08/4.56 tff(c_2177, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e3)). % 13.08/4.56 tff(c_2173, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e6)). % 13.08/4.56 tff(c_2169, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e5)). % 13.08/4.56 tff(c_2165, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e7)). % 13.08/4.56 tff(c_2161, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n1)!=e3)). % 13.08/4.57 tff(c_2156, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n1)!=e6)). % 13.08/4.57 tff(c_2152, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n1)!=e5)). % 13.08/4.57 tff(c_2148, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n1)!=e7)). % 13.17/4.57 tff(c_2144, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n1)!=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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 13.17/4.57 tff(c_2140, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n1)!=e8)). % 13.17/4.57 tff(c_2136, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n1)!=e3)). % 13.17/4.57 tff(c_2132, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n1)!=e5)). % 13.17/4.57 tff(c_2128, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n1)!=e6)). % 13.17/4.57 tff(c_2124, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n13, e13), n1)!=e7)). % 13.17/4.57 tff(c_2056, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n1))). % 13.17/4.57 tff(c_2002, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n1)!=e8)). % 13.17/4.57 tff(c_2003, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n1)!=e5)). % 13.17/4.57 tff(c_2004, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n1)!=e6)). % 13.17/4.57 tff(c_2108, plain, (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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1)!=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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n1))). % 13.17/4.57 tff(c_2006, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n1)!=e7)). % 13.17/4.57 tff(c_2101, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n12, e12), n1)!=e3)). % 13.17/4.57 tff(c_2007, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1)!=e3)). % 13.17/4.57 tff(c_2008, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1)!=e5)). % 13.17/4.57 tff(c_2009, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1)!=e6)). % 13.17/4.57 tff(c_2010, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1)!=e7)). % 13.17/4.57 tff(c_2001, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n11, e11), n1)!=e8)). % 13.17/4.57 tff(c_2011, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1)!=e3)). % 13.17/4.57 tff(c_2077, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n1)!=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, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 13.17/4.57 tff(c_2012, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1)!=e5)). % 13.17/4.57 tff(c_2013, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1)!=e6)). % 13.17/4.57 tff(c_2015, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1)!=e7)). % 13.17/4.57 tff(c_2000, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n10, e10), n1)!=e8)). % 13.17/4.57 tff(c_2020, plain, (select(store(store(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1, e2), n15, e15), n1)!=e8)). % 13.17/4.57 tff(c_2023, plain, (select(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1)!=e7)). % 13.17/4.57 tff(c_2024, plain, (select(store(store(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1, e9), n30, e30), n1)!=e6)). % 13.17/4.57 tff(c_2028, plain, (e9!=e3)). % 13.17/4.57 tff(c_2043, plain, (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), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1, e3), n12, e12), n16, e16), n28, e28), n17, e17), n23, e23), n24, e24), n1, e7), n10, e10))=n1)). % 13.17/4.57 tff(c_2029, plain, (e9!=e5)). % 13.17/4.57 tff(c_2030, plain, (e9!=e6)). % 13.17/4.57 tff(c_2039, plain, (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), n1, e9), n30, e30), n1, e2), n15, e15), n25, e25), n18, e18), n20, e20), n1, e8), n21, e21), n1, e6), n11, e11), n14, e14), n29, e29), n1, e5), n26, e26), n22, e22), n27, e27), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, 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), n1))). % 13.17/4.57 tff(c_2032, plain, (e9!=e7)). % 13.17/4.57 tff(c_2027, plain, (e9!=e8)). % 13.17/4.57 tff(c_1993, plain, (n9=n1)). % 13.17/4.57 tff(c_1902, plain, (e8!=e3)). % 13.17/4.57 tff(c_1901, plain, (e8!=e2)). % 13.17/4.57 tff(c_1903, plain, (e8!=e5)). % 13.17/4.57 tff(c_1904, plain, (e8!=e6)). % 13.17/4.57 tff(c_1897, plain, (e8!=e7)). % 13.17/4.57 tff(c_1804, plain, (n8=n1)). % 13.17/4.57 tff(c_1503, plain, (select(store(store(store(a1, n13, e13), n1, e1), n19, e19), n1)!=e7)). % 13.17/4.57 tff(c_1499, plain, (select(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1)!=e7)). % 13.17/4.58 tff(c_1476, plain, (e7!=e2)). % 13.17/4.58 tff(c_1473, plain, (e7!=e1)). % 13.17/4.58 tff(c_1477, plain, (e7!=e3)). % 13.17/4.58 tff(c_1478, plain, (e7!=e5)). % 13.17/4.58 tff(c_1472, plain, (e7!=e6)). % 13.17/4.58 tff(c_1405, plain, (n7=n1)). % 13.17/4.58 tff(c_1156, plain, (e6!=e1)). % 13.17/4.58 tff(c_1151, plain, (select(store(store(store(a1, n13, e13), n1, e1), n19, e19), n1)!=e6)). % 13.17/4.58 tff(c_1147, plain, (select(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1)!=e6)). % 13.17/4.58 tff(c_1134, plain, (e6!=e3)). % 13.17/4.58 tff(c_1135, plain, (e6!=e2)). % 13.17/4.58 tff(c_1131, plain, (e6!=e5)). % 13.17/4.58 tff(c_1089, plain, (n6=n1)). % 13.17/4.58 tff(c_941, plain, (e5!=e1)). % 13.17/4.58 tff(c_932, plain, (select(store(store(store(a1, n13, e13), n1, e1), n19, e19), n1)!=e5)). % 13.17/4.58 tff(c_905, plain, (select(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1)!=e5)). % 13.17/4.58 tff(c_911, plain, (select(store(store(store(store(a1, n13, e13), n1, e1), n19, e19), n4, e4), n1)!=e3)). % 13.17/4.58 tff(c_906, plain, (e5!=e2)). % 13.17/4.58 tff(c_832, plain, (select(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n4, e4), n1)=e3)). % 13.17/4.58 tff(c_901, plain, (e5!=e3)). % 13.17/4.58 tff(c_831, plain, (n5=n1)). % 13.17/4.58 tff(c_454, plain, (select(store(store(store(a1, n13, e13), n1, e1), n19, e19), n1)!=e3)). % 13.17/4.58 tff(c_455, plain, (e3!=e1)). % 13.17/4.58 tff(c_453, plain, (e3!=e2)). % 13.17/4.58 tff(c_436, plain, (n3=n1)). % 13.17/4.58 tff(c_376, plain, (select(a1, n1)!=e2)). % 13.17/4.58 tff(c_372, plain, (select(store(a1, n13, e13), n1)!=e2)). % 13.17/4.58 tff(c_359, plain, (e2!=e1)). % 13.17/4.58 tff(c_352, plain, (n2=n1)). % 13.17/4.58 tff(c_336, plain, (select(store(a1, n13, e13), n1)!=e1)). % 13.17/4.58 tff(c_335, plain, (select(a1, n1)!=e1)). % 13.17/4.58 tff(c_4, plain, (![A_6, I_4, E_7, J_5]: (select(store(A_6, I_4, E_7), J_5)=select(A_6, J_5) | J_5=I_4))). % 13.17/4.58 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 13.17/4.58 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.17/4.58 %------------------------------------------------------------------------------