%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV504-1.050 : 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 : n011.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 61.27s 17.73s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWV504-1.050 : 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.09/0.29 % Computer : n011.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Wed Apr 9 03:39:03 EDT 2025 % 0.09/0.29 % CPUTime : % 61.27/17.72 % 61.27/17.73 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.27/17.73 % 61.27/17.73 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.27/17.74 %$ store > sk > select > #nlpp > n9 > n8 > n7 > n6 > n50 > n5 > n49 > n48 > n47 > n46 > n45 > n44 > n43 > n42 > n41 > n40 > n4 > n39 > n38 > n37 > n36 > n35 > n34 > n33 > n32 > n31 > 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 > e50 > e5 > e49 > e48 > e47 > e46 > e45 > e44 > e43 > e42 > e41 > e40 > e4 > e39 > e38 > e37 > e36 > e35 > e34 > e33 > e32 > e31 > 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 % 61.27/17.74 % 61.27/17.74 %Foreground sorts: % 61.27/17.74 % 61.27/17.74 % 61.27/17.74 %Background operators: % 61.27/17.74 % 61.27/17.74 % 61.27/17.74 %Foreground operators: % 61.27/17.74 tff(e29, type, e29: $i). % 61.27/17.74 tff(a1, type, a1: $i). % 61.27/17.74 tff(e43, type, e43: $i). % 61.27/17.74 tff(n22, type, n22: $i). % 61.27/17.74 tff(n27, type, n27: $i). % 61.27/17.74 tff(n16, type, n16: $i). % 61.27/17.74 tff(n12, type, n12: $i). % 61.27/17.74 tff(e1, type, e1: $i). % 61.27/17.74 tff(e8, type, e8: $i). % 61.27/17.74 tff(e21, type, e21: $i). % 61.27/17.74 tff(n24, type, n24: $i). % 61.27/17.74 tff(e15, type, e15: $i). % 61.27/17.74 tff(n42, type, n42: $i). % 61.27/17.74 tff(e33, type, e33: $i). % 61.27/17.74 tff(n35, type, n35: $i). % 61.27/17.74 tff(e50, type, e50: $i). % 61.27/17.74 tff(e40, type, e40: $i). % 61.27/17.74 tff(e18, type, e18: $i). % 61.27/17.74 tff(e38, type, e38: $i). % 61.27/17.74 tff(e24, type, e24: $i). % 61.27/17.74 tff(e31, type, e31: $i). % 61.27/17.74 tff(n33, type, n33: $i). % 61.27/17.74 tff(n36, type, n36: $i). % 61.27/17.74 tff(e39, type, e39: $i). % 61.27/17.74 tff(e48, type, e48: $i). % 61.27/17.74 tff(store, type, store: ($i * $i * $i) > $i). % 61.27/17.74 tff(n23, type, n23: $i). % 61.27/17.74 tff(n8, type, n8: $i). % 61.27/17.74 tff(e20, type, e20: $i). % 61.27/17.74 tff(e41, type, e41: $i). % 61.27/17.74 tff(e19, type, e19: $i). % 61.27/17.74 tff(e16, type, e16: $i). % 61.27/17.74 tff(n30, type, n30: $i). % 61.27/17.74 tff(e35, type, e35: $i). % 61.27/17.74 tff(e2, type, e2: $i). % 61.27/17.74 tff(n28, type, n28: $i). % 61.27/17.74 tff(n9, type, n9: $i). % 61.27/17.74 tff(e42, type, e42: $i). % 61.27/17.74 tff(e37, type, e37: $i). % 61.27/17.74 tff(e13, type, e13: $i). % 61.27/17.74 tff(n3, type, n3: $i). % 61.27/17.74 tff(e32, type, e32: $i). % 61.27/17.74 tff(e22, type, e22: $i). % 61.27/17.74 tff(n46, type, n46: $i). % 61.27/17.74 tff(n48, type, n48: $i). % 61.27/17.74 tff(n39, type, n39: $i). % 61.27/17.74 tff(e34, type, e34: $i). % 61.27/17.74 tff(n1, type, n1: $i). % 61.27/17.74 tff(n29, type, n29: $i). % 61.27/17.74 tff(e9, type, e9: $i). % 61.27/17.74 tff(n37, type, n37: $i). % 61.27/17.74 tff(n44, type, n44: $i). % 61.27/17.74 tff(n50, type, n50: $i). % 61.27/17.74 tff(n7, type, n7: $i). % 61.27/17.74 tff(e25, type, e25: $i). % 61.27/17.74 tff(e26, type, e26: $i). % 61.27/17.74 tff(n6, type, n6: $i). % 61.27/17.74 tff(e17, type, e17: $i). % 61.27/17.74 tff(n26, type, n26: $i). % 61.27/17.74 tff(e27, type, e27: $i). % 61.27/17.74 tff(e10, type, e10: $i). % 61.27/17.74 tff(e7, type, e7: $i). % 61.27/17.74 tff(n13, type, n13: $i). % 61.27/17.74 tff(sk, type, sk: ($i * $i) > $i). % 61.27/17.74 tff(e36, type, e36: $i). % 61.27/17.74 tff(n4, type, n4: $i). % 61.27/17.74 tff(n10, type, n10: $i). % 61.27/17.74 tff(n14, type, n14: $i). % 61.27/17.74 tff(e45, type, e45: $i). % 61.27/17.74 tff(n15, type, n15: $i). % 61.27/17.74 tff(n17, type, n17: $i). % 61.27/17.74 tff(n40, type, n40: $i). % 61.27/17.74 tff(e30, type, e30: $i). % 61.27/17.74 tff(select, type, select: ($i * $i) > $i). % 61.27/17.74 tff(e49, type, e49: $i). % 61.27/17.74 tff(n31, type, n31: $i). % 61.27/17.74 tff(e47, type, e47: $i). % 61.27/17.74 tff(n49, type, n49: $i). % 61.27/17.74 tff(n47, type, n47: $i). % 61.27/17.74 tff(n32, type, n32: $i). % 61.27/17.74 tff(n20, type, n20: $i). % 61.27/17.74 tff(e23, type, e23: $i). % 61.27/17.74 tff(n18, type, n18: $i). % 61.27/17.74 tff(n38, type, n38: $i). % 61.27/17.74 tff(e14, type, e14: $i). % 61.27/17.74 tff(n11, type, n11: $i). % 61.27/17.74 tff(e12, type, e12: $i). % 61.27/17.74 tff(e4, type, e4: $i). % 61.27/17.74 tff(n45, type, n45: $i). % 61.27/17.74 tff(n34, type, n34: $i). % 61.27/17.74 tff(e6, type, e6: $i). % 61.27/17.74 tff(e46, type, e46: $i). % 61.27/17.74 tff(n19, type, n19: $i). % 61.27/17.74 tff(n2, type, n2: $i). % 61.27/17.74 tff(e11, type, e11: $i). % 61.27/17.74 tff(e28, type, e28: $i). % 61.27/17.74 tff(n5, type, n5: $i). % 61.27/17.74 tff(e44, type, e44: $i). % 61.27/17.74 tff(e3, type, e3: $i). % 61.27/17.74 tff(n43, type, n43: $i). % 61.27/17.74 tff(n25, type, n25: $i). % 61.27/17.74 tff(e5, type, e5: $i). % 61.27/17.74 tff(n21, type, n21: $i). % 61.27/17.74 tff(n41, type, n41: $i). % 61.27/17.74 % 61.27/17.74 %Saturated clause set: % 61.27/17.74 tff(c_10822, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n21, e21), n31, e31), n1, e1), n16)!=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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n49, e49), n1, e1), n16))). % 61.27/17.74 tff(c_10817, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n49, e49), 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n21, e21), n31, e31), n1, e1))=n16)). % 61.27/17.74 tff(c_10813, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n49, e49), n1, e1), n16)!=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(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n21, e21), n31, e31), n16))). % 61.27/17.74 tff(c_10809, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n21, e21), n31, e31), n16)!=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(store(store(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n49, e49), n16))). % 61.27/17.74 tff(c_10805, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n49, e49), n16)!=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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n21, e21), n16))). % 61.27/17.74 tff(c_10801, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n21, e21), n16)!=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(store(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n16))). % 61.27/17.74 tff(c_10796, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n48, e48), n16)!=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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n16))). % 61.27/17.74 tff(c_10791, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n16)!=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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n16))). % 61.27/17.74 tff(c_10785, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n24, e24), n16)!=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(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n47, e47), n16))). % 61.27/17.74 tff(c_10780, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n16)!=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(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16))). % 61.27/17.74 tff(c_10775, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16)!=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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n16))). % 61.27/17.74 tff(c_10771, 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(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n16)!=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(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16))). % 61.27/17.74 tff(c_10766, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16)!=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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n16))). % 61.27/17.74 tff(c_10762, 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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16))). % 61.27/17.74 tff(c_10758, 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(store(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16))). % 61.27/17.75 tff(c_10754, 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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n16))). % 61.27/17.75 tff(c_10750, 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(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16))). % 61.27/17.75 tff(c_10709, 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(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n16)!=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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n16))). % 61.27/17.75 tff(c_10742, 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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n16))). % 61.27/17.75 tff(c_10738, 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(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16))). % 61.27/17.75 tff(c_10734, 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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n16))). % 61.27/17.75 tff(c_10730, 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(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16))). % 61.27/17.75 tff(c_10726, 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(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n16))). % 61.27/17.75 tff(c_10722, 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(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16))). % 61.27/17.75 tff(c_10718, 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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n16))). % 61.27/17.75 tff(c_10714, 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(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16))). % 61.27/17.75 tff(c_10710, 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(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n16))). % 61.27/17.75 tff(c_10705, 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(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16))). % 61.27/17.75 tff(c_10701, 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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16)!=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, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n16))). % 61.27/17.75 tff(c_10696, 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(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16))). % 61.27/17.75 tff(c_10692, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16))). % 61.27/17.75 tff(c_10687, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16)!=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, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16))). % 61.27/17.75 tff(c_10683, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16))). % 61.27/17.75 tff(c_10679, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16)!=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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16))). % 61.27/17.75 tff(c_10675, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n16))). % 61.27/17.75 tff(c_10671, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n16)!=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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16))). % 61.27/17.75 tff(c_10667, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n4, e4), n16)!=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(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n16, e28), n29, e29), n16, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n16, e39), n16, e40), n16, e41), n42, e42), n16, e43), n44, e44), n16, e45), n46, e46), n16))). % 61.27/17.75 tff(c_10663, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n16))). % 61.27/17.75 tff(c_10659, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n25, e25), n16)!=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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16))). % 61.27/17.75 tff(c_10655, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n16))). % 61.27/17.75 tff(c_10651, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n24, e24), n16)!=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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16))). % 61.27/17.76 tff(c_10647, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n16))). % 61.27/17.76 tff(c_10642, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16, e22), n23, e23), n16)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16))). % 61.27/17.76 tff(c_10636, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n16)!=e43)). % 61.27/17.76 tff(c_10594, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n16)!=e45)). % 61.27/17.76 tff(c_10629, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n16)!=e45)). % 61.27/17.76 tff(c_10624, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16)!=e9)). % 61.27/17.76 tff(c_10620, 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(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n16)!=e43)). % 61.27/17.76 tff(c_10616, 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(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n16)!=e45)). % 61.27/17.76 tff(c_10611, 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), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16, e19), n16, e20), n21, e21), n16)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16))). % 61.27/17.76 tff(c_10607, 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(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n16)!=e41)). % 61.27/17.76 tff(c_10603, 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(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n16)!=e43)). % 61.27/17.76 tff(c_10599, 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(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n16)!=e45)). % 61.27/17.76 tff(c_10595, 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(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n16)!=e41)). % 61.27/17.76 tff(c_10590, 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(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n16)!=e40)). % 61.27/17.76 tff(c_10586, 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(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n16)!=e43)). % 61.27/17.76 tff(c_10582, 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(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n16)!=e45)). % 61.27/17.76 tff(c_10578, 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(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n16)!=e40)). % 61.27/17.76 tff(c_10574, 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(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n16)!=e39)). % 61.27/17.76 tff(c_10570, 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(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n16)!=e41)). % 61.27/17.76 tff(c_10566, 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(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n16)!=e43)). % 61.27/17.76 tff(c_10562, 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(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n16)!=e45)). % 61.27/17.76 tff(c_10558, 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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n16)!=e39)). % 61.27/17.76 tff(c_10554, 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(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n48, e48), n29, e29), n3, e3), n37, e37), n12, e12), n5, e5), n32, e32), n16)!=e45)). % 61.27/17.76 tff(c_10550, 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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n16)!=e41)). % 61.27/17.76 tff(c_10546, 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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n16)!=e45)). % 61.27/17.76 tff(c_10542, 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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n16)!=e43)). % 61.27/17.76 tff(c_10538, 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(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n10, e10), n16)!=e40)). % 61.27/17.76 tff(c_10534, 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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16)!=e41)). % 61.27/17.76 tff(c_10530, 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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16)!=e45)). % 61.27/17.76 tff(c_10526, 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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16)!=e43)). % 61.27/17.76 tff(c_10522, 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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16)!=e39)). % 61.27/17.76 tff(c_10518, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16))). % 61.27/17.76 tff(c_10514, 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(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n2, e2), n16)!=e40)). % 61.27/17.76 tff(c_10510, 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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16)!=e41)). % 61.27/17.76 tff(c_10506, 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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16)!=e45)). % 61.27/17.76 tff(c_10502, 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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16)!=e43)). % 61.27/17.76 tff(c_10498, 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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16)!=e39)). % 61.27/17.76 tff(c_10494, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n16)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16))). % 61.27/17.76 tff(c_10490, 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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16)!=e41)). % 61.27/17.76 tff(c_10486, 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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16)!=e45)). % 61.27/17.77 tff(c_10482, 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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16)!=e43)). % 61.27/17.77 tff(c_10478, 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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16)!=e39)). % 61.27/17.77 tff(c_10474, 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(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n16)!=e40)). % 61.27/17.77 tff(c_10470, 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(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n16)!=e40)). % 61.27/17.77 tff(c_10466, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n16))). % 61.27/17.77 tff(c_10462, 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(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16)!=e41)). % 61.27/17.77 tff(c_10458, 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(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16)!=e45)). % 61.27/17.77 tff(c_10454, 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(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16)!=e43)). % 61.27/17.77 tff(c_10450, 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(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16)!=e39)). % 61.27/17.77 tff(c_10445, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n16)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16))). % 61.27/17.77 tff(c_10441, 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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16)!=e41)). % 61.27/17.77 tff(c_10437, 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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16)!=e45)). % 61.27/17.77 tff(c_10433, 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(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n16)!=e40)). % 61.27/17.77 tff(c_10429, 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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16)!=e43)). % 61.27/17.77 tff(c_10425, 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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16)!=e39)). % 61.27/17.77 tff(c_10421, 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(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n16)!=e40)). % 61.27/17.77 tff(c_10417, 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(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16)!=e41)). % 61.27/17.77 tff(c_10413, 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(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16)!=e45)). % 61.27/17.77 tff(c_10409, 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(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16)!=e43)). % 61.27/17.77 tff(c_10405, 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(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16)!=e39)). % 61.27/17.77 tff(c_10401, 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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16)!=e41)). % 61.27/17.77 tff(c_10397, 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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16)!=e45)). % 61.27/17.77 tff(c_10393, 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(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n23, e23), n16)!=e40)). % 61.27/17.77 tff(c_10389, 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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16)!=e43)). % 61.27/17.77 tff(c_10385, 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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16)!=e39)). % 61.27/17.77 tff(c_10381, 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(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n38, e38), n16)!=e40)). % 61.27/17.77 tff(c_10377, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16))). % 61.27/17.77 tff(c_10373, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16)!=e41)). % 61.27/17.77 tff(c_10369, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16)!=e45)). % 61.27/17.77 tff(c_10365, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16)!=e43)). % 61.27/17.77 tff(c_10361, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16)!=e39)). % 61.27/17.77 tff(c_10357, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16)!=e30)). % 61.27/17.77 tff(c_10353, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n44, e44), n16)!=e40)). % 61.27/17.77 tff(c_10349, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16))). % 61.27/17.77 tff(c_10345, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=e41)). % 61.27/17.77 tff(c_10341, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=e45)). % 61.27/17.77 tff(c_10337, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=e43)). % 61.27/17.77 tff(c_10333, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=e30)). % 61.27/17.77 tff(c_10329, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=e39)). % 61.27/17.77 tff(c_10325, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n16))). % 61.27/17.77 tff(c_10321, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e28)). % 61.27/17.77 tff(c_10317, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e41)). % 61.27/17.77 tff(c_10313, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n36, e36), n16)!=e40)). % 61.27/17.77 tff(c_10309, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e45)). % 61.27/17.77 tff(c_10305, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e43)). % 61.27/17.77 tff(c_10301, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e30)). % 61.27/17.77 tff(c_10297, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e39)). % 61.27/17.77 tff(c_10293, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n14, e14), n16)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16))). % 61.27/17.77 tff(c_10289, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e28)). % 61.27/17.77 tff(c_10285, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e41)). % 61.27/17.77 tff(c_10281, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e30)). % 61.27/17.77 tff(c_10277, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e45)). % 61.27/17.77 tff(c_10273, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n11, e11), n16)!=e40)). % 61.27/17.77 tff(c_10269, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e43)). % 61.27/17.78 tff(c_10265, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e39)). % 61.27/17.78 tff(c_10260, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n16))). % 61.27/17.78 tff(c_10256, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e41)). % 61.27/17.78 tff(c_10252, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e30)). % 61.27/17.78 tff(c_10248, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e45)). % 61.27/17.78 tff(c_10244, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e43)). % 61.27/17.78 tff(c_10240, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e28)). % 61.27/17.78 tff(c_10236, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e39)). % 61.27/17.78 tff(c_10232, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n16)!=e40)). % 61.27/17.78 tff(c_10228, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n16)!=e40)). % 61.27/17.78 tff(c_10224, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n13, e13), n16)!=e8)). % 61.27/17.78 tff(c_10220, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e41)). % 61.27/17.78 tff(c_10029, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e41)). % 61.27/17.78 tff(c_10030, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e30)). % 61.27/17.78 tff(c_10031, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e45)). % 61.27/17.78 tff(c_10032, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e43)). % 61.27/17.78 tff(c_10204, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e30)). % 61.27/17.78 tff(c_10033, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e28)). % 61.27/17.78 tff(c_10034, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e39)). % 61.27/17.78 tff(c_10036, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n16)!=e40)). % 61.27/17.78 tff(c_10035, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e41)). % 61.27/17.78 tff(c_10037, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e30)). % 61.27/17.78 tff(c_10038, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e45)). % 61.27/17.78 tff(c_10039, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e43)). % 61.27/17.78 tff(c_10040, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e28)). % 61.27/17.78 tff(c_10175, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e45)). % 61.27/17.78 tff(c_10041, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e39)). % 61.27/17.78 tff(c_10046, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n16)!=e40)). % 61.27/17.78 tff(c_10042, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e41)). % 61.27/17.78 tff(c_10043, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e30)). % 61.27/17.78 tff(c_10044, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e45)). % 61.27/17.78 tff(c_10045, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e43)). % 61.27/17.78 tff(c_10047, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e28)). % 61.27/17.78 tff(c_10048, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e22)). % 61.27/17.78 tff(c_10140, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e43)). % 61.27/17.78 tff(c_10049, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e39)). % 61.27/17.78 tff(c_10056, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n16)!=e40)). % 61.54/17.78 tff(c_10059, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n16)!=e16)). % 61.54/17.78 tff(c_10028, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n12, e12), n16)!=e8)). % 61.54/17.78 tff(c_10061, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n16)!=e40)). % 61.54/17.78 tff(c_10060, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n16)!=e16)). % 61.54/17.78 tff(c_10027, plain, (select(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), n16, e8), n16, e9), n10, e10), n11, e11), n16)!=e8)). % 61.54/17.78 tff(c_10062, plain, (select(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), n16, e8), n16, e9), n10, e10), n16)!=e40)). % 61.54/17.78 tff(c_10108, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e28)). % 61.54/17.78 tff(c_10063, plain, (select(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), n16, e8), n16, e9), n10, e10), n16)!=e20)). % 61.54/17.78 tff(c_10064, plain, (select(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), n16, e8), n16, e9), n10, e10), n16)!=e16)). % 61.54/17.78 tff(c_10026, plain, (select(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), n16, e8), n16, e9), n10, e10), n16)!=e8)). % 61.54/17.78 tff(c_10078, plain, (e9!=e20)). % 61.54/17.78 tff(c_10070, plain, (e9!=e41)). % 61.54/17.78 tff(c_10071, plain, (e9!=e30)). % 61.54/17.78 tff(c_10072, plain, (e9!=e45)). % 61.54/17.78 tff(c_10091, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e39)). % 61.54/17.78 tff(c_10073, plain, (e9!=e43)). % 61.54/17.78 tff(c_10075, plain, (e9!=e22)). % 61.54/17.78 tff(c_10074, plain, (e9!=e28)). % 61.54/17.78 tff(c_10076, plain, (e9!=e39)). % 61.54/17.78 tff(c_10080, plain, (e9!=e40)). % 61.54/17.78 tff(c_10081, plain, (e9!=e16)). % 61.54/17.78 tff(c_10069, plain, (e9!=e8)). % 61.54/17.78 tff(c_10086, 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, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16, e9), n17, e17), n42, e42), n47, e47), n18, e18), n16)!=e40)). % 61.54/17.78 tff(c_10024, plain, (n9=n16)). % 61.55/17.78 tff(c_9887, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e20)). % 61.55/17.78 tff(c_9883, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e41)). % 61.55/17.78 tff(c_9879, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e30)). % 61.55/17.78 tff(c_9875, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e45)). % 61.55/17.78 tff(c_9871, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e43)). % 61.55/17.78 tff(c_9867, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e28)). % 61.55/17.78 tff(c_9863, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e22)). % 61.55/17.78 tff(c_9859, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e39)). % 61.55/17.78 tff(c_9851, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n33, e33), n16)!=e40)). % 61.55/17.78 tff(c_9847, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e20)). % 61.55/17.78 tff(c_9843, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e45)). % 61.55/17.78 tff(c_9839, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e43)). % 61.55/17.78 tff(c_9835, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e28)). % 61.55/17.78 tff(c_9831, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e19)). % 61.55/17.78 tff(c_9827, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e22)). % 61.55/17.78 tff(c_9823, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e39)). % 61.55/17.78 tff(c_9819, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e41)). % 61.55/17.78 tff(c_9815, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e30)). % 61.55/17.78 tff(c_9811, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e41)). % 61.55/17.79 tff(c_9807, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e30)). % 61.55/17.79 tff(c_9803, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e45)). % 61.55/17.79 tff(c_9799, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e43)). % 61.55/17.79 tff(c_9795, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e28)). % 61.55/17.79 tff(c_9791, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e19)). % 61.55/17.79 tff(c_9787, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e22)). % 61.55/17.79 tff(c_9783, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e39)). % 61.55/17.79 tff(c_9779, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e20)). % 61.55/17.79 tff(c_9775, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n7, e7), n16)!=e40)). % 61.55/17.79 tff(c_9771, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e41)). % 61.55/17.79 tff(c_9767, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e30)). % 61.55/17.79 tff(c_9763, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e45)). % 61.55/17.79 tff(c_9759, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e43)). % 61.55/17.79 tff(c_9755, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e28)). % 61.55/17.79 tff(c_9751, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e19)). % 61.55/17.79 tff(c_9747, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e22)). % 61.55/17.79 tff(c_9743, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e39)). % 61.55/17.79 tff(c_9739, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e20)). % 61.55/17.79 tff(c_9735, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n15, e15), n16)!=e40)). % 61.55/17.79 tff(c_9731, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n27, e27), n16)!=e40)). % 61.55/17.79 tff(c_9456, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e40)). % 61.55/17.79 tff(c_9724, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e16)). % 61.55/17.79 tff(c_9720, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e41)). % 61.55/17.79 tff(c_9449, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e16)). % 61.55/17.79 tff(c_9450, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e41)). % 61.55/17.79 tff(c_9710, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e30)). % 61.55/17.79 tff(c_9451, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e30)). % 61.55/17.79 tff(c_9452, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e45)). % 61.55/17.79 tff(c_9453, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e43)). % 61.55/17.79 tff(c_9454, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e28)). % 61.55/17.79 tff(c_9455, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e19)). % 61.55/17.79 tff(c_9457, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e22)). % 61.55/17.79 tff(c_9458, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e39)). % 61.55/17.79 tff(c_9459, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e20)). % 61.55/17.79 tff(c_9681, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e45)). % 61.55/17.79 tff(c_9465, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n16)!=e40)). % 61.55/17.79 tff(c_9460, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e41)). % 61.55/17.79 tff(c_9461, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e30)). % 61.55/17.79 tff(c_9462, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e45)). % 61.55/17.79 tff(c_9463, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e43)). % 61.55/17.79 tff(c_9464, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e28)). % 61.55/17.79 tff(c_9466, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e19)). % 61.55/17.79 tff(c_9467, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e22)). % 61.55/17.79 tff(c_9652, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e43)). % 61.55/17.79 tff(c_9468, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e39)). % 61.55/17.79 tff(c_9469, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e20)). % 61.55/17.79 tff(c_9474, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e40)). % 61.55/17.79 tff(c_9448, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n16)!=e16)). % 61.55/17.79 tff(c_9470, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e41)). % 61.55/17.79 tff(c_9471, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e30)). % 61.55/17.79 tff(c_9472, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e45)). % 61.55/17.79 tff(c_9473, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e43)). % 61.55/17.79 tff(c_9619, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e28)). % 61.55/17.79 tff(c_9475, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e28)). % 61.55/17.79 tff(c_9476, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e19)). % 61.55/17.79 tff(c_9477, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e22)). % 61.55/17.79 tff(c_9478, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e39)). % 61.55/17.79 tff(c_9479, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e20)). % 61.55/17.79 tff(c_9483, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e40)). % 61.55/17.79 tff(c_9447, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n16)!=e16)). % 61.55/17.79 tff(c_9583, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e19)). % 61.55/17.79 tff(c_9551, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e22)). % 61.55/17.79 tff(c_9518, plain, (e8!=e41)). % 61.55/17.79 tff(c_9519, plain, (e8!=e30)). % 61.55/17.79 tff(c_9520, plain, (e8!=e45)). % 61.55/17.79 tff(c_9521, plain, (e8!=e43)). % 61.55/17.79 tff(c_9522, plain, (e8!=e28)). % 61.55/17.79 tff(c_9542, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e39)). % 61.55/17.79 tff(c_9523, plain, (e8!=e19)). % 61.55/17.79 tff(c_9524, plain, (e8!=e22)). % 61.55/17.79 tff(c_9525, plain, (e8!=e39)). % 61.55/17.79 tff(c_9531, plain, (e8!=e40)). % 61.55/17.79 tff(c_9532, plain, (e8!=e20)). % 61.55/17.79 tff(c_9537, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e41), n16, e30), n16, e45), n16, e43), n16, e28), n16, e19), n16, e22), n16, e39), n16, e20), n16, e40), n16, e16), n16, e8), n49, e49), n14, e14), n13, e13), n6, e6), n16)!=e20)). % 61.55/17.79 tff(c_9517, plain, (e8!=e16)). % 61.55/17.79 tff(c_9445, plain, (n8=n16)). % 61.55/17.79 tff(c_9285, plain, (select(a1, n16)!=e16)). % 61.55/17.79 tff(c_9279, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e16)). % 61.55/17.79 tff(c_9275, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e16)). % 61.55/17.79 tff(c_9271, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e16)). % 61.55/17.79 tff(c_9267, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e16)). % 61.55/17.79 tff(c_9263, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e16)). % 61.55/17.79 tff(c_9258, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16)!=e16)). % 61.55/17.79 tff(c_8915, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16)!=e22)). % 61.55/17.79 tff(c_8917, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16)!=e19)). % 61.55/17.79 tff(c_8894, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16)!=e20)). % 61.55/17.79 tff(c_8838, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16)!=e40)). % 61.55/17.79 tff(c_8918, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e28)). % 61.55/17.79 tff(c_8905, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n7, e7), n16)!=e39)). % 61.55/17.79 tff(c_8924, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e19)). % 61.55/17.79 tff(c_8904, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e39)). % 61.55/17.79 tff(c_8914, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e22)). % 61.55/17.79 tff(c_8893, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e20)). % 61.55/17.79 tff(c_8837, plain, (select(store(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n6, e6), n16)!=e40)). % 61.55/17.79 tff(c_8925, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e28)). % 61.55/17.79 tff(c_8926, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e43)). % 61.55/17.79 tff(c_8835, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e40)). % 61.55/17.79 tff(c_8892, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e20)). % 61.55/17.79 tff(c_8903, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e39)). % 61.55/17.79 tff(c_8913, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e22)). % 61.55/17.79 tff(c_8923, plain, (select(store(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n5, e5), n16)!=e19)). % 61.55/17.79 tff(c_8927, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e43)). % 61.55/17.79 tff(c_8928, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e45)). % 61.55/17.79 tff(c_8929, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e28)). % 61.55/17.79 tff(c_8891, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e20)). % 61.55/17.79 tff(c_8834, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e40)). % 61.55/17.79 tff(c_8902, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e39)). % 61.55/17.79 tff(c_8912, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e22)). % 61.55/17.79 tff(c_8922, plain, (select(store(store(store(store(a1, n1, e1), n2, e2), n3, e3), n4, e4), n16)!=e19)). % 61.55/17.79 tff(c_8930, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e45)). % 61.55/17.79 tff(c_8931, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e30)). % 61.55/17.79 tff(c_8932, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e43)). % 61.55/17.79 tff(c_8933, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e28)). % 61.55/17.79 tff(c_8901, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e39)). % 61.55/17.79 tff(c_8890, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e20)). % 61.55/17.79 tff(c_8911, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e22)). % 61.55/17.80 tff(c_8921, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e19)). % 61.55/17.80 tff(c_8833, plain, (select(store(store(store(a1, n1, e1), n2, e2), n3, e3), n16)!=e40)). % 61.55/17.80 tff(c_8935, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e30)). % 61.55/17.80 tff(c_8934, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e41)). % 61.55/17.80 tff(c_8937, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e43)). % 61.55/17.80 tff(c_8936, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e45)). % 61.55/17.80 tff(c_8938, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e28)). % 61.55/17.80 tff(c_8900, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e39)). % 61.55/17.80 tff(c_8910, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e22)). % 61.55/17.80 tff(c_8889, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e20)). % 61.55/17.80 tff(c_8832, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e40)). % 61.55/17.80 tff(c_8920, plain, (select(store(store(a1, n1, e1), n2, e2), n16)!=e19)). % 61.55/17.80 tff(c_8939, plain, (select(store(a1, n1, e1), n16)=select(a1, n16))). % 61.55/17.80 tff(c_8940, plain, (select(a1, n16)!=e41)). % 61.55/17.80 tff(c_8941, plain, (select(a1, n16)!=e45)). % 61.55/17.80 tff(c_8942, plain, (select(a1, n16)!=e43)). % 61.55/17.80 tff(c_8943, plain, (select(a1, n16)!=e30)). % 61.55/17.80 tff(c_8944, plain, (select(a1, n16)!=e28)). % 61.55/17.80 tff(c_8909, plain, (select(a1, n16)!=e22)). % 61.55/17.80 tff(c_8899, plain, (select(a1, n16)!=e39)). % 61.55/17.80 tff(c_8888, plain, (select(a1, n16)!=e20)). % 61.55/17.80 tff(c_8831, plain, (select(a1, n16)!=e40)). % 61.55/17.80 tff(c_8919, plain, (select(a1, n16)!=e19)). % 61.55/17.80 tff(c_8955, plain, (e41!=e16)). % 61.55/17.80 tff(c_8956, plain, (e30!=e16)). % 61.55/17.80 tff(c_8957, plain, (e45!=e16)). % 61.55/17.80 tff(c_8958, plain, (e43!=e16)). % 61.55/17.80 tff(c_8959, plain, (e28!=e16)). % 61.55/17.80 tff(c_8960, plain, (e19!=e16)). % 61.55/17.80 tff(c_8961, plain, (e22!=e16)). % 61.55/17.80 tff(c_8945, plain, (n45=n16)). % 61.55/17.80 tff(c_8947, plain, (n43=n16)). % 61.55/17.80 tff(c_8946, plain, (n41=n16)). % 61.55/17.80 tff(c_8962, plain, (e39!=e16)). % 61.55/17.80 tff(c_8948, plain, (n30=n16)). % 61.55/17.80 tff(c_8963, plain, (e20!=e16)). % 61.55/17.80 tff(c_8897, plain, (n20=n16)). % 61.55/17.80 tff(c_8886, plain, (n40=n16)). % 61.55/17.80 tff(c_8907, plain, (n39=n16)). % 61.55/17.80 tff(c_8916, plain, (n22=n16)). % 61.55/17.80 tff(c_8949, plain, (n28=n16)). % 61.55/17.80 tff(c_8950, plain, (e40!=e16)). % 61.55/17.80 tff(c_8595, plain, (n19=n16)). % 61.55/17.80 tff(c_7482, plain, (e41!=e40)). % 61.55/17.80 tff(c_7483, plain, (e40!=e30)). % 61.55/17.80 tff(c_7484, plain, (e45!=e40)). % 61.55/17.80 tff(c_7485, plain, (e43!=e40)). % 61.55/17.80 tff(c_7486, plain, (e40!=e28)). % 61.55/17.80 tff(c_7487, plain, (e40!=e19)). % 61.55/17.80 tff(c_7488, plain, (e40!=e22)). % 61.55/17.80 tff(c_7489, plain, (e40!=e39)). % 61.55/17.80 tff(c_7481, plain, (e40!=e20)). % 61.55/17.80 tff(c_7001, plain, (e41!=e20)). % 61.55/17.80 tff(c_7002, plain, (e30!=e20)). % 61.55/17.80 tff(c_7003, plain, (e45!=e20)). % 61.55/17.80 tff(c_7004, plain, (e43!=e20)). % 61.55/17.80 tff(c_7005, plain, (e28!=e20)). % 61.55/17.80 tff(c_7006, plain, (e20!=e19)). % 61.55/17.80 tff(c_7007, plain, (e22!=e20)). % 61.55/17.80 tff(c_6996, plain, (e39!=e20)). % 61.55/17.80 tff(c_5760, plain, (e41!=e39)). % 61.55/17.80 tff(c_5761, plain, (e39!=e30)). % 61.63/17.80 tff(c_5762, plain, (e45!=e39)). % 61.63/17.80 tff(c_5763, plain, (e43!=e39)). % 61.63/17.80 tff(c_5764, plain, (e39!=e28)). % 61.63/17.80 tff(c_5765, plain, (e39!=e19)). % 61.63/17.80 tff(c_5757, plain, (e39!=e22)). % 61.63/17.80 tff(c_4684, plain, (e41!=e22)). % 61.63/17.80 tff(c_4685, plain, (e30!=e22)). % 61.63/17.80 tff(c_4686, plain, (e45!=e22)). % 61.63/17.80 tff(c_4687, plain, (e43!=e22)). % 61.63/17.80 tff(c_4688, plain, (e28!=e22)). % 61.63/17.80 tff(c_4681, plain, (e22!=e19)). % 61.63/17.80 tff(c_4097, plain, (e41!=e19)). % 61.63/17.80 tff(c_4098, plain, (e30!=e19)). % 61.63/17.80 tff(c_4099, plain, (e45!=e19)). % 61.63/17.80 tff(c_4100, plain, (e43!=e19)). % 61.63/17.80 tff(c_4094, plain, (e28!=e19)). % 61.63/17.80 tff(c_3402, plain, (e41!=e28)). % 61.63/17.80 tff(c_3403, plain, (e30!=e28)). % 61.63/17.80 tff(c_3404, plain, (e45!=e28)). % 61.63/17.80 tff(c_3399, plain, (e43!=e28)). % 61.63/17.80 tff(c_2504, plain, (e43!=e41)). % 61.63/17.80 tff(c_2505, plain, (e43!=e30)). % 61.63/17.80 tff(c_2499, plain, (e45!=e43)). % 61.63/17.80 tff(c_1621, plain, (e45!=e41)). % 61.63/17.80 tff(c_1618, plain, (e45!=e30)). % 61.63/17.80 tff(c_1044, plain, (e41!=e30)). % 61.63/17.80 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))). % 61.63/17.80 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 61.63/17.80 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.63/17.80 %------------------------------------------------------------------------------