%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV503-1.040 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:30:52 PM UTC 2025 % Result : Satisfiable 23.08s 9.47s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV503-1.040 : TPTP v9.0.0. Released v4.0.0. % 0.06/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.12/0.33 % Computer : n011.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Apr 9 03:38:33 EDT 2025 % 0.12/0.33 % CPUTime : % 23.08/9.47 % 23.08/9.47 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.08/9.47 % 23.08/9.47 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.08/9.48 %$ store > sk > select > #nlpp > n9 > n8 > n7 > n6 > n5 > 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 > e5 > 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 % 23.08/9.48 % 23.08/9.48 %Foreground sorts: % 23.08/9.48 % 23.08/9.48 % 23.08/9.48 %Background operators: % 23.08/9.48 % 23.08/9.48 % 23.08/9.48 %Foreground operators: % 23.08/9.48 tff(e29, type, e29: $i). % 23.08/9.48 tff(a1, type, a1: $i). % 23.08/9.48 tff(n22, type, n22: $i). % 23.08/9.48 tff(n27, type, n27: $i). % 23.08/9.48 tff(n16, type, n16: $i). % 23.08/9.48 tff(n12, type, n12: $i). % 23.08/9.48 tff(e1, type, e1: $i). % 23.08/9.48 tff(e8, type, e8: $i). % 23.08/9.48 tff(e21, type, e21: $i). % 23.08/9.48 tff(n24, type, n24: $i). % 23.08/9.48 tff(e15, type, e15: $i). % 23.08/9.48 tff(e33, type, e33: $i). % 23.08/9.48 tff(n35, type, n35: $i). % 23.08/9.48 tff(e40, type, e40: $i). % 23.08/9.48 tff(e18, type, e18: $i). % 23.08/9.48 tff(e38, type, e38: $i). % 23.08/9.48 tff(e24, type, e24: $i). % 23.08/9.48 tff(e31, type, e31: $i). % 23.08/9.48 tff(n33, type, n33: $i). % 23.08/9.48 tff(n36, type, n36: $i). % 23.08/9.48 tff(e39, type, e39: $i). % 23.08/9.48 tff(store, type, store: ($i * $i * $i) > $i). % 23.08/9.48 tff(n23, type, n23: $i). % 23.08/9.48 tff(n8, type, n8: $i). % 23.08/9.48 tff(e20, type, e20: $i). % 23.08/9.48 tff(e19, type, e19: $i). % 23.08/9.48 tff(e16, type, e16: $i). % 23.08/9.48 tff(n30, type, n30: $i). % 23.08/9.48 tff(e35, type, e35: $i). % 23.08/9.48 tff(e2, type, e2: $i). % 23.08/9.48 tff(n28, type, n28: $i). % 23.08/9.48 tff(n9, type, n9: $i). % 23.08/9.48 tff(e37, type, e37: $i). % 23.08/9.48 tff(e13, type, e13: $i). % 23.08/9.48 tff(n3, type, n3: $i). % 23.08/9.48 tff(e32, type, e32: $i). % 23.08/9.48 tff(e22, type, e22: $i). % 23.08/9.48 tff(n39, type, n39: $i). % 23.08/9.48 tff(e34, type, e34: $i). % 23.08/9.48 tff(n1, type, n1: $i). % 23.08/9.48 tff(n29, type, n29: $i). % 23.08/9.48 tff(e9, type, e9: $i). % 23.08/9.48 tff(n37, type, n37: $i). % 23.08/9.48 tff(n7, type, n7: $i). % 23.08/9.48 tff(e25, type, e25: $i). % 23.08/9.48 tff(e26, type, e26: $i). % 23.08/9.48 tff(n6, type, n6: $i). % 23.08/9.48 tff(e17, type, e17: $i). % 23.08/9.48 tff(n26, type, n26: $i). % 23.08/9.48 tff(e27, type, e27: $i). % 23.08/9.48 tff(e10, type, e10: $i). % 23.08/9.48 tff(e7, type, e7: $i). % 23.08/9.48 tff(n13, type, n13: $i). % 23.08/9.48 tff(sk, type, sk: ($i * $i) > $i). % 23.08/9.48 tff(e36, type, e36: $i). % 23.08/9.48 tff(n4, type, n4: $i). % 23.08/9.48 tff(n10, type, n10: $i). % 23.08/9.48 tff(n14, type, n14: $i). % 23.08/9.48 tff(n15, type, n15: $i). % 23.08/9.48 tff(n17, type, n17: $i). % 23.08/9.48 tff(n40, type, n40: $i). % 23.08/9.48 tff(e30, type, e30: $i). % 23.08/9.48 tff(select, type, select: ($i * $i) > $i). % 23.08/9.48 tff(n31, type, n31: $i). % 23.08/9.48 tff(n32, type, n32: $i). % 23.08/9.48 tff(n20, type, n20: $i). % 23.08/9.48 tff(e23, type, e23: $i). % 23.08/9.48 tff(n18, type, n18: $i). % 23.08/9.48 tff(n38, type, n38: $i). % 23.08/9.48 tff(e14, type, e14: $i). % 23.08/9.48 tff(n11, type, n11: $i). % 23.08/9.48 tff(e12, type, e12: $i). % 23.08/9.48 tff(e4, type, e4: $i). % 23.08/9.48 tff(n34, type, n34: $i). % 23.08/9.48 tff(e6, type, e6: $i). % 23.08/9.48 tff(n19, type, n19: $i). % 23.08/9.48 tff(n2, type, n2: $i). % 23.08/9.48 tff(e11, type, e11: $i). % 23.08/9.48 tff(e28, type, e28: $i). % 23.08/9.48 tff(n5, type, n5: $i). % 23.08/9.48 tff(e3, type, e3: $i). % 23.08/9.48 tff(n25, type, n25: $i). % 23.08/9.48 tff(e5, type, e5: $i). % 23.08/9.48 tff(n21, type, n21: $i). % 23.08/9.48 % 23.08/9.48 %Saturated clause set: % 23.08/9.48 tff(c_6048, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1))). % 23.08/9.48 tff(c_6054, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1))). % 23.08/9.49 tff(c_6061, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1))). % 23.08/9.49 tff(c_6062, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1))). % 23.08/9.49 tff(c_6063, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n1))). % 23.08/9.49 tff(c_6064, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), 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, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1))). % 23.08/9.49 tff(c_6065, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n1))). % 23.08/9.49 tff(c_6066, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1))). % 23.08/9.49 tff(c_6067, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n1))). % 23.08/9.49 tff(c_6068, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n1)!=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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1))). % 23.08/9.49 tff(c_6069, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n1))). % 23.08/9.49 tff(c_6071, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1))). % 23.08/9.49 tff(c_6072, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e5)). % 23.08/9.49 tff(c_6075, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n1))). % 23.08/9.49 tff(c_6077, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e5)). % 23.08/9.49 tff(c_6078, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e3)). % 23.08/9.49 tff(c_6076, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n1)!=e4)). % 23.08/9.49 tff(c_6079, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1))). % 23.08/9.49 tff(c_6081, plain, (select(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e3)). % 23.08/9.49 tff(c_6083, plain, (select(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e5)). % 23.08/9.49 tff(c_6082, plain, (select(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e4)). % 23.08/9.49 tff(c_6080, plain, (select(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n1)!=e9)). % 23.08/9.49 tff(c_6084, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n1))). % 23.08/9.49 tff(c_6087, plain, (select(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e5)). % 23.08/9.49 tff(c_6086, plain, (select(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e4)). % 23.08/9.49 tff(c_6085, plain, (select(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e9)). % 23.08/9.49 tff(c_6088, plain, (select(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e3)). % 23.08/9.49 tff(c_6837, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n1)!=e4)). % 23.08/9.49 tff(c_6089, plain, (select(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n1)!=e1)). % 23.08/9.49 tff(c_6090, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1))). % 23.08/9.50 tff(c_6102, plain, (select(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e5)). % 23.08/9.50 tff(c_6093, plain, (select(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e4)). % 23.08/9.50 tff(c_6108, plain, (select(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e1)). % 23.08/9.50 tff(c_6096, plain, (select(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e3)). % 23.08/9.50 tff(c_6091, plain, (select(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n1)!=e9)). % 23.08/9.50 tff(c_6116, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n1))). % 23.08/9.50 tff(c_6133, plain, (select(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e1)). % 23.08/9.50 tff(c_6152, plain, (select(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e5)). % 23.08/9.50 tff(c_6124, plain, (select(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e3)). % 23.08/9.50 tff(c_6824, plain, (select(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), 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, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1))). % 23.08/9.50 tff(c_6143, plain, (select(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e4)). % 23.08/9.50 tff(c_6094, plain, (select(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=e9)). % 23.08/9.50 tff(c_6162, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n1)!=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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1))). % 23.08/9.50 tff(c_6189, plain, (select(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e1)). % 23.08/9.50 tff(c_6171, plain, (select(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e4)). % 23.08/9.50 tff(c_6357, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1)!=e4)). % 23.08/9.50 tff(c_6180, plain, (select(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e5)). % 23.08/9.50 tff(c_6199, plain, (select(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e3)). % 23.08/9.50 tff(c_6095, plain, (select(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=e9)). % 23.08/9.50 tff(c_6793, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1))). % 23.08/9.50 tff(c_6208, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n1))). % 23.08/9.50 tff(c_6226, plain, (select(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e3)). % 23.08/9.50 tff(c_6097, plain, (select(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e4)). % 23.08/9.50 tff(c_6217, plain, (select(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e5)). % 23.08/9.50 tff(c_6689, plain, (select(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e2)). % 23.08/9.50 tff(c_6098, plain, (select(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e9)). % 23.08/9.50 tff(c_6099, plain, (select(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1)!=e1)). % 23.08/9.50 tff(c_6100, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1))). % 23.08/9.50 tff(c_6765, plain, (select(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n1))). % 23.08/9.50 tff(c_6103, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e1)). % 23.08/9.51 tff(c_6101, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e4)). % 23.08/9.51 tff(c_6104, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e9)). % 23.08/9.51 tff(c_6105, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e5)). % 23.08/9.51 tff(c_6195, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e2)). % 23.08/9.51 tff(c_6121, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=e3)). % 23.08/9.51 tff(c_6106, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n1))). % 23.08/9.51 tff(c_6111, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e1)). % 23.08/9.51 tff(c_6737, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), 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(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1))). % 23.23/9.51 tff(c_6112, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e5)). % 23.23/9.51 tff(c_6110, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e8)). % 23.23/9.51 tff(c_6109, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e3)). % 23.23/9.51 tff(c_6107, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e4)). % 23.23/9.51 tff(c_6113, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e9)). % 23.23/9.51 tff(c_6158, plain, (select(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1)!=e2)). % 23.23/9.51 tff(c_6114, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1))). % 23.23/9.51 tff(c_6117, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e8)). % 23.23/9.51 tff(c_6115, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e1)). % 23.23/9.51 tff(c_6706, plain, (select(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n1))). % 23.23/9.51 tff(c_6120, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e5)). % 23.23/9.51 tff(c_6119, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e4)). % 23.23/9.51 tff(c_6118, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e3)). % 23.23/9.51 tff(c_6122, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e9)). % 23.23/9.51 tff(c_6123, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n1))). % 23.23/9.51 tff(c_6126, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e1)). % 23.23/9.51 tff(c_6059, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e10)). % 23.23/9.51 tff(c_6678, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), 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(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n1))). % 23.23/9.51 tff(c_6125, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e2)). % 23.23/9.51 tff(c_6128, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e3)). % 23.23/9.51 tff(c_6127, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e4)). % 23.23/9.51 tff(c_6129, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e5)). % 23.23/9.51 tff(c_6130, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e8)). % 23.23/9.51 tff(c_6131, plain, (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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n1)!=e9)). % 23.23/9.51 tff(c_6136, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e1)). % 23.23/9.51 tff(c_6060, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e10)). % 23.23/9.51 tff(c_6649, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), n28, e28), n29, e29), n19, e19), 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), n1))). % 23.23/9.51 tff(c_6135, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e2)). % 23.23/9.52 tff(c_6134, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e3)). % 23.23/9.52 tff(c_6138, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e5)). % 23.23/9.52 tff(c_6137, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e4)). % 23.23/9.52 tff(c_6140, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e8)). % 23.23/9.52 tff(c_6139, plain, (select(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n1)!=e2)). % 23.23/9.52 tff(c_6141, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n1)!=e9)). % 23.23/9.52 tff(c_6148, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e2)). % 23.23/9.52 tff(c_6146, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e5)). % 23.23/9.52 tff(c_6617, 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(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), n28, e28), n29, e29), n19, e19))=n1)). % 23.23/9.52 tff(c_6145, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e4)). % 23.23/9.52 tff(c_6147, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e1)). % 23.23/9.52 tff(c_6144, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e3)). % 23.23/9.52 tff(c_6149, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e8)). % 23.23/9.52 tff(c_6150, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e9)). % 23.23/9.52 tff(c_6058, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n1)!=e10)). % 23.23/9.52 tff(c_6153, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e2)). % 23.23/9.52 tff(c_6154, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e4)). % 23.23/9.52 tff(c_6155, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e1)). % 23.23/9.52 tff(c_6586, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n40, e40), 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, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), n28, e28), n29, e29), n1))). % 23.23/9.52 tff(c_6156, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e5)). % 23.23/9.52 tff(c_6151, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e3)). % 23.23/9.52 tff(c_6157, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e8)). % 23.23/9.52 tff(c_6159, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e9)). % 23.23/9.52 tff(c_6160, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e1)). % 23.23/9.52 tff(c_6057, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n1)!=e10)). % 23.23/9.52 tff(c_6161, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e4)). % 23.23/9.52 tff(c_6164, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e2)). % 23.23/9.52 tff(c_6163, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e3)). % 23.23/9.52 tff(c_6555, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), n28, e28), n29, e29), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), n1))). % 23.23/9.52 tff(c_6165, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e5)). % 23.23/9.52 tff(c_6166, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e8)). % 23.23/9.52 tff(c_6167, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e9)). % 23.23/9.52 tff(c_6169, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e3)). % 23.23/9.52 tff(c_6168, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e5)). % 23.23/9.52 tff(c_6056, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n1)!=e10)). % 23.23/9.52 tff(c_6170, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e2)). % 23.23/9.52 tff(c_6172, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e4)). % 23.23/9.52 tff(c_6173, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e1)). % 23.23/9.52 tff(c_6524, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n39, e39), 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(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), n28, e28), n1))). % 23.23/9.52 tff(c_6174, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e8)). % 23.23/9.52 tff(c_6175, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e9)). % 23.23/9.52 tff(c_6179, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e1)). % 23.23/9.53 tff(c_6177, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e2)). % 23.23/9.53 tff(c_6178, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e3)). % 23.23/9.53 tff(c_6055, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n1)!=e10)). % 23.23/9.53 tff(c_6181, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e4)). % 23.23/9.53 tff(c_6176, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e5)). % 23.23/9.53 tff(c_6182, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e8)). % 23.23/9.53 tff(c_6493, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), 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(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), n1))). % 23.23/9.53 tff(c_6183, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e9)). % 23.23/9.53 tff(c_6186, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e3)). % 23.23/9.53 tff(c_6185, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e4)). % 23.23/9.53 tff(c_6184, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e2)). % 23.23/9.53 tff(c_6188, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e5)). % 23.23/9.53 tff(c_6053, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n1)!=e10)). % 23.23/9.53 tff(c_6187, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e1)). % 23.23/9.53 tff(c_6190, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e8)). % 23.23/9.53 tff(c_6191, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e9)). % 23.23/9.53 tff(c_6192, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e1)). % 23.23/9.53 tff(c_6196, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e3)). % 23.23/9.53 tff(c_6197, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e4)). % 23.23/9.53 tff(c_6193, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e2)). % 23.23/9.53 tff(c_6194, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e5)). % 23.23/9.53 tff(c_6052, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n1)!=e10)). % 23.23/9.53 tff(c_6198, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e8)). % 23.23/9.53 tff(c_6200, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e9)). % 23.23/9.53 tff(c_6051, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n1)!=e10)). % 23.23/9.53 tff(c_6205, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e4)). % 23.23/9.53 tff(c_6203, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e2)). % 23.23/9.53 tff(c_6202, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e3)). % 23.23/9.53 tff(c_6201, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e1)). % 23.23/9.54 tff(c_6204, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e5)). % 23.23/9.54 tff(c_6206, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e8)). % 23.23/9.54 tff(c_6207, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e9)). % 23.23/9.54 tff(c_6050, 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n1)!=e10)). % 23.23/9.54 tff(c_6409, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), 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, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n1))). % 23.23/9.54 tff(c_6209, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e3)). % 23.23/9.54 tff(c_6212, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e1)). % 23.23/9.54 tff(c_6211, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e2)). % 23.23/9.54 tff(c_6210, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e4)). % 23.23/9.54 tff(c_6213, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e5)). % 23.23/9.54 tff(c_6323, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), 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(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n1))). % 23.23/9.54 tff(c_6214, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e8)). % 23.23/9.54 tff(c_6215, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e9)). % 23.23/9.54 tff(c_6049, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n1)!=e10)). % 23.23/9.54 tff(c_6378, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), 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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n1))). % 23.23/9.54 tff(c_6220, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e1)). % 23.23/9.54 tff(c_6218, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e2)). % 23.23/9.54 tff(c_6219, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e3)). % 23.23/9.54 tff(c_6221, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e4)). % 23.23/9.54 tff(c_6216, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e5)). % 23.23/9.54 tff(c_6222, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e8)). % 23.23/9.54 tff(c_6223, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e9)). % 23.23/9.54 tff(c_6047, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n1)!=e10)). % 23.23/9.54 tff(c_6341, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), 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, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n1))). % 23.23/9.54 tff(c_6252, plain, (select(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n1)!=e11)). % 23.23/9.54 tff(c_6232, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n1)!=e10)). % 23.23/9.54 tff(c_6253, plain, (select(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n1)!=e11)). % 23.23/9.54 tff(c_6238, plain, (select(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1)!=e9)). % 23.23/9.54 tff(c_6239, plain, (select(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1)!=e8)). % 23.23/9.54 tff(c_6243, plain, (select(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n1)!=e8)). % 23.23/9.54 tff(c_6244, plain, (select(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n1)!=e6)). % 23.23/9.54 tff(c_6237, plain, (select(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n1)!=e9)). % 23.23/9.54 tff(c_6309, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), 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(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n1))). % 23.23/9.54 tff(c_6245, plain, (select(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n1)!=e6)). % 23.23/9.54 tff(c_6236, plain, (select(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n1)!=e9)). % 23.23/9.54 tff(c_6242, plain, (select(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n1)!=e8)). % 23.23/9.54 tff(c_6247, plain, (select(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n1)!=e6)). % 23.23/9.54 tff(c_6248, plain, (select(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n1)!=e5)). % 23.23/9.54 tff(c_6288, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n27, e27), n28, e28), n29, e29), n30, e30), n31, e31), n32, e32), n33, e33), n34, e34), n35, e35), n36, e36), n37, e37), n38, e38), 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(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1, e2), n40, e40), n38, e38), n39, e39), n1, e1), n1, e9), n1, e3), n1, e5), n1, e4), n30, e30), n15, e15), n34, e34), n1))). % 23.23/9.54 tff(c_6241, plain, (select(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n1)!=e8)). % 23.23/9.54 tff(c_6235, plain, (select(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n1)!=e9)). % 23.23/9.54 tff(c_6255, plain, (e11!=e1)). % 23.23/9.54 tff(c_6276, plain, (select(store(store(store(store(store(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), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n26, e26), n1)!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), n33, e33), n1))). % 23.23/9.54 tff(c_6254, plain, (e3!=e11)). % 23.23/9.54 tff(c_6256, plain, (e2!=e11)). % 23.23/9.54 tff(c_6264, plain, (e5!=e11)). % 23.23/9.54 tff(c_6265, plain, (e4!=e11)). % 23.23/9.55 tff(c_6270, plain, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1, e11), n25, e25), n17, e17), n7, e7), n32, e32), n1, e6), n18, e18), n37, e37), n31, e31), n13, e13), n12, e12), n36, e36), n20, e20), n35, e35), n23, e23), n26, e26), n21, e21), n27, e27), n1, e10), n22, e22), n1, e8), 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(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1, e8), n1, e9), n1, e10), n1, e11), n12, e12), n13, e13), n14, e14), n15, e15), n16, e16), n17, e17), n18, e18), n19, e19), n20, e20), n21, e21), n22, e22), n23, e23), n24, e24), n25, e25), n1))). % 23.23/9.55 tff(c_6263, plain, (e6!=e11)). % 23.23/9.55 tff(c_6262, plain, (e8!=e11)). % 23.23/9.55 tff(c_6261, plain, (e9!=e11)). % 23.23/9.55 tff(c_6251, plain, (e11!=e10)). % 23.23/9.55 tff(c_6045, plain, (n11=n1)). % 23.23/9.55 tff(c_5383, plain, (e3!=e10)). % 23.23/9.55 tff(c_5384, plain, (e2!=e10)). % 23.23/9.55 tff(c_5385, plain, (e10!=e1)). % 23.23/9.55 tff(c_5387, plain, (e5!=e10)). % 23.23/9.55 tff(c_5388, plain, (e4!=e10)). % 23.23/9.55 tff(c_5386, plain, (e6!=e10)). % 23.23/9.55 tff(c_5389, plain, (e8!=e10)). % 23.23/9.55 tff(c_5381, plain, (e9!=e10)). % 23.23/9.55 tff(c_5231, plain, (n10=n1)). % 23.23/9.55 tff(c_4740, plain, (select(a1, n1)!=e9)). % 23.23/9.55 tff(c_4736, plain, (select(store(a1, n16, e16), n1)!=e9)). % 23.23/9.55 tff(c_4732, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e9)). % 23.23/9.55 tff(c_4728, plain, (select(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1)!=e9)). % 23.23/9.55 tff(c_4694, plain, (e9!=e5)). % 23.23/9.55 tff(c_4695, plain, (e9!=e6)). % 23.23/9.55 tff(c_4693, plain, (e9!=e1)). % 23.23/9.55 tff(c_4692, plain, (e9!=e2)). % 23.23/9.55 tff(c_4691, plain, (e9!=e4)). % 23.23/9.55 tff(c_4690, plain, (e9!=e3)). % 23.23/9.55 tff(c_4688, plain, (e9!=e8)). % 23.23/9.55 tff(c_4505, plain, (n9=n1)). % 23.23/9.55 tff(c_3949, plain, (select(a1, n1)!=e8)). % 23.23/9.55 tff(c_3945, plain, (select(store(a1, n16, e16), n1)!=e8)). % 23.23/9.55 tff(c_3937, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e8)). % 23.23/9.55 tff(c_3933, plain, (select(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1)!=e8)). % 23.23/9.55 tff(c_3707, plain, (e8!=e2)). % 23.23/9.55 tff(c_3708, plain, (e8!=e3)). % 23.23/9.55 tff(c_3709, plain, (e8!=e4)). % 23.23/9.55 tff(c_3710, plain, (e8!=e5)). % 23.23/9.55 tff(c_3687, plain, (select(store(store(store(store(store(store(store(a1, n1, e1), n1, e2), n1, e3), n1, e4), n1, e5), n1, e6), n7, e7), n1)=e6)). % 23.23/9.55 tff(c_3706, plain, (e8!=e1)). % 23.23/9.55 tff(c_3705, plain, (e8!=e6)). % 23.23/9.55 tff(c_3686, plain, (n8=n1)). % 23.23/9.55 tff(c_3372, plain, (select(a1, n1)!=e6)). % 23.23/9.55 tff(c_3368, plain, (select(store(a1, n16, e16), n1)!=e6)). % 23.23/9.55 tff(c_3364, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e6)). % 23.23/9.55 tff(c_3359, plain, (select(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1)!=e6)). % 23.23/9.55 tff(c_3339, plain, (e6!=e1)). % 23.23/9.55 tff(c_3340, plain, (e6!=e2)). % 23.23/9.55 tff(c_3341, plain, (e6!=e3)). % 23.23/9.55 tff(c_3342, plain, (e6!=e4)). % 23.23/9.55 tff(c_3334, plain, (e6!=e5)). % 23.23/9.55 tff(c_3143, plain, (n6=n1)). % 23.23/9.55 tff(c_2499, plain, (select(a1, n1)!=e5)). % 23.23/9.55 tff(c_2495, plain, (select(store(a1, n16, e16), n1)!=e5)). % 23.23/9.55 tff(c_2487, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e5)). % 23.23/9.55 tff(c_2483, plain, (select(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1)!=e5)). % 23.23/9.55 tff(c_2468, plain, (e5!=e1)). % 23.23/9.55 tff(c_2469, plain, (e5!=e2)). % 23.23/9.55 tff(c_2470, plain, (e5!=e3)). % 23.23/9.55 tff(c_2465, plain, (e5!=e4)). % 23.23/9.55 tff(c_2314, plain, (n5=n1)). % 23.23/9.55 tff(c_1797, plain, (select(a1, n1)!=e4)). % 23.23/9.55 tff(c_1793, plain, (select(store(a1, n16, e16), n1)!=e4)). % 23.23/9.55 tff(c_1785, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e4)). % 23.43/9.55 tff(c_1775, plain, (select(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1)!=e4)). % 23.43/9.55 tff(c_1776, plain, (e4!=e1)). % 23.43/9.55 tff(c_1777, plain, (e4!=e2)). % 23.43/9.55 tff(c_1771, plain, (e4!=e3)). % 23.43/9.55 tff(c_1654, plain, (n4=n1)). % 23.43/9.55 tff(c_1235, plain, (select(store(store(store(a1, n16, e16), n14, e14), n24, e24), n1)!=e3)). % 23.43/9.55 tff(c_1254, plain, (select(a1, n1)!=e3)). % 23.43/9.55 tff(c_1249, plain, (select(store(a1, n16, e16), n1)!=e3)). % 23.43/9.55 tff(c_1236, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e3)). % 23.43/9.55 tff(c_1237, plain, (e3!=e1)). % 23.43/9.55 tff(c_1234, plain, (e3!=e2)). % 23.43/9.55 tff(c_1127, plain, (n3=n1)). % 23.43/9.55 tff(c_741, plain, (select(store(store(a1, n16, e16), n14, e14), n1)!=e2)). % 23.43/9.55 tff(c_750, plain, (select(a1, n1)!=e2)). % 23.43/9.55 tff(c_742, plain, (select(store(a1, n16, e16), n1)!=e2)). % 23.43/9.55 tff(c_740, plain, (e2!=e1)). % 23.43/9.55 tff(c_673, plain, (n2=n1)). % 23.43/9.55 tff(c_436, plain, (select(store(a1, n16, e16), n1)!=e1)). % 23.43/9.55 tff(c_435, plain, (select(a1, n1)!=e1)). % 23.43/9.56 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))). % 23.43/9.56 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 23.43/9.56 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.43/9.56 %------------------------------------------------------------------------------