%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV503-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 : n005.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 64.74s 16.54s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV503-1.050 : TPTP v9.0.0. Released v4.0.0. % 0.07/0.13 % 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.13/0.34 % Computer : n005.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 03:38:27 EDT 2025 % 0.13/0.34 % CPUTime : % 64.74/16.54 % 64.74/16.54 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 64.74/16.54 % 64.74/16.54 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 64.74/16.55 %$ 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 % 64.74/16.55 % 64.74/16.55 %Foreground sorts: % 64.74/16.55 % 64.74/16.55 % 64.74/16.55 %Background operators: % 64.74/16.55 % 64.74/16.55 % 64.74/16.55 %Foreground operators: % 64.74/16.55 tff(e29, type, e29: $i). % 64.74/16.55 tff(a1, type, a1: $i). % 64.74/16.55 tff(e43, type, e43: $i). % 64.74/16.55 tff(n22, type, n22: $i). % 64.74/16.55 tff(n27, type, n27: $i). % 64.74/16.55 tff(n16, type, n16: $i). % 64.74/16.55 tff(n12, type, n12: $i). % 64.74/16.55 tff(e1, type, e1: $i). % 64.74/16.55 tff(e8, type, e8: $i). % 64.74/16.55 tff(e21, type, e21: $i). % 64.74/16.55 tff(n24, type, n24: $i). % 64.74/16.55 tff(e15, type, e15: $i). % 64.74/16.55 tff(n42, type, n42: $i). % 64.74/16.55 tff(e33, type, e33: $i). % 64.74/16.55 tff(n35, type, n35: $i). % 64.74/16.55 tff(e50, type, e50: $i). % 64.74/16.55 tff(e40, type, e40: $i). % 64.74/16.55 tff(e18, type, e18: $i). % 64.74/16.55 tff(e38, type, e38: $i). % 64.74/16.55 tff(e24, type, e24: $i). % 64.74/16.55 tff(e31, type, e31: $i). % 64.74/16.55 tff(n33, type, n33: $i). % 64.74/16.55 tff(n36, type, n36: $i). % 64.74/16.55 tff(e39, type, e39: $i). % 64.74/16.55 tff(e48, type, e48: $i). % 64.74/16.55 tff(store, type, store: ($i * $i * $i) > $i). % 64.74/16.55 tff(n23, type, n23: $i). % 64.74/16.55 tff(n8, type, n8: $i). % 64.74/16.55 tff(e20, type, e20: $i). % 64.74/16.55 tff(e41, type, e41: $i). % 64.74/16.55 tff(e19, type, e19: $i). % 64.74/16.55 tff(e16, type, e16: $i). % 64.74/16.55 tff(n30, type, n30: $i). % 64.74/16.55 tff(e35, type, e35: $i). % 64.74/16.55 tff(e2, type, e2: $i). % 64.74/16.55 tff(n28, type, n28: $i). % 64.74/16.55 tff(n9, type, n9: $i). % 64.74/16.55 tff(e42, type, e42: $i). % 64.74/16.55 tff(e37, type, e37: $i). % 64.74/16.55 tff(e13, type, e13: $i). % 64.74/16.55 tff(n3, type, n3: $i). % 64.74/16.55 tff(e32, type, e32: $i). % 64.74/16.55 tff(e22, type, e22: $i). % 64.74/16.55 tff(n46, type, n46: $i). % 64.74/16.55 tff(n48, type, n48: $i). % 64.74/16.55 tff(n39, type, n39: $i). % 64.74/16.55 tff(e34, type, e34: $i). % 64.74/16.55 tff(n1, type, n1: $i). % 64.74/16.55 tff(n29, type, n29: $i). % 64.74/16.55 tff(e9, type, e9: $i). % 64.74/16.55 tff(n37, type, n37: $i). % 64.74/16.55 tff(n44, type, n44: $i). % 64.74/16.55 tff(n50, type, n50: $i). % 64.74/16.55 tff(n7, type, n7: $i). % 64.74/16.55 tff(e25, type, e25: $i). % 64.74/16.55 tff(e26, type, e26: $i). % 64.74/16.55 tff(n6, type, n6: $i). % 64.74/16.55 tff(e17, type, e17: $i). % 64.74/16.55 tff(n26, type, n26: $i). % 64.74/16.55 tff(e27, type, e27: $i). % 64.74/16.55 tff(e10, type, e10: $i). % 64.74/16.55 tff(e7, type, e7: $i). % 64.74/16.55 tff(n13, type, n13: $i). % 64.74/16.55 tff(sk, type, sk: ($i * $i) > $i). % 64.74/16.55 tff(e36, type, e36: $i). % 64.74/16.55 tff(n4, type, n4: $i). % 64.74/16.55 tff(n10, type, n10: $i). % 64.74/16.55 tff(n14, type, n14: $i). % 64.74/16.55 tff(e45, type, e45: $i). % 64.74/16.55 tff(n15, type, n15: $i). % 64.74/16.55 tff(n17, type, n17: $i). % 64.74/16.55 tff(n40, type, n40: $i). % 64.74/16.55 tff(e30, type, e30: $i). % 64.74/16.55 tff(select, type, select: ($i * $i) > $i). % 64.74/16.55 tff(e49, type, e49: $i). % 64.74/16.55 tff(n31, type, n31: $i). % 64.74/16.55 tff(e47, type, e47: $i). % 64.74/16.55 tff(n49, type, n49: $i). % 64.74/16.55 tff(n47, type, n47: $i). % 64.74/16.55 tff(n32, type, n32: $i). % 64.74/16.55 tff(n20, type, n20: $i). % 64.74/16.55 tff(e23, type, e23: $i). % 64.74/16.55 tff(n18, type, n18: $i). % 64.74/16.55 tff(n38, type, n38: $i). % 64.74/16.55 tff(e14, type, e14: $i). % 64.74/16.55 tff(n11, type, n11: $i). % 64.74/16.55 tff(e12, type, e12: $i). % 64.74/16.55 tff(e4, type, e4: $i). % 64.74/16.55 tff(n45, type, n45: $i). % 64.74/16.55 tff(n34, type, n34: $i). % 64.74/16.55 tff(e6, type, e6: $i). % 64.74/16.55 tff(e46, type, e46: $i). % 64.74/16.55 tff(n19, type, n19: $i). % 64.74/16.55 tff(n2, type, n2: $i). % 64.74/16.55 tff(e11, type, e11: $i). % 64.74/16.55 tff(e28, type, e28: $i). % 64.74/16.55 tff(n5, type, n5: $i). % 64.74/16.55 tff(e44, type, e44: $i). % 64.74/16.55 tff(e3, type, e3: $i). % 64.74/16.55 tff(n43, type, n43: $i). % 64.74/16.55 tff(n25, type, n25: $i). % 64.74/16.55 tff(e5, type, e5: $i). % 64.74/16.55 tff(n21, type, n21: $i). % 64.74/16.55 tff(n41, type, n41: $i). % 64.74/16.55 % 64.74/16.55 %Saturated clause set: % 64.74/16.55 tff(c_12037, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1))). % 64.74/16.55 tff(c_12046, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n1))). % 64.74/16.55 tff(c_12056, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1))). % 64.74/16.55 tff(c_12065, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n1))). % 64.74/16.55 tff(c_13150, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n1))). % 64.74/16.55 tff(c_12075, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1))). % 64.74/16.56 tff(c_12081, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n1))). % 64.74/16.56 tff(c_12090, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1))). % 64.74/16.56 tff(c_12099, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n1))). % 64.74/16.56 tff(c_12108, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1))). % 64.74/16.56 tff(c_12117, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n1))). % 64.74/16.56 tff(c_12126, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1))). % 64.74/16.56 tff(c_12136, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1))). % 64.74/16.56 tff(c_12145, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1))). % 64.74/16.56 tff(c_12154, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n1))). % 64.74/16.56 tff(c_12163, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1))). % 64.74/16.56 tff(c_12173, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n1))). % 64.74/16.56 tff(c_12182, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1))). % 64.74/16.56 tff(c_12192, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n49, e49), n50, e50), n1)!=e1)). % 64.74/16.56 tff(c_12201, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n1))). % 64.74/16.56 tff(c_12211, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n49, e49), n1)!=e1)). % 64.74/16.56 tff(c_12220, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1))). % 64.74/16.56 tff(c_12229, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n1)!=e1)). % 64.74/16.56 tff(c_12261, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1))). % 64.74/16.56 tff(c_12233, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n1))). % 64.74/16.56 tff(c_13112, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n1)!=e1)). % 64.74/16.56 tff(c_13107, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1))). % 64.74/16.56 tff(c_13102, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n1)!=e1)). % 64.74/16.56 tff(c_13098, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n1))). % 64.74/16.56 tff(c_13094, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n1)!=e1)). % 64.74/16.56 tff(c_13089, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n1)!=e5)). % 64.74/16.56 tff(c_13084, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1))). % 64.74/16.56 tff(c_13080, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n1)!=e4)). % 64.74/16.56 tff(c_13075, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n1)!=e5)). % 64.74/16.56 tff(c_13071, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n1)!=e1)). % 64.74/16.56 tff(c_13064, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n1)!=e1)). % 64.74/16.57 tff(c_13058, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n1)!=e5)). % 64.74/16.57 tff(c_13054, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n1)!=e1)). % 64.74/16.57 tff(c_13049, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n1)!=e5)). % 64.74/16.57 tff(c_13045, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n1)!=e3)). % 64.74/16.57 tff(c_13040, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1))). % 64.74/16.57 tff(c_13036, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n1)!=e1)). % 64.74/16.57 tff(c_13031, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n1)!=e5)). % 64.74/16.57 tff(c_13027, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n1)!=e3)). % 64.74/16.57 tff(c_13023, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n1)!=e12)). % 64.74/16.57 tff(c_13018, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1))). % 64.74/16.57 tff(c_13014, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1)!=e3)). % 64.74/16.57 tff(c_12985, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n1)!=e12)). % 64.74/16.57 tff(c_13006, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1)!=e5)). % 64.74/16.57 tff(c_13002, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1)!=e1)). % 64.74/16.57 tff(c_12998, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1)!=e12)). % 64.74/16.57 tff(c_12994, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1)!=e10)). % 64.74/16.57 tff(c_12990, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1)!=e1)). % 64.74/16.57 tff(c_12986, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1)!=e3)). % 64.74/16.57 tff(c_12980, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1)!=e5)). % 64.74/16.57 tff(c_12976, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1)!=e12)). % 64.74/16.57 tff(c_12972, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e10)). % 64.74/16.57 tff(c_12968, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e2)). % 64.74/16.57 tff(c_12964, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e3)). % 64.74/16.57 tff(c_12959, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e5)). % 64.74/16.57 tff(c_12576, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n1)!=e12)). % 64.74/16.57 tff(c_12952, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e1)). % 64.74/16.57 tff(c_12948, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e12)). % 64.74/16.57 tff(c_12944, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e15)). % 64.74/16.57 tff(c_12940, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e2)). % 64.74/16.57 tff(c_12935, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e5)). % 64.74/16.57 tff(c_12931, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e3)). % 64.74/16.57 tff(c_12927, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e1)). % 64.74/16.57 tff(c_12922, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e10)). % 64.74/16.57 tff(c_12021, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e4)). % 64.74/16.57 tff(c_12915, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e12)). % 64.74/16.57 tff(c_12020, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e1)). % 64.74/16.57 tff(c_12022, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e5)). % 64.74/16.57 tff(c_12024, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e3)). % 64.74/16.58 tff(c_12023, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e10)). % 64.74/16.58 tff(c_12025, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e12)). % 64.74/16.58 tff(c_12019, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=e2)). % 64.74/16.58 tff(c_12026, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1))). % 64.74/16.58 tff(c_12030, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e4)). % 64.74/16.58 tff(c_12885, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n49, e49), n50, e50), store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n21, e21), n31, e31), n1, e1))=n1)). % 64.74/16.58 tff(c_12029, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e1)). % 64.74/16.58 tff(c_12034, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e10)). % 64.74/16.58 tff(c_12031, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e5)). % 64.74/16.58 tff(c_12028, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e2)). % 64.74/16.58 tff(c_12035, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e12)). % 64.74/16.58 tff(c_12837, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=e4)). % 64.74/16.58 tff(c_12032, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e3)). % 64.74/16.58 tff(c_12036, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1))). % 64.74/16.58 tff(c_12039, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e4)). % 64.74/16.58 tff(c_12853, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n49, e49), n50, e50), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n21, e21), n31, e31), n1))). % 64.74/16.58 tff(c_12038, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e2)). % 64.74/16.58 tff(c_12043, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e10)). % 64.74/16.58 tff(c_12042, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e3)). % 64.74/16.58 tff(c_12040, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e1)). % 64.74/16.58 tff(c_12044, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e12)). % 64.74/16.58 tff(c_12041, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e5)). % 64.74/16.58 tff(c_12048, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e4)). % 64.74/16.58 tff(c_12053, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e12)). % 64.74/16.58 tff(c_12824, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n21, e21), n31, e31), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n49, e49), n1))). % 64.74/16.58 tff(c_12045, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e2)). % 64.74/16.58 tff(c_12049, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e5)). % 64.74/16.58 tff(c_12047, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e1)). % 64.74/16.58 tff(c_12051, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e10)). % 64.74/16.58 tff(c_12050, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e3)). % 64.74/16.58 tff(c_12777, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1)!=e4)). % 64.74/16.58 tff(c_12057, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e1)). % 64.74/16.58 tff(c_12060, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e3)). % 64.74/16.58 tff(c_12061, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e12)). % 64.74/16.58 tff(c_12793, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n49, e49), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n21, e21), n1))). % 64.74/16.58 tff(c_12058, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e5)). % 64.74/16.58 tff(c_12055, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e4)). % 64.74/16.58 tff(c_12054, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e2)). % 64.74/16.59 tff(c_12059, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e10)). % 64.74/16.59 tff(c_12063, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e2)). % 64.74/16.59 tff(c_12064, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e4)). % 64.74/16.59 tff(c_12066, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e5)). % 64.74/16.59 tff(c_12069, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e12)). % 64.74/16.59 tff(c_12062, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e1)). % 64.74/16.59 tff(c_12068, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e3)). % 64.74/16.59 tff(c_12067, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e10)). % 64.74/16.59 tff(c_12070, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e1)). % 64.74/16.59 tff(c_12077, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e10)). % 64.74/16.59 tff(c_12720, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1)!=e4)). % 64.74/16.59 tff(c_12076, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e5)). % 64.74/16.59 tff(c_12072, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e2)). % 64.74/16.59 tff(c_12078, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e12)). % 64.74/16.59 tff(c_12736, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n1))). % 64.74/16.59 tff(c_12074, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e4)). % 64.74/16.59 tff(c_12073, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e3)). % 64.74/16.59 tff(c_12085, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e3)). % 64.74/16.59 tff(c_12083, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e2)). % 64.74/16.59 tff(c_12087, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e4)). % 64.74/16.59 tff(c_12088, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e5)). % 64.74/16.59 tff(c_12082, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e1)). % 64.74/16.59 tff(c_12091, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e12)). % 64.74/16.59 tff(c_12084, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e11)). % 64.74/16.59 tff(c_12089, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e10)). % 64.74/16.59 tff(c_12096, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e5)). % 64.74/16.59 tff(c_12095, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e3)). % 64.74/16.59 tff(c_12097, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e10)). % 64.74/16.59 tff(c_12663, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1)!=e4)). % 64.74/16.59 tff(c_12098, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e4)). % 64.74/16.59 tff(c_12100, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e12)). % 64.74/16.59 tff(c_12093, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e2)). % 64.74/16.59 tff(c_12679, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1))). % 64.74/16.59 tff(c_12094, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e11)). % 64.74/16.59 tff(c_12101, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e1)). % 64.74/16.59 tff(c_12110, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e4)). % 64.74/16.59 tff(c_12106, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e10)). % 64.74/16.59 tff(c_12105, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e5)). % 64.74/16.59 tff(c_12107, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e11)). % 64.74/16.59 tff(c_12102, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e2)). % 64.74/16.59 tff(c_12111, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e12)). % 64.74/16.59 tff(c_12649, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n1))). % 64.74/16.59 tff(c_12103, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e3)). % 64.74/16.59 tff(c_12109, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e1)). % 64.74/16.59 tff(c_12112, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e1)). % 64.74/16.59 tff(c_12116, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e10)). % 64.74/16.59 tff(c_12118, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e11)). % 64.74/16.59 tff(c_12518, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n1)!=e4)). % 64.74/16.59 tff(c_12120, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e12)). % 64.74/16.59 tff(c_12115, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e5)). % 64.74/16.59 tff(c_12113, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e2)). % 64.74/16.59 tff(c_12618, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1))). % 64.74/16.59 tff(c_12114, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e3)). % 64.74/16.59 tff(c_12119, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e4)). % 64.74/16.59 tff(c_12128, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e12)). % 64.74/16.59 tff(c_12127, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e11)). % 64.74/16.59 tff(c_12125, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e10)). % 64.74/16.59 tff(c_12129, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e4)). % 64.74/16.59 tff(c_12123, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e3)). % 64.74/16.60 tff(c_12121, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e1)). % 64.74/16.60 tff(c_12122, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e2)). % 64.74/16.60 tff(c_12124, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e5)). % 64.74/16.60 tff(c_12138, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e12)). % 64.74/16.60 tff(c_12137, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e11)). % 64.74/16.60 tff(c_12135, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e10)). % 64.74/16.60 tff(c_12131, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e2)). % 64.74/16.60 tff(c_12139, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e4)). % 64.74/16.60 tff(c_12133, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e3)). % 64.74/16.60 tff(c_12563, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n1)!=e12)). % 64.74/16.60 tff(c_12134, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e5)). % 64.74/16.60 tff(c_12130, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e1)). % 64.74/16.60 tff(c_12148, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e12)). % 64.74/16.60 tff(c_12147, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e11)). % 64.74/16.60 tff(c_12146, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e10)). % 64.74/16.60 tff(c_12140, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e1)). % 64.74/16.60 tff(c_12142, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e3)). % 64.74/16.60 tff(c_12143, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e4)). % 64.74/16.60 tff(c_12534, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n1)!=e4)). % 64.74/16.60 tff(c_12144, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e5)). % 64.74/16.60 tff(c_12141, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e2)). % 64.74/16.60 tff(c_12159, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e12)). % 64.74/16.60 tff(c_12156, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e9)). % 64.74/16.60 tff(c_12155, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e5)). % 64.74/16.60 tff(c_12151, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e2)). % 64.74/16.60 tff(c_12153, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e4)). % 64.74/16.60 tff(c_12157, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e10)). % 65.00/16.60 tff(c_12505, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n21, e21), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n48, e48), n1))). % 65.00/16.60 tff(c_12158, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e11)). % 65.00/16.60 tff(c_12149, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e1)). % 65.00/16.60 tff(c_12152, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e3)). % 65.00/16.60 tff(c_12167, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e10)). % 65.00/16.60 tff(c_12168, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e11)). % 65.00/16.60 tff(c_12457, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n1)!=e4)). % 65.00/16.60 tff(c_12161, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e2)). % 65.00/16.60 tff(c_12162, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e3)). % 65.00/16.60 tff(c_12166, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e9)). % 65.00/16.60 tff(c_12473, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1, e12), n1, e5), n32, e32), n1, e4), n24, e24), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n46, e46), n47, e47), n1))). % 65.00/16.60 tff(c_12165, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e5)). % 65.00/16.60 tff(c_12160, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e1)). % 65.00/16.60 tff(c_12164, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e4)). % 65.00/16.60 tff(c_12170, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e12)). % 65.00/16.60 tff(c_12178, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e9)). % 65.00/16.60 tff(c_12180, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e11)). % 65.00/16.60 tff(c_12179, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e10)). % 65.00/16.60 tff(c_12177, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e5)). % 65.00/16.60 tff(c_12443, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1, e3), n37, e37), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n1))). % 65.00/16.60 tff(c_12176, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e4)). % 65.00/16.60 tff(c_12171, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e7)). % 65.00/16.60 tff(c_12175, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e3)). % 65.00/16.60 tff(c_12172, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e1)). % 65.00/16.60 tff(c_12181, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e12)). % 65.00/16.60 tff(c_12396, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n1)!=e4)). % 65.00/16.60 tff(c_12174, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e2)). % 65.00/16.60 tff(c_12187, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e4)). % 65.00/16.60 tff(c_12189, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e5)). % 65.00/16.60 tff(c_12412, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1))). % 65.00/16.60 tff(c_12190, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e9)). % 65.00/16.60 tff(c_12186, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e3)). % 65.00/16.60 tff(c_12193, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e11)). % 65.00/16.60 tff(c_12194, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e12)). % 65.00/16.60 tff(c_12183, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e7)). % 65.00/16.60 tff(c_12184, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e1)). % 65.00/16.60 tff(c_12185, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e2)). % 65.00/16.60 tff(c_12191, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n1)!=e10)). % 65.00/16.60 tff(c_12383, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n29, e29), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1))). % 65.00/16.60 tff(c_12204, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e11)). % 65.00/16.60 tff(c_12203, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e10)). % 65.00/16.60 tff(c_12202, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e9)). % 65.00/16.60 tff(c_12200, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e7)). % 65.00/16.60 tff(c_12199, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e5)). % 65.00/16.60 tff(c_12296, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n1)!=e4)). % 65.00/16.60 tff(c_12195, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e1)). % 65.00/16.60 tff(c_12017, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e15)). % 65.00/16.60 tff(c_12205, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e12)). % 65.00/16.60 tff(c_12352, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n1))). % 65.00/16.60 tff(c_12198, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e4)). % 65.00/16.60 tff(c_12197, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e3)). % 65.00/16.60 tff(c_12196, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n1)!=e2)). % 65.00/16.61 tff(c_12212, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e4)). % 65.00/16.61 tff(c_12213, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e5)). % 65.00/16.61 tff(c_12214, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e9)). % 65.00/16.61 tff(c_12215, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e7)). % 65.00/16.61 tff(c_12218, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e12)). % 65.00/16.61 tff(c_12317, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1, e2), n1, e10), n48, e48), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1))). % 65.00/16.61 tff(c_12210, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e3)). % 65.00/16.61 tff(c_12209, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e2)). % 65.00/16.61 tff(c_12208, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e1)). % 65.00/16.61 tff(c_12206, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e6)). % 65.00/16.61 tff(c_12216, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e10)). % 65.00/16.61 tff(c_12217, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e11)). % 65.00/16.61 tff(c_12016, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n1)!=e15)). % 65.00/16.61 tff(c_12080, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1)!=e15)). % 65.00/16.61 tff(c_12281, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1))). % 65.00/16.61 tff(c_12092, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1)!=e13)). % 65.00/16.61 tff(c_12235, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n1)!=e13)). % 65.00/16.61 tff(c_12079, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n1)!=e15)). % 65.00/16.61 tff(c_12246, plain, (e7!=e16)). % 65.00/16.61 tff(c_12247, plain, (e9!=e16)). % 65.00/16.61 tff(c_12266, 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n41, e41), n42, e42), n43, e43), n44, e44), n45, e45), n1)!=e4)). % 65.00/16.61 tff(c_12248, plain, (e16!=e10)). % 65.00/16.61 tff(c_12240, plain, (e16!=e13)). % 65.00/16.61 tff(c_12262, 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, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n50, e50), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1))). % 65.00/16.61 tff(c_12245, plain, (e3!=e16)). % 65.00/16.61 tff(c_12244, plain, (e5!=e16)). % 65.00/16.61 tff(c_12243, plain, (e4!=e16)). % 65.00/16.61 tff(c_12242, plain, (e2!=e16)). % 65.00/16.61 tff(c_12239, plain, (e6!=e16)). % 65.00/16.61 tff(c_12241, plain, (e16!=e1)). % 65.00/16.61 tff(c_12251, plain, (e16!=e12)). % 65.00/16.61 tff(c_12257, 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), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1, e15), n1, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1, e16), n1, e8), n49, e49), n14, e14), n1, e13), n1, e6), n27, e27), n1, e15), n1, e7), n33, e33), n1, e9), n17, e17), n42, e42), n47, e47), n18, e18), n26, e26), n34, e34), n1, e11), n36, e36), n44, e44), n38, e38), n23, e23), n25, e25), n46, e46), n35, e35), n1))). % 65.00/16.61 tff(c_12252, plain, (e16!=e11)). % 65.00/16.61 tff(c_12238, plain, (e16!=e15)). % 65.00/16.61 tff(c_12014, plain, (n16=n1)). % 65.00/16.61 tff(c_11755, plain, (e8!=e15)). % 65.00/16.61 tff(c_11049, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n1, e7), n1, e8), n1, e9), n1, e10), n1, e11), n1, e12), n1, e13), n14, e14), n1)=e13)). % 65.00/16.61 tff(c_11074, plain, (e6!=e15)). % 65.00/16.61 tff(c_11075, plain, (e7!=e15)). % 65.00/16.61 tff(c_11076, plain, (e9!=e15)). % 65.00/16.61 tff(c_11073, plain, (e5!=e15)). % 65.00/16.61 tff(c_11072, plain, (e4!=e15)). % 65.00/16.61 tff(c_11071, plain, (e3!=e15)). % 65.00/16.61 tff(c_11070, plain, (e2!=e15)). % 65.00/16.61 tff(c_11069, plain, (e15!=e1)). % 65.00/16.61 tff(c_11077, plain, (e15!=e10)). % 65.00/16.61 tff(c_11078, plain, (e15!=e11)). % 65.00/16.61 tff(c_11079, plain, (e15!=e12)). % 65.00/16.61 tff(c_11068, plain, (e15!=e13)). % 65.00/16.61 tff(c_11048, plain, (n15=n1)). % 65.00/16.61 tff(c_10228, plain, (e8!=e13)). % 65.00/16.61 tff(c_10229, plain, (e13!=e1)). % 65.00/16.61 tff(c_10230, plain, (e2!=e13)). % 65.00/16.61 tff(c_10231, plain, (e3!=e13)). % 65.00/16.61 tff(c_10232, plain, (e4!=e13)). % 65.00/16.61 tff(c_10233, plain, (e5!=e13)). % 65.00/16.61 tff(c_10234, plain, (e6!=e13)). % 65.00/16.61 tff(c_10235, plain, (e7!=e13)). % 65.00/16.61 tff(c_10236, plain, (e9!=e13)). % 65.00/16.61 tff(c_10237, plain, (e13!=e10)). % 65.00/16.61 tff(c_10238, plain, (e13!=e11)). % 65.00/16.61 tff(c_10224, plain, (e13!=e12)). % 65.00/16.61 tff(c_9956, plain, (n13=n1)). % 65.00/16.61 tff(c_9019, plain, (select(a1, n1)!=e12)). % 65.00/16.61 tff(c_9015, plain, (select(store(a1, n41, e41), n1)!=e12)). % 65.00/16.61 tff(c_9007, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e12)). % 65.00/16.61 tff(c_9003, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e12)). % 65.00/16.61 tff(c_8998, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e12)). % 65.00/16.61 tff(c_8994, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e12)). % 65.00/16.61 tff(c_8986, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e12)). % 65.00/16.61 tff(c_8982, plain, (select(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n1)!=e12)). % 65.00/16.61 tff(c_8977, plain, (select(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n1)!=e12)). % 65.00/16.61 tff(c_8973, plain, (select(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n1)!=e12)). % 65.00/16.61 tff(c_8965, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1)!=e12)). % 65.00/16.61 tff(c_8937, plain, (e8!=e12)). % 65.00/16.61 tff(c_8938, plain, (e12!=e1)). % 65.00/16.61 tff(c_8939, plain, (e2!=e12)). % 65.00/16.61 tff(c_8940, plain, (e3!=e12)). % 65.00/16.61 tff(c_8941, plain, (e4!=e12)). % 65.00/16.61 tff(c_8942, plain, (e5!=e12)). % 65.00/16.61 tff(c_8943, plain, (e6!=e12)). % 65.00/16.61 tff(c_8944, plain, (e7!=e12)). % 65.00/16.61 tff(c_8945, plain, (e9!=e12)). % 65.00/16.61 tff(c_8946, plain, (e12!=e10)). % 65.00/16.61 tff(c_8935, plain, (e12!=e11)). % 65.00/16.61 tff(c_8768, plain, (n12=n1)). % 65.00/16.61 tff(c_8231, plain, (select(a1, n1)!=e11)). % 65.00/16.61 tff(c_8227, plain, (select(store(a1, n41, e41), n1)!=e11)). % 65.00/16.61 tff(c_8218, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e11)). % 65.00/16.61 tff(c_8214, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e11)). % 65.00/16.61 tff(c_8210, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e11)). % 65.00/16.61 tff(c_8206, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e11)). % 65.00/16.61 tff(c_8202, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e11)). % 65.00/16.61 tff(c_8194, plain, (select(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n1)!=e11)). % 65.00/16.61 tff(c_8190, plain, (select(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n1)!=e11)). % 65.00/16.61 tff(c_8186, plain, (select(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n1)!=e11)). % 65.00/16.61 tff(c_8160, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1)!=e11)). % 65.00/16.61 tff(c_8161, plain, (e11!=e1)). % 65.00/16.61 tff(c_8162, plain, (e2!=e11)). % 65.00/16.61 tff(c_8163, plain, (e3!=e11)). % 65.00/16.61 tff(c_8164, plain, (e4!=e11)). % 65.00/16.61 tff(c_8165, plain, (e5!=e11)). % 65.00/16.61 tff(c_8166, plain, (e6!=e11)). % 65.00/16.61 tff(c_8167, plain, (e7!=e11)). % 65.00/16.61 tff(c_8168, plain, (e8!=e11)). % 65.00/16.61 tff(c_8169, plain, (e9!=e11)). % 65.00/16.61 tff(c_8156, plain, (e11!=e10)). % 65.00/16.61 tff(c_7870, plain, (n11=n1)). % 65.00/16.61 tff(c_7104, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n40, e40), n1)!=e10)). % 65.00/16.61 tff(c_7065, plain, (select(a1, n1)!=e10)). % 65.00/16.61 tff(c_7061, plain, (select(store(a1, n41, e41), n1)!=e10)). % 65.00/16.61 tff(c_7057, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e10)). % 65.00/16.61 tff(c_7053, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e10)). % 65.00/16.61 tff(c_7049, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e10)). % 65.00/16.61 tff(c_7041, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e10)). % 65.00/16.61 tff(c_7037, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e10)). % 65.00/16.61 tff(c_7033, plain, (select(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n1)!=e10)). % 65.00/16.61 tff(c_7029, plain, (select(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n1)!=e10)). % 65.00/16.61 tff(c_7025, plain, (select(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n1)!=e10)). % 65.00/16.61 tff(c_6723, plain, (e10!=e1)). % 65.00/16.61 tff(c_6724, plain, (e2!=e10)). % 65.00/16.61 tff(c_6725, plain, (e3!=e10)). % 65.00/16.61 tff(c_6726, plain, (e4!=e10)). % 65.00/16.61 tff(c_6727, plain, (e5!=e10)). % 65.00/16.61 tff(c_6728, plain, (e6!=e10)). % 65.00/16.61 tff(c_6729, plain, (e7!=e10)). % 65.00/16.61 tff(c_6730, plain, (e8!=e10)). % 65.00/16.61 tff(c_6722, plain, (e9!=e10)). % 65.00/16.61 tff(c_6623, plain, (n10=n1)). % 65.00/16.61 tff(c_6542, plain, (select(store(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n20, e20), n1)!=e9)). % 65.00/16.61 tff(c_6513, plain, (select(a1, n1)!=e9)). % 65.00/16.61 tff(c_6508, plain, (select(store(a1, n41, e41), n1)!=e9)). % 65.00/16.61 tff(c_6504, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e9)). % 65.00/16.61 tff(c_6496, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e9)). % 65.00/16.61 tff(c_6492, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e9)). % 65.00/16.61 tff(c_6487, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e9)). % 65.00/16.61 tff(c_6483, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e9)). % 65.00/16.61 tff(c_6475, plain, (select(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n1)!=e9)). % 65.00/16.61 tff(c_6471, plain, (select(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n1)!=e9)). % 65.00/16.61 tff(c_6190, plain, (e9!=e1)). % 65.00/16.61 tff(c_6191, plain, (e9!=e2)). % 65.00/16.61 tff(c_6192, plain, (e9!=e3)). % 65.00/16.61 tff(c_6193, plain, (e9!=e4)). % 65.00/16.61 tff(c_6194, plain, (e9!=e5)). % 65.00/16.62 tff(c_6195, plain, (e9!=e6)). % 65.00/16.62 tff(c_6196, plain, (e9!=e7)). % 65.00/16.62 tff(c_6189, plain, (e9!=e8)). % 65.00/16.62 tff(c_6142, plain, (n9=n1)). % 65.00/16.62 tff(c_5955, plain, (select(store(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n39, e39), n1)!=e8)). % 65.00/16.62 tff(c_6008, plain, (select(a1, n1)!=e8)). % 65.00/16.62 tff(c_6004, plain, (select(store(a1, n41, e41), n1)!=e8)). % 65.00/16.62 tff(c_5996, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e8)). % 65.00/16.62 tff(c_5992, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e8)). % 65.00/16.62 tff(c_5987, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e8)). % 65.00/16.62 tff(c_5983, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e8)). % 65.00/16.62 tff(c_5975, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e8)). % 65.00/16.62 tff(c_5956, plain, (select(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n1)!=e8)). % 65.00/16.62 tff(c_5957, plain, (e8!=e1)). % 65.00/16.62 tff(c_5958, plain, (e8!=e2)). % 65.00/16.62 tff(c_5959, plain, (e8!=e3)). % 65.00/16.62 tff(c_5960, plain, (e8!=e4)). % 65.00/16.62 tff(c_5961, plain, (e8!=e5)). % 65.00/16.62 tff(c_5962, plain, (e8!=e6)). % 65.00/16.62 tff(c_5952, plain, (e8!=e7)). % 65.00/16.62 tff(c_5749, plain, (n8=n1)). % 65.00/16.62 tff(c_4942, plain, (select(store(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n22, e22), n1)!=e7)). % 65.00/16.62 tff(c_4985, plain, (select(a1, n1)!=e7)). % 65.00/16.62 tff(c_4981, plain, (select(store(a1, n41, e41), n1)!=e7)). % 65.00/16.62 tff(c_4977, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e7)). % 65.00/16.62 tff(c_4973, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e7)). % 65.00/16.62 tff(c_4965, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e7)). % 65.00/16.62 tff(c_4961, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e7)). % 65.00/16.62 tff(c_4943, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e7)). % 65.00/16.62 tff(c_4944, plain, (e7!=e1)). % 65.00/16.62 tff(c_4945, plain, (e7!=e2)). % 65.00/16.62 tff(c_4946, plain, (e7!=e3)). % 65.00/16.62 tff(c_4947, plain, (e7!=e4)). % 65.00/16.62 tff(c_4948, plain, (e7!=e5)). % 65.00/16.62 tff(c_4941, plain, (e7!=e6)). % 65.00/16.62 tff(c_4871, plain, (n7=n1)). % 65.00/16.62 tff(c_4647, plain, (select(a1, n1)!=e6)). % 65.00/16.62 tff(c_4643, plain, (select(store(a1, n41, e41), n1)!=e6)). % 65.00/16.62 tff(c_4639, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e6)). % 65.00/16.62 tff(c_4610, plain, (select(store(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n19, e19), n1)!=e6)). % 65.00/16.62 tff(c_4632, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e6)). % 65.00/16.62 tff(c_4628, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e6)). % 65.00/16.62 tff(c_4611, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e6)). % 65.00/16.62 tff(c_4612, plain, (e6!=e1)). % 65.00/16.62 tff(c_4613, plain, (e6!=e2)). % 65.00/16.62 tff(c_4614, plain, (e6!=e3)). % 65.00/16.62 tff(c_4615, plain, (e6!=e4)). % 65.00/16.62 tff(c_4607, plain, (e6!=e5)). % 65.00/16.62 tff(c_4328, plain, (n6=n1)). % 65.00/16.62 tff(c_3363, plain, (select(store(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n28, e28), n1)!=e5)). % 65.00/16.62 tff(c_3392, plain, (select(a1, n1)!=e5)). % 65.00/16.62 tff(c_3388, plain, (select(store(a1, n41, e41), n1)!=e5)). % 65.00/16.62 tff(c_3384, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e5)). % 65.00/16.62 tff(c_3379, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e5)). % 65.00/16.62 tff(c_3364, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e5)). % 65.00/16.62 tff(c_3365, plain, (e5!=e1)). % 65.00/16.62 tff(c_3366, plain, (e5!=e2)). % 65.00/16.62 tff(c_3367, plain, (e5!=e3)). % 65.00/16.62 tff(c_3362, plain, (e5!=e4)). % 65.00/16.62 tff(c_3157, plain, (n5=n1)). % 65.00/16.62 tff(c_2433, plain, (select(store(store(store(store(a1, n41, e41), n30, e30), n45, e45), n43, e43), n1)!=e4)). % 65.00/16.62 tff(c_2456, plain, (select(a1, n1)!=e4)). % 65.00/16.62 tff(c_2452, plain, (select(store(a1, n41, e41), n1)!=e4)). % 65.00/16.62 tff(c_2444, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e4)). % 65.00/16.62 tff(c_2434, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e4)). % 65.00/16.62 tff(c_2435, plain, (e4!=e1)). % 65.00/16.62 tff(c_2436, plain, (e4!=e2)). % 65.00/16.62 tff(c_2430, plain, (e4!=e3)). % 65.00/16.62 tff(c_2278, plain, (n4=n1)). % 65.00/16.62 tff(c_1747, plain, (select(store(store(store(a1, n41, e41), n30, e30), n45, e45), n1)!=e3)). % 65.00/16.62 tff(c_1765, plain, (select(a1, n1)!=e3)). % 65.00/16.62 tff(c_1761, plain, (select(store(a1, n41, e41), n1)!=e3)). % 65.00/16.62 tff(c_1748, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e3)). % 65.00/16.62 tff(c_1749, plain, (e3!=e1)). % 65.00/16.62 tff(c_1745, plain, (e3!=e2)). % 65.00/16.62 tff(c_1583, plain, (n3=n1)). % 65.00/16.62 tff(c_1018, plain, (select(store(store(a1, n41, e41), n30, e30), n1)!=e2)). % 65.00/16.62 tff(c_1031, plain, (select(a1, n1)!=e2)). % 65.00/16.62 tff(c_1019, plain, (select(store(a1, n41, e41), n1)!=e2)). % 65.00/16.62 tff(c_1017, plain, (e2!=e1)). % 65.00/16.62 tff(c_910, plain, (n2=n1)). % 65.00/16.62 tff(c_536, plain, (select(store(a1, n41, e41), n1)!=e1)). % 65.00/16.62 tff(c_535, plain, (select(a1, n1)!=e1)). % 65.00/16.62 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))). % 65.00/16.62 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 65.00/16.62 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.00/16.62 %------------------------------------------------------------------------------