%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV506-1.030 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n012.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:55 PM UTC 2025 % Result : Satisfiable 22.93s 10.39s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV506-1.030 : TPTP v9.0.0. Released v4.0.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 03:38:44 EDT 2025 % 0.13/0.34 % CPUTime : % 22.86/10.38 % 22.93/10.39 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.93/10.39 % 22.93/10.39 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.93/10.40 %$ store > sk > select > #nlpp > i_1129 > i9 > i8 > i7 > i6 > i5 > i4 > i30 > i3 > i29 > i28 > i27 > i26 > i25 > i24 > i23 > i22 > i21 > i20 > i2 > i19 > i18 > i17 > i16 > i15 > i14 > i13 > i12 > i11 > i10 > i1 > e_1131 > e_1130 > e9 > e8 > e7 > e6 > e5 > e4 > e30 > e3 > e29 > e28 > e27 > e26 > e25 > e24 > e23 > e22 > e21 > e20 > e2 > e19 > e18 > e17 > e16 > e15 > e14 > e13 > e12 > e11 > e10 > e1 > a_1128 > a_1127 > a_1126 > a_1125 > a_1124 > a_1123 > a_1122 > a_1121 > a_1120 > a_1119 > a_1118 > a_1117 > a_1116 > a_1115 > a_1114 > a_1113 > a_1112 > a_1111 > a_1110 > a_1109 > a_1108 > a_1107 > a_1106 > a_1105 > a_1104 > a_1103 > a_1102 > a_1101 > a_1100 > a_1099 > a_1098 > a_1097 > a_1096 > a_1095 > a_1094 > a_1093 > a_1092 > a_1091 > a_1090 > a_1089 > a_1088 > a_1087 > a_1086 > a_1085 > a_1084 > a_1083 > a_1082 > a_1081 > a_1080 > a_1079 > a_1078 > a_1077 > a_1076 > a_1075 > a_1074 > a_1073 > a_1072 > a_1071 > a_1070 > a_1069 > a1 % 22.93/10.40 % 22.93/10.40 %Foreground sorts: % 22.93/10.40 % 22.93/10.40 % 22.93/10.40 %Background operators: % 22.93/10.40 % 22.93/10.40 % 22.93/10.40 %Foreground operators: % 22.93/10.40 tff(e29, type, e29: $i). % 22.93/10.40 tff(a_1096, type, a_1096: $i). % 22.93/10.40 tff(a1, type, a1: $i). % 22.93/10.40 tff(e1, type, e1: $i). % 22.93/10.40 tff(a_1092, type, a_1092: $i). % 22.93/10.40 tff(e8, type, e8: $i). % 22.93/10.40 tff(e_1130, type, e_1130: $i). % 22.93/10.40 tff(a_1094, type, a_1094: $i). % 22.93/10.40 tff(a_1089, type, a_1089: $i). % 22.93/10.40 tff(a_1116, type, a_1116: $i). % 22.93/10.40 tff(e21, type, e21: $i). % 22.93/10.40 tff(a_1107, type, a_1107: $i). % 22.93/10.40 tff(i16, type, i16: $i). % 22.93/10.40 tff(a_1109, type, a_1109: $i). % 22.93/10.40 tff(a_1100, type, a_1100: $i). % 22.93/10.40 tff(a_1084, type, a_1084: $i). % 22.93/10.40 tff(a_1074, type, a_1074: $i). % 22.93/10.40 tff(e15, type, e15: $i). % 22.93/10.40 tff(i14, type, i14: $i). % 22.93/10.40 tff(a_1087, type, a_1087: $i). % 22.93/10.40 tff(i11, type, i11: $i). % 22.93/10.40 tff(a_1103, type, a_1103: $i). % 22.93/10.40 tff(a_1108, type, a_1108: $i). % 22.93/10.40 tff(e18, type, e18: $i). % 22.93/10.40 tff(a_1101, type, a_1101: $i). % 22.93/10.40 tff(e24, type, e24: $i). % 22.93/10.40 tff(a_1105, type, a_1105: $i). % 22.93/10.40 tff(a_1085, type, a_1085: $i). % 22.93/10.40 tff(i23, type, i23: $i). % 22.93/10.40 tff(a_1121, type, a_1121: $i). % 22.93/10.40 tff(i30, type, i30: $i). % 22.93/10.40 tff(a_1102, type, a_1102: $i). % 22.93/10.40 tff(store, type, store: ($i * $i * $i) > $i). % 22.93/10.40 tff(a_1070, type, a_1070: $i). % 22.93/10.40 tff(a_1111, type, a_1111: $i). % 22.93/10.40 tff(e20, type, e20: $i). % 22.93/10.40 tff(e19, type, e19: $i). % 22.93/10.40 tff(e16, type, e16: $i). % 22.93/10.40 tff(i20, type, i20: $i). % 22.93/10.40 tff(e2, type, e2: $i). % 22.93/10.40 tff(a_1120, type, a_1120: $i). % 22.93/10.40 tff(i18, type, i18: $i). % 22.93/10.40 tff(i27, type, i27: $i). % 22.93/10.40 tff(a_1099, type, a_1099: $i). % 22.93/10.40 tff(i26, type, i26: $i). % 22.93/10.40 tff(a_1072, type, a_1072: $i). % 22.93/10.40 tff(a_1110, type, a_1110: $i). % 22.93/10.40 tff(e13, type, e13: $i). % 22.93/10.40 tff(a_1081, type, a_1081: $i). % 22.93/10.40 tff(i22, type, i22: $i). % 22.93/10.40 tff(e22, type, e22: $i). % 22.93/10.40 tff(i12, type, i12: $i). % 22.93/10.40 tff(i15, type, i15: $i). % 22.93/10.40 tff(i17, type, i17: $i). % 22.93/10.40 tff(i19, type, i19: $i). % 22.93/10.40 tff(i21, type, i21: $i). % 22.93/10.40 tff(a_1104, type, a_1104: $i). % 22.93/10.40 tff(e9, type, e9: $i). % 22.93/10.40 tff(a_1090, type, a_1090: $i). % 22.93/10.40 tff(i25, type, i25: $i). % 22.93/10.40 tff(i28, type, i28: $i). % 22.93/10.40 tff(a_1126, type, a_1126: $i). % 22.93/10.40 tff(a_1091, type, a_1091: $i). % 22.93/10.40 tff(a_1077, type, a_1077: $i). % 22.93/10.40 tff(e25, type, e25: $i). % 22.93/10.40 tff(e26, type, e26: $i). % 22.93/10.40 tff(i10, type, i10: $i). % 22.93/10.40 tff(e_1131, type, e_1131: $i). % 22.93/10.40 tff(e17, type, e17: $i). % 22.93/10.40 tff(e27, type, e27: $i). % 22.93/10.40 tff(a_1127, type, a_1127: $i). % 22.93/10.40 tff(e10, type, e10: $i). % 22.93/10.40 tff(e7, type, e7: $i). % 22.93/10.40 tff(a_1098, type, a_1098: $i). % 22.93/10.40 tff(a_1095, type, a_1095: $i). % 22.93/10.40 tff(i8, type, i8: $i). % 22.93/10.40 tff(i9, type, i9: $i). % 22.93/10.40 tff(sk, type, sk: ($i * $i) > $i). % 22.93/10.40 tff(i29, type, i29: $i). % 22.93/10.40 tff(i7, type, i7: $i). % 22.93/10.40 tff(a_1075, type, a_1075: $i). % 22.93/10.40 tff(i1, type, i1: $i). % 22.93/10.40 tff(a_1069, type, a_1069: $i). % 22.93/10.40 tff(a_1113, type, a_1113: $i). % 22.93/10.40 tff(i2, type, i2: $i). % 22.93/10.40 tff(a_1071, type, a_1071: $i). % 22.93/10.40 tff(e30, type, e30: $i). % 22.93/10.40 tff(select, type, select: ($i * $i) > $i). % 22.93/10.40 tff(a_1097, type, a_1097: $i). % 22.93/10.40 tff(a_1122, type, a_1122: $i). % 22.93/10.40 tff(a_1125, type, a_1125: $i). % 22.93/10.40 tff(a_1093, type, a_1093: $i). % 22.93/10.40 tff(a_1112, type, a_1112: $i). % 22.93/10.40 tff(a_1114, type, a_1114: $i). % 22.93/10.40 tff(e23, type, e23: $i). % 22.93/10.40 tff(a_1118, type, a_1118: $i). % 22.93/10.40 tff(e14, type, e14: $i). % 22.93/10.40 tff(a_1115, type, a_1115: $i). % 22.93/10.40 tff(a_1086, type, a_1086: $i). % 22.93/10.40 tff(e12, type, e12: $i). % 22.93/10.40 tff(e4, type, e4: $i). % 22.93/10.40 tff(i13, type, i13: $i). % 22.93/10.40 tff(a_1083, type, a_1083: $i). % 22.93/10.40 tff(a_1076, type, a_1076: $i). % 22.93/10.40 tff(a_1106, type, a_1106: $i). % 22.93/10.40 tff(a_1123, type, a_1123: $i). % 22.93/10.40 tff(a_1119, type, a_1119: $i). % 22.93/10.40 tff(a_1124, type, a_1124: $i). % 22.93/10.40 tff(e6, type, e6: $i). % 22.93/10.40 tff(i5, type, i5: $i). % 22.93/10.40 tff(i_1129, type, i_1129: $i). % 22.93/10.40 tff(e11, type, e11: $i). % 22.93/10.40 tff(a_1082, type, a_1082: $i). % 22.93/10.40 tff(e28, type, e28: $i). % 22.93/10.40 tff(i4, type, i4: $i). % 22.93/10.40 tff(a_1079, type, a_1079: $i). % 22.93/10.40 tff(e3, type, e3: $i). % 22.93/10.40 tff(a_1073, type, a_1073: $i). % 22.93/10.40 tff(a_1080, type, a_1080: $i). % 22.93/10.40 tff(i24, type, i24: $i). % 22.93/10.40 tff(e5, type, e5: $i). % 22.93/10.40 tff(a_1088, type, a_1088: $i). % 22.93/10.40 tff(i3, type, i3: $i). % 22.93/10.40 tff(a_1117, type, a_1117: $i). % 22.93/10.40 tff(a_1078, type, a_1078: $i). % 22.93/10.40 tff(a_1128, type, a_1128: $i). % 22.93/10.40 tff(i6, type, i6: $i). % 22.93/10.40 % 22.93/10.40 %Saturated clause set: % 22.93/10.40 tff(c_20239, plain, (select(a1, i30)=e_1130)). % 22.93/10.40 tff(c_20226, plain, (select(a_1069, i30)=e_1130)). % 22.93/10.40 tff(c_20209, plain, (select(a_1070, i30)=e_1130)). % 22.93/10.40 tff(c_20151, plain, (select(a_1071, i30)=e_1130)). % 22.93/10.40 tff(c_20110, plain, (select(a_1072, i30)=e_1130)). % 22.93/10.40 tff(c_19394, plain, (select(a_1082, i30)=e_1130)). % 22.93/10.40 tff(c_20113, plain, (select(a_1112, i30)=e30)). % 22.93/10.40 tff(c_19372, plain, (select(a_1073, i30)=e_1130)). % 22.93/10.40 tff(c_19429, plain, (select(a_1092, i30)=e_1130)). % 22.93/10.40 tff(c_20071, plain, (select(a_1122, i30)=e30)). % 22.93/10.40 tff(c_19421, plain, (select(a_1087, i30)=e_1130)). % 22.93/10.40 tff(c_19419, plain, (select(a_1086, i30)=e_1130)). % 22.93/10.40 tff(c_19971, plain, (select(a_1078, i30)=e_1130)). % 22.93/10.40 tff(c_20013, plain, (select(a_1110, i30)=e30)). % 22.93/10.40 tff(c_19381, plain, (select(a_1077, i30)=e_1130)). % 22.93/10.40 tff(c_19377, plain, (select(a_1076, i30)=e_1130)). % 22.93/10.40 tff(c_19972, plain, (select(a_1123, i30)=e30)). % 22.93/10.40 tff(c_19387, plain, (select(a_1079, i30)=e_1130)). % 22.93/10.40 tff(c_19376, plain, (select(a_1075, i30)=e_1130)). % 22.93/10.40 tff(c_19931, plain, (select(a_1105, i30)=e30)). % 22.93/10.40 tff(c_19916, plain, (select(a_1109, i30)=e30)). % 22.93/10.40 tff(c_19608, plain, (select(a_1093, i30)=e_1130)). % 22.93/10.40 tff(c_19427, plain, (select(a_1090, i30)=e_1130)). % 22.93/10.40 tff(c_19874, plain, (select(a_1127, i30)=e30)). % 22.93/10.40 tff(c_19425, plain, (select(a_1089, i30)=e_1130)). % 22.93/10.40 tff(c_19845, plain, (select(a_1116, i30)=e30)). % 22.93/10.40 tff(c_19423, plain, (select(a_1088, i30)=e_1130)). % 22.93/10.40 tff(c_19441, plain, (select(a_1095, i30)=e_1130)). % 22.93/10.40 tff(c_19806, plain, (select(a_1124, i30)=e30)). % 22.93/10.40 tff(c_19447, plain, (select(a_1097, i30)=e_1130)). % 22.93/10.40 tff(c_19779, plain, (select(a_1125, i30)=e30)). % 22.93/10.40 tff(c_19741, plain, (select(a_1117, i30)=e30)). % 22.93/10.40 tff(c_19754, plain, (select(a_1126, i30)=e30)). % 22.93/10.40 tff(c_19428, plain, (select(a_1091, i30)=e_1130)). % 22.93/10.40 tff(c_19729, plain, (select(a_1118, i30)=e30)). % 22.93/10.40 tff(c_19714, plain, (select(a_1114, i30)=e30)). % 22.93/10.40 tff(c_19701, plain, (select(a_1115, i30)=e30)). % 22.93/10.40 tff(c_19686, plain, (select(a_1107, i30)=e30)). % 22.93/10.40 tff(c_19445, plain, (select(a_1096, i30)=e_1130)). % 22.93/10.40 tff(c_19661, plain, (select(a_1108, i30)=e30)). % 22.93/10.40 tff(c_19405, plain, (select(a_1085, i30)=e_1130)). % 22.93/10.40 tff(c_19449, plain, (select(a_1098, i30)=e_1130)). % 22.93/10.40 tff(c_19622, plain, (select(a_1128, i30)=e30)). % 22.93/10.40 tff(c_19609, plain, (select(a_1113, i30)=e30)). % 22.93/10.40 tff(c_19433, plain, (select(a_1094, i30)=e_1130)). % 22.93/10.40 tff(c_19400, plain, (select(a_1083, i30)=e_1130)). % 22.93/10.40 tff(c_19570, plain, (select(a_1121, i30)=e30)). % 22.93/10.40 tff(c_19557, plain, (select(a_1106, i30)=e30)). % 22.93/10.40 tff(c_19393, plain, (select(a_1081, i30)=e_1130)). % 22.93/10.40 tff(c_19528, plain, (select(a_1120, i30)=e30)). % 22.93/10.40 tff(c_19375, plain, (select(a_1074, i30)=e_1130)). % 22.93/10.40 tff(c_19450, plain, (sk(a_1098, a_1128)=i30)). % 22.93/10.40 tff(c_19499, plain, (select(a_1119, i30)=e30)). % 22.93/10.40 tff(c_19388, plain, (select(a_1080, i30)=e_1130)). % 22.93/10.41 tff(c_19474, plain, (select(a_1111, i30)=e30)). % 22.93/10.41 tff(c_19404, plain, (select(a_1084, i30)=e_1130)). % 22.93/10.41 tff(c_19457, plain, (e_1130!=e30)). % 22.93/10.41 tff(c_19452, plain, (e_1131=e30)). % 22.93/10.41 tff(c_19370, plain, (i_1129=i30)). % 22.93/10.41 tff(c_1544, plain, (![J_14]: (select(a_1117, J_14)=select(a_1116, J_14) | i26=J_14))). % 22.93/10.41 tff(c_1514, plain, (![J_14]: (select(a_1080, J_14)=select(a_1079, J_14) | i12=J_14))). % 22.93/10.41 tff(c_1613, plain, (![J_14]: (select(a_1124, J_14)=select(a_1123, J_14) | i17=J_14))). % 22.93/10.41 tff(c_1481, plain, (![J_14]: (select(a_1113, J_14)=select(a_1112, J_14) | i11=J_14))). % 22.93/10.41 tff(c_1652, plain, (![J_14]: (select(a_1076, J_14)=select(a_1075, J_14) | i8=J_14))). % 22.93/10.41 tff(c_1616, plain, (![J_14]: (select(a_1123, J_14)=select(a_1122, J_14) | i28=J_14))). % 22.93/10.41 tff(c_1553, plain, (![J_14]: (select(a_1115, J_14)=select(a_1114, J_14) | i29=J_14))). % 22.93/10.41 tff(c_1589, plain, (![J_14]: (select(a_1073, J_14)=select(a_1072, J_14) | i5=J_14))). % 22.93/10.41 tff(c_1511, plain, (![J_14]: (select(a_1102, J_14)=select(a_1101, J_14) | i4=J_14))). % 22.93/10.41 tff(c_1640, plain, (![J_14]: (select(a_1095, J_14)=select(a_1094, J_14) | i27=J_14))). % 22.93/10.41 tff(c_1493, plain, (![J_14]: (select(a_1118, J_14)=select(a_1117, J_14) | i22=J_14))). % 22.93/10.41 tff(c_1637, plain, (![J_14]: (select(a_1104, J_14)=select(a_1103, J_14) | i30=J_14))). % 22.93/10.41 tff(c_1517, plain, (![J_14]: (select(a_1109, J_14)=select(a_1108, J_14) | i20=J_14))). % 22.93/10.41 tff(c_1562, plain, (![J_14]: (select(a_1127, J_14)=select(a_1126, J_14) | i7=J_14))). % 22.93/10.41 tff(c_1523, plain, (![J_14]: (select(a_1091, J_14)=select(a_1090, J_14) | i23=J_14))). % 22.93/10.41 tff(c_1649, plain, (![J_14]: (select(a_1119, J_14)=select(a_1118, J_14) | i27=J_14))). % 22.93/10.41 tff(c_1586, plain, (![J_14]: (select(a_1085, J_14)=select(a_1084, J_14) | i17=J_14))). % 22.93/10.41 tff(c_1610, plain, (![J_14]: (select(a_1086, J_14)=select(a_1085, J_14) | i18=J_14))). % 22.93/10.41 tff(c_1565, plain, (![J_14]: (select(a_1072, J_14)=select(a_1071, J_14) | i4=J_14))). % 22.93/10.41 tff(c_1658, plain, (![J_14]: (select(a_1081, J_14)=select(a_1080, J_14) | i13=J_14))). % 22.93/10.41 tff(c_1622, plain, (![J_14]: (select(a_1093, J_14)=select(a_1092, J_14) | i25=J_14))). % 22.93/10.41 tff(c_1583, plain, (![J_14]: (select(a_1111, J_14)=select(a_1110, J_14) | i21=J_14))). % 22.93/10.41 tff(c_1532, plain, (![J_14]: (select(a_1126, J_14)=select(a_1125, J_14) | i24=J_14))). % 22.93/10.41 tff(c_1574, plain, (![J_14]: (select(a_1112, J_14)=select(a_1111, J_14) | i6=J_14))). % 22.93/10.41 tff(c_1568, plain, (![J_14]: (select(a_1074, J_14)=select(a_1073, J_14) | i6=J_14))). % 22.93/10.41 tff(c_1538, plain, (![J_14]: (select(a_1096, J_14)=select(a_1095, J_14) | i28=J_14))). % 22.93/10.41 tff(c_1499, plain, (![J_14]: (select(a_1092, J_14)=select(a_1091, J_14) | i24=J_14))). % 22.93/10.41 tff(c_1526, plain, (![J_14]: (select(a_1105, J_14)=select(a_1104, J_14) | i2=J_14))). % 22.93/10.41 tff(c_1580, plain, (![J_14]: (select(a_1088, J_14)=select(a_1087, J_14) | i20=J_14))). % 22.93/10.41 tff(c_1655, plain, (![J_14]: (select(a_1083, J_14)=select(a_1082, J_14) | i15=J_14))). % 22.93/10.41 tff(c_1547, plain, (![J_14]: (select(a_1100, J_14)=select(a_1099, J_14) | i1=J_14))). % 22.93/10.41 tff(c_1604, plain, (![J_14]: (select(a_1084, J_14)=select(a_1083, J_14) | i16=J_14))). % 22.93/10.41 tff(c_1550, plain, (![J_14]: (select(a_1120, J_14)=select(a_1119, J_14) | i3=J_14))). % 22.93/10.41 tff(c_1598, plain, (![J_14]: (select(a_1108, J_14)=select(a_1107, J_14) | i18=J_14))). % 22.93/10.41 tff(c_1628, plain, (![J_14]: (select(a_1070, J_14)=select(a_1069, J_14) | i2=J_14))). % 22.93/10.41 tff(c_1505, plain, (![J_14]: (select(a_1090, J_14)=select(a_1089, J_14) | i22=J_14))). % 22.93/10.41 tff(c_1634, plain, (![J_14]: (select(a_1101, J_14)=select(a_1100, J_14) | i19=J_14))). % 22.93/10.41 tff(c_1592, plain, (![J_14]: (select(a_1103, J_14)=select(a_1102, J_14) | i9=J_14))). % 22.93/10.41 tff(c_1631, plain, (![J_14]: (select(a_1128, J_14)=select(a_1127, J_14) | i10=J_14))). % 22.93/10.41 tff(c_1484, plain, (![J_14]: (select(a_1116, J_14)=select(a_1115, J_14) | i5=J_14))). % 22.93/10.41 tff(c_1529, plain, (![J_14]: (select(a_1099, J_14)=select(a1, J_14) | i13=J_14))). % 22.93/10.41 tff(c_1487, plain, (![J_14]: (select(a_1110, J_14)=select(a_1109, J_14) | i8=J_14))). % 22.93/10.41 tff(c_1490, plain, (![J_14]: (select(a_1106, J_14)=select(a_1105, J_14) | i15=J_14))). % 22.93/10.41 tff(c_1502, plain, (![J_14]: (select(a_1125, J_14)=select(a_1124, J_14) | i23=J_14))). % 22.93/10.41 tff(c_1607, plain, (![J_14]: (select(a_1082, J_14)=select(a_1081, J_14) | i14=J_14))). % 22.93/10.41 tff(c_1496, plain, (![J_14]: (select(a_1097, J_14)=select(a_1096, J_14) | i29=J_14))). % 22.93/10.41 tff(c_1508, plain, (![J_14]: (select(a_1087, J_14)=select(a_1086, J_14) | i19=J_14))). % 22.93/10.41 tff(c_1643, plain, (![J_14]: (select(a_1114, J_14)=select(a_1113, J_14) | i14=J_14))). % 22.93/10.41 tff(c_1619, plain, (![J_14]: (select(a_1121, J_14)=select(a_1120, J_14) | i12=J_14))). % 22.93/10.41 tff(c_1535, plain, (![J_14]: (select(a_1069, J_14)=select(a1, J_14) | i1=J_14))). % 22.93/10.41 tff(c_1520, plain, (![J_14]: (select(a_1079, J_14)=select(a_1078, J_14) | i11=J_14))). % 22.93/10.41 tff(c_1559, plain, (![J_14]: (select(a_1075, J_14)=select(a_1074, J_14) | i7=J_14))). % 22.93/10.41 tff(c_1556, plain, (![J_14]: (select(a_1071, J_14)=select(a_1070, J_14) | i3=J_14))). % 22.93/10.41 tff(c_1646, plain, (![J_14]: (select(a_1078, J_14)=select(a_1077, J_14) | i10=J_14))). % 22.93/10.41 tff(c_1577, plain, (![J_14]: (select(a_1107, J_14)=select(a_1106, J_14) | i25=J_14))). % 22.93/10.41 tff(c_1601, plain, (![J_14]: (select(a_1098, J_14)=select(a_1097, J_14) | i1=J_14))). % 22.93/10.41 tff(c_1541, plain, (![J_14]: (select(a_1077, J_14)=select(a_1076, J_14) | i9=J_14))). % 22.93/10.41 tff(c_1595, plain, (![J_14]: (select(a_1089, J_14)=select(a_1088, J_14) | i21=J_14))). % 22.93/10.42 tff(c_1571, plain, (![J_14]: (select(a_1122, J_14)=select(a_1121, J_14) | i16=J_14))). % 22.93/10.42 tff(c_1625, plain, (![J_14]: (select(a_1094, J_14)=select(a_1093, J_14) | i26=J_14))). % 22.93/10.42 tff(c_1270, plain, (select(a_1110, i8)=e8)). % 22.93/10.42 tff(c_1351, plain, (select(a_1074, i6)=e6)). % 22.93/10.42 tff(c_1282, plain, (select(a_1092, i24)=e24)). % 22.93/10.42 tff(c_1294, plain, (select(a_1102, i4)=e4)). % 22.93/10.42 tff(c_1324, plain, (select(a_1077, i9)=e9)). % 22.93/10.42 tff(c_1327, plain, (select(a_1117, i26)=e26)). % 22.93/10.42 tff(c_1393, plain, (select(a_1086, i18)=e18)). % 22.93/10.42 tff(c_1396, plain, (select(a_1124, i17)=e17)). % 22.93/10.42 tff(c_1330, plain, (select(a_1100, i1)=e1)). % 22.93/10.42 tff(c_1384, plain, (select(a_1098, i1)=e1)). % 22.93/10.42 tff(c_1354, plain, (select(a_1122, i16)=e16)). % 22.93/10.42 tff(c_1399, plain, (select(a_1123, i28)=e28)). % 22.93/10.42 tff(c_1291, plain, (select(a_1087, i19)=e19)). % 22.93/10.42 tff(c_1402, plain, (select(a_1121, i12)=e12)). % 22.93/10.42 tff(c_1276, plain, (select(a_1118, i22)=e22)). % 22.93/10.42 tff(c_1279, plain, (select(a_1097, i29)=e29)). % 22.93/10.42 tff(c_1297, plain, (select(a_1080, i12)=e12)). % 22.93/10.42 tff(c_1333, plain, (select(a_1120, i3)=e3)). % 22.93/10.42 tff(c_1387, plain, (select(a_1084, i16)=e16)). % 22.93/10.42 tff(c_1405, plain, (select(a_1093, i25)=e25)). % 22.93/10.42 tff(c_1408, plain, (select(a_1094, i26)=e26)). % 22.93/10.42 tff(c_1390, plain, (select(a_1082, i14)=e14)). % 22.93/10.42 tff(c_1375, plain, (select(a_1103, i9)=e9)). % 22.93/10.42 tff(c_1318, plain, (select(a_1069, i1)=e1)). % 22.93/10.42 tff(c_1381, plain, (select(a_1108, i18)=e18)). % 22.93/10.42 tff(c_1336, plain, (select(a_1115, i29)=e29)). % 22.93/10.42 tff(c_1321, plain, (select(a_1096, i28)=e28)). % 22.93/10.42 tff(c_1411, plain, (select(a_1070, i2)=e2)). % 22.93/10.42 tff(c_1414, plain, (select(a_1128, i10)=e10)). % 22.93/10.42 tff(c_1372, plain, (select(a_1073, i5)=e5)). % 22.93/10.42 tff(c_1378, plain, (select(a_1089, i21)=e21)). % 22.93/10.42 tff(c_1315, plain, (select(a_1126, i24)=e24)). % 22.93/10.42 tff(c_1288, plain, (select(a_1090, i22)=e22)). % 22.93/10.42 tff(c_1300, plain, (select(a_1109, i20)=e20)). % 22.93/10.42 tff(c_1366, plain, (select(a_1111, i21)=e21)). % 22.93/10.42 tff(c_1339, plain, (select(a_1071, i3)=e3)). % 22.93/10.42 tff(c_1417, plain, (select(a_1101, i19)=e19)). % 22.93/10.42 tff(c_1420, plain, (select(a_1104, i30)=e30)). % 22.93/10.42 tff(c_1369, plain, (select(a_1085, i17)=e17)). % 22.93/10.42 tff(c_1423, plain, (select(a_1095, i27)=e27)). % 22.93/10.42 tff(c_1426, plain, (select(a_1114, i14)=e14)). % 22.93/10.42 tff(c_1342, plain, (select(a_1075, i7)=e7)). % 22.93/10.42 tff(c_1312, plain, (select(a_1099, i13)=e13)). % 22.93/10.42 tff(c_1360, plain, (select(a_1107, i25)=e25)). % 22.93/10.42 tff(c_1357, plain, (select(a_1112, i6)=e6)). % 22.93/10.42 tff(c_1363, plain, (select(a_1088, i20)=e20)). % 22.93/10.42 tff(c_1306, plain, (select(a_1091, i23)=e23)). % 22.93/10.42 tff(c_1303, plain, (select(a_1079, i11)=e11)). % 22.93/10.42 tff(c_1345, plain, (select(a_1127, i7)=e7)). % 22.93/10.42 tff(c_1309, plain, (select(a_1105, i2)=e2)). % 22.93/10.42 tff(c_1348, plain, (select(a_1072, i4)=e4)). % 22.93/10.42 tff(c_1285, plain, (select(a_1125, i23)=e23)). % 22.93/10.42 tff(c_1273, plain, (select(a_1106, i15)=e15)). % 22.93/10.42 tff(c_1267, plain, (select(a_1116, i5)=e5)). % 22.93/10.42 tff(c_1429, plain, (select(a_1078, i10)=e10)). % 22.93/10.42 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))). % 22.93/10.42 tff(c_1432, plain, (select(a_1119, i27)=e27)). % 22.93/10.42 tff(c_1435, plain, (select(a_1076, i8)=e8)). % 22.93/10.42 tff(c_1438, plain, (select(a_1083, i15)=e15)). % 22.93/10.42 tff(c_1441, plain, (select(a_1081, i13)=e13)). % 22.93/10.42 tff(c_1264, plain, (select(a_1113, i11)=e11)). % 22.93/10.42 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 22.93/10.42 tff(c_94, plain, (store(a_1112, i11, e11)=a_1113)). % 22.93/10.42 tff(c_100, plain, (store(a_1115, i5, e5)=a_1116)). % 22.93/10.42 tff(c_88, plain, (store(a_1109, i8, e8)=a_1110)). % 22.93/10.42 tff(c_80, plain, (store(a_1105, i15, e15)=a_1106)). % 22.93/10.42 tff(c_104, plain, (store(a_1117, i22, e22)=a_1118)). % 22.93/10.42 tff(c_62, plain, (store(a_1096, i29, e29)=a_1097)). % 22.93/10.42 tff(c_52, plain, (store(a_1091, i24, e24)=a_1092)). % 22.93/10.42 tff(c_118, plain, (store(a_1124, i23, e23)=a_1125)). % 22.93/10.42 tff(c_48, plain, (store(a_1089, i22, e22)=a_1090)). % 22.93/10.42 tff(c_42, plain, (store(a_1086, i19, e19)=a_1087)). % 22.93/10.42 tff(c_72, plain, (store(a_1101, i4, e4)=a_1102)). % 22.93/10.42 tff(c_28, plain, (store(a_1079, i12, e12)=a_1080)). % 22.93/10.42 tff(c_86, plain, (store(a_1108, i20, e20)=a_1109)). % 22.93/10.42 tff(c_26, plain, (store(a_1078, i11, e11)=a_1079)). % 22.93/10.42 tff(c_50, plain, (store(a_1090, i23, e23)=a_1091)). % 22.93/10.42 tff(c_78, plain, (store(a_1104, i2, e2)=a_1105)). % 22.93/10.42 tff(c_66, plain, (store(a1, i13, e13)=a_1099)). % 22.93/10.42 tff(c_120, plain, (store(a_1125, i24, e24)=a_1126)). % 22.93/10.42 tff(c_6, plain, (store(a1, i1, e1)=a_1069)). % 22.93/10.42 tff(c_60, plain, (store(a_1095, i28, e28)=a_1096)). % 22.93/10.42 tff(c_22, plain, (store(a_1076, i9, e9)=a_1077)). % 22.93/10.42 tff(c_102, plain, (store(a_1116, i26, e26)=a_1117)). % 22.93/10.42 tff(c_68, plain, (store(a_1099, i1, e1)=a_1100)). % 22.93/10.42 tff(c_108, plain, (store(a_1119, i3, e3)=a_1120)). % 22.93/10.42 tff(c_98, plain, (store(a_1114, i29, e29)=a_1115)). % 22.93/10.42 tff(c_10, plain, (store(a_1070, i3, e3)=a_1071)). % 22.93/10.42 tff(c_18, plain, (store(a_1074, i7, e7)=a_1075)). % 22.93/10.42 tff(c_122, plain, (store(a_1126, i7, e7)=a_1127)). % 22.93/10.42 tff(c_12, plain, (store(a_1071, i4, e4)=a_1072)). % 22.93/10.42 tff(c_16, plain, (store(a_1073, i6, e6)=a_1074)). % 22.93/10.42 tff(c_112, plain, (store(a_1121, i16, e16)=a_1122)). % 22.93/10.42 tff(c_92, plain, (store(a_1111, i6, e6)=a_1112)). % 22.93/10.42 tff(c_82, plain, (store(a_1106, i25, e25)=a_1107)). % 22.93/10.42 tff(c_44, plain, (store(a_1087, i20, e20)=a_1088)). % 22.93/10.42 tff(c_90, plain, (store(a_1110, i21, e21)=a_1111)). % 22.93/10.42 tff(c_38, plain, (store(a_1084, i17, e17)=a_1085)). % 22.93/10.42 tff(c_14, plain, (store(a_1072, i5, e5)=a_1073)). % 22.93/10.42 tff(c_74, plain, (store(a_1102, i9, e9)=a_1103)). % 22.93/10.42 tff(c_46, plain, (store(a_1088, i21, e21)=a_1089)). % 22.93/10.42 tff(c_84, plain, (store(a_1107, i18, e18)=a_1108)). % 22.93/10.42 tff(c_64, plain, (store(a_1097, i1, e1)=a_1098)). % 22.93/10.42 tff(c_36, plain, (store(a_1083, i16, e16)=a_1084)). % 22.93/10.42 tff(c_32, plain, (store(a_1081, i14, e14)=a_1082)). % 22.93/10.42 tff(c_40, plain, (store(a_1085, i18, e18)=a_1086)). % 22.93/10.42 tff(c_116, plain, (store(a_1123, i17, e17)=a_1124)). % 22.93/10.42 tff(c_114, plain, (store(a_1122, i28, e28)=a_1123)). % 22.93/10.42 tff(c_110, plain, (store(a_1120, i12, e12)=a_1121)). % 22.93/10.42 tff(c_54, plain, (store(a_1092, i25, e25)=a_1093)). % 22.93/10.42 tff(c_56, plain, (store(a_1093, i26, e26)=a_1094)). % 22.93/10.42 tff(c_8, plain, (store(a_1069, i2, e2)=a_1070)). % 22.93/10.42 tff(c_124, plain, (store(a_1127, i10, e10)=a_1128)). % 22.93/10.42 tff(c_70, plain, (store(a_1100, i19, e19)=a_1101)). % 22.93/10.43 tff(c_76, plain, (store(a_1103, i30, e30)=a_1104)). % 22.93/10.43 tff(c_58, plain, (store(a_1094, i27, e27)=a_1095)). % 22.93/10.43 tff(c_96, plain, (store(a_1113, i14, e14)=a_1114)). % 22.93/10.43 tff(c_24, plain, (store(a_1077, i10, e10)=a_1078)). % 22.93/10.43 tff(c_106, plain, (store(a_1118, i27, e27)=a_1119)). % 22.93/10.43 tff(c_20, plain, (store(a_1075, i8, e8)=a_1076)). % 22.93/10.43 tff(c_34, plain, (store(a_1082, i15, e15)=a_1083)). % 22.93/10.43 tff(c_30, plain, (store(a_1080, i13, e13)=a_1081)). % 22.93/10.43 tff(c_860, plain, (i3!=i17)). % 22.93/10.43 tff(c_654, plain, (i7!=i22)). % 22.93/10.43 tff(c_974, plain, (i15!=i1)). % 22.93/10.43 tff(c_274, plain, (i25!=i18)). % 22.93/10.43 tff(c_786, plain, (i4!=i28)). % 22.93/10.43 tff(c_952, plain, (i26!=i1)). % 22.93/10.43 tff(c_780, plain, (i6!=i5)). % 22.93/10.43 tff(c_798, plain, (i4!=i22)). % 22.93/10.43 tff(c_682, plain, (i8!=i7)). % 22.93/10.43 tff(c_784, plain, (i4!=i29)). % 22.93/10.43 tff(c_502, plain, (i16!=i11)). % 22.93/10.43 tff(c_540, plain, (i16!=i10)). % 22.93/10.43 tff(c_176, plain, (i29!=i23)). % 22.93/10.43 tff(c_340, plain, (i17!=i16)). % 22.93/10.43 tff(c_662, plain, (i7!=i18)). % 22.93/10.43 tff(c_836, plain, (i3!=i29)). % 22.93/10.43 tff(c_198, plain, (i25!=i22)). % 22.93/10.43 tff(c_870, plain, (i3!=i12)). % 22.93/10.43 tff(c_164, plain, (i29!=i24)). % 22.93/10.43 tff(c_630, plain, (i8!=i12)). % 22.93/10.43 tff(c_156, plain, (i28!=i25)). % 22.93/10.43 tff(c_802, plain, (i4!=i20)). % 22.93/10.43 tff(c_522, plain, (i25!=i10)). % 22.93/10.43 tff(c_294, plain, (i27!=i17)). % 22.93/10.43 tff(c_226, plain, (i28!=i20)). % 22.93/10.43 tff(c_230, plain, (i26!=i20)). % 22.93/10.43 tff(c_338, plain, (i18!=i16)). % 22.93/10.43 tff(c_500, plain, (i17!=i11)). % 22.93/10.43 tff(c_898, plain, (i25!=i2)). % 22.93/10.43 tff(c_960, plain, (i22!=i1)). % 22.93/10.43 tff(c_690, plain, (i6!=i27)). % 22.93/10.43 tff(c_556, plain, (i9!=i28)). % 22.93/10.43 tff(c_418, plain, (i23!=i13)). % 22.93/10.43 tff(c_758, plain, (i5!=i17)). % 22.93/10.43 tff(c_888, plain, (i30!=i2)). % 22.93/10.43 tff(c_646, plain, (i7!=i26)). % 22.93/10.43 tff(c_580, plain, (i9!=i16)). % 22.93/10.43 tff(c_350, plain, (i26!=i15)). % 22.93/10.43 tff(c_258, plain, (i22!=i19)). % 22.93/10.43 tff(c_904, plain, (i22!=i2)). % 22.93/10.43 tff(c_872, plain, (i3!=i11)). % 22.93/10.43 tff(c_428, plain, (i18!=i13)). % 22.93/10.43 tff(c_288, plain, (i30!=i17)). % 22.93/10.43 tff(c_678, plain, (i7!=i10)). % 22.93/10.43 tff(c_290, plain, (i29!=i17)). % 22.93/10.43 tff(c_404, plain, (i30!=i13)). % 22.93/10.43 tff(c_426, plain, (i19!=i13)). % 22.93/10.43 tff(c_444, plain, (i27!=i12)). % 22.93/10.43 tff(c_842, plain, (i3!=i26)). % 22.93/10.43 tff(c_458, plain, (i20!=i12)). % 22.93/10.43 tff(c_266, plain, (i29!=i18)). % 22.93/10.43 tff(c_268, plain, (i28!=i18)). % 22.93/10.43 tff(c_416, plain, (i24!=i13)). % 22.93/10.43 tff(c_710, plain, (i6!=i17)). % 22.93/10.43 tff(c_282, plain, (i21!=i18)). % 22.93/10.43 tff(c_280, plain, (i22!=i18)). % 22.93/10.43 tff(c_160, plain, (i26!=i25)). % 22.93/10.43 tff(c_390, plain, (i21!=i14)). % 22.93/10.43 tff(c_938, plain, (i5!=i2)). % 22.93/10.43 tff(c_934, plain, (i7!=i2)). % 22.93/10.43 tff(c_304, plain, (i22!=i17)). % 22.93/10.43 tff(c_146, plain, (i29!=i26)). % 22.93/10.43 tff(c_584, plain, (i9!=i14)). % 22.93/10.43 tff(c_544, plain, (i14!=i10)). % 22.93/10.43 tff(c_496, plain, (i19!=i11)). % 22.93/10.43 tff(c_634, plain, (i8!=i10)). % 22.93/10.43 tff(c_694, plain, (i6!=i25)). % 22.93/10.43 tff(c_460, plain, (i19!=i12)). % 22.93/10.43 tff(c_602, plain, (i8!=i26)). % 22.93/10.43 tff(c_200, plain, (i24!=i22)). % 22.93/10.43 tff(c_986, plain, (i9!=i1)). % 22.93/10.43 tff(c_902, plain, (i23!=i2)). % 22.93/10.43 tff(c_638, plain, (i7!=i30)). % 22.93/10.43 tff(c_624, plain, (i8!=i15)). % 22.93/10.43 tff(c_704, plain, (i6!=i20)). % 22.93/10.43 tff(c_874, plain, (i3!=i10)). % 22.93/10.43 tff(c_162, plain, (i30!=i24)). % 22.93/10.43 tff(c_422, plain, (i21!=i13)). % 22.93/10.43 tff(c_808, plain, (i4!=i17)). % 22.93/10.43 tff(c_976, plain, (i14!=i1)). % 22.93/10.43 tff(c_256, plain, (i23!=i19)). % 22.93/10.43 tff(c_434, plain, (i15!=i13)). % 22.93/10.43 tff(c_272, plain, (i26!=i18)). % 22.93/10.43 tff(c_292, plain, (i28!=i17)). % 22.93/10.43 tff(c_220, plain, (i22!=i21)). % 22.93/10.43 tff(c_620, plain, (i8!=i17)). % 22.93/10.43 tff(c_530, plain, (i21!=i10)). % 22.93/10.43 tff(c_424, plain, (i20!=i13)). % 22.93/10.43 tff(c_774, plain, (i9!=i5)). % 22.93/10.43 tff(c_240, plain, (i21!=i20)). % 22.93/10.43 tff(c_658, plain, (i7!=i20)). % 22.93/10.43 tff(c_700, plain, (i6!=i22)). % 22.93/10.43 tff(c_328, plain, (i23!=i16)). % 22.93/10.43 tff(c_850, plain, (i3!=i22)). % 22.93/10.43 tff(c_554, plain, (i9!=i29)). % 22.93/10.43 tff(c_618, plain, (i8!=i18)). % 22.93/10.43 tff(c_754, plain, (i5!=i19)). % 22.93/10.43 tff(c_260, plain, (i21!=i19)). % 22.93/10.43 tff(c_284, plain, (i20!=i18)). % 22.93/10.43 tff(c_962, plain, (i21!=i1)). % 22.93/10.43 tff(c_804, plain, (i4!=i19)). % 22.93/10.43 tff(c_152, plain, (i30!=i25)). % 22.93/10.43 tff(c_778, plain, (i7!=i5)). % 22.93/10.43 tff(c_806, plain, (i4!=i18)). % 22.93/10.43 tff(c_674, plain, (i7!=i12)). % 22.93/10.43 tff(c_202, plain, (i23!=i22)). % 22.93/10.43 tff(c_196, plain, (i26!=i22)). % 22.93/10.43 tff(c_154, plain, (i29!=i25)). % 22.93/10.43 tff(c_374, plain, (i29!=i14)). % 22.93/10.43 tff(c_368, plain, (i17!=i15)). % 22.93/10.43 tff(c_660, plain, (i7!=i19)). % 22.93/10.43 tff(c_854, plain, (i3!=i20)). % 22.93/10.43 tff(c_546, plain, (i13!=i10)). % 22.93/10.43 tff(c_254, plain, (i24!=i19)). % 22.93/10.43 tff(c_332, plain, (i21!=i16)). % 22.93/10.43 tff(c_264, plain, (i30!=i18)). % 22.93/10.43 tff(c_548, plain, (i12!=i10)). % 22.93/10.43 tff(c_438, plain, (i30!=i12)). % 22.93/10.43 tff(c_382, plain, (i25!=i14)). % 22.93/10.43 tff(c_518, plain, (i27!=i10)). % 22.93/10.43 tff(c_172, plain, (i25!=i24)). % 22.93/10.43 tff(c_666, plain, (i7!=i16)). % 22.93/10.43 tff(c_838, plain, (i3!=i28)). % 22.93/10.43 tff(c_830, plain, (i6!=i4)). % 22.93/10.43 tff(c_398, plain, (i17!=i14)). % 22.93/10.43 tff(c_866, plain, (i3!=i14)). % 22.93/10.43 tff(c_616, plain, (i8!=i19)). % 22.93/10.43 tff(c_908, plain, (i20!=i2)). % 22.93/10.43 tff(c_132, plain, (i30!=i29)). % 22.93/10.43 tff(c_656, plain, (i7!=i21)). % 22.93/10.43 tff(c_796, plain, (i4!=i23)). % 22.93/10.43 tff(c_510, plain, (i12!=i11)). % 22.93/10.43 tff(c_964, plain, (i20!=i1)). % 22.93/10.43 tff(c_342, plain, (i30!=i15)). % 22.93/10.43 tff(c_598, plain, (i8!=i28)). % 22.93/10.43 tff(c_180, plain, (i27!=i23)). % 22.93/10.43 tff(c_298, plain, (i25!=i17)). % 22.93/10.44 tff(c_322, plain, (i26!=i16)). % 22.93/10.44 tff(c_402, plain, (i15!=i14)). % 22.93/10.44 tff(c_772, plain, (i5!=i10)). % 22.93/10.44 tff(c_920, plain, (i2!=i14)). % 22.93/10.44 tff(c_442, plain, (i28!=i12)). % 22.93/10.44 tff(c_192, plain, (i28!=i22)). % 22.93/10.44 tff(c_728, plain, (i8!=i6)). % 22.93/10.44 tff(c_730, plain, (i7!=i6)). % 22.93/10.44 tff(c_736, plain, (i5!=i28)). % 22.93/10.44 tff(c_440, plain, (i29!=i12)). % 22.93/10.44 tff(c_148, plain, (i28!=i26)). % 22.93/10.44 tff(c_252, plain, (i25!=i19)). % 22.93/10.44 tff(c_478, plain, (i28!=i11)). % 22.93/10.44 tff(c_664, plain, (i7!=i17)). % 22.93/10.44 tff(c_188, plain, (i30!=i22)). % 22.93/10.44 tff(c_412, plain, (i26!=i13)). % 22.93/10.44 tff(c_742, plain, (i5!=i25)). % 22.93/10.44 tff(c_312, plain, (i18!=i17)). % 22.93/10.44 tff(c_848, plain, (i3!=i23)). % 22.93/10.44 tff(c_684, plain, (i6!=i30)). % 22.93/10.44 tff(c_994, plain, (i5!=i1)). % 22.93/10.44 tff(c_910, plain, (i2!=i19)). % 22.93/10.44 tff(c_900, plain, (i24!=i2)). % 22.93/10.44 tff(c_468, plain, (i15!=i12)). % 22.93/10.44 tff(c_238, plain, (i22!=i20)). % 22.93/10.44 tff(c_942, plain, (i3!=i2)). % 22.93/10.44 tff(c_410, plain, (i27!=i13)). % 22.93/10.44 tff(c_954, plain, (i25!=i1)). % 22.93/10.44 tff(c_168, plain, (i27!=i24)). % 22.93/10.44 tff(c_950, plain, (i27!=i1)). % 22.93/10.44 tff(c_222, plain, (i30!=i20)). % 22.93/10.44 tff(c_720, plain, (i6!=i12)). % 22.93/10.44 tff(c_470, plain, (i14!=i12)). % 22.93/10.44 tff(c_358, plain, (i22!=i15)). % 22.93/10.44 tff(c_698, plain, (i6!=i23)). % 22.93/10.44 tff(c_454, plain, (i22!=i12)). % 22.93/10.44 tff(c_966, plain, (i19!=i1)). % 22.93/10.44 tff(c_856, plain, (i3!=i19)). % 22.93/10.44 tff(c_926, plain, (i2!=i11)). % 22.93/10.44 tff(c_242, plain, (i30!=i19)). % 22.93/10.44 tff(c_852, plain, (i3!=i21)). % 22.93/10.44 tff(c_310, plain, (i19!=i17)). % 22.93/10.44 tff(c_486, plain, (i24!=i11)). % 22.93/10.44 tff(c_432, plain, (i16!=i13)). % 22.93/10.44 tff(c_828, plain, (i7!=i4)). % 22.93/10.44 tff(c_550, plain, (i11!=i10)). % 22.93/10.44 tff(c_614, plain, (i8!=i20)). % 22.93/10.44 tff(c_820, plain, (i4!=i11)). % 22.93/10.44 tff(c_364, plain, (i19!=i15)). % 22.93/10.44 tff(c_832, plain, (i5!=i4)). % 22.93/10.44 tff(c_400, plain, (i16!=i14)). % 22.93/10.44 tff(c_276, plain, (i24!=i18)). % 22.93/10.44 tff(c_190, plain, (i29!=i22)). % 22.93/10.44 tff(c_370, plain, (i16!=i15)). % 22.93/10.44 tff(c_140, plain, (i29!=i27)). % 22.93/10.44 tff(c_752, plain, (i5!=i20)). % 22.93/10.44 tff(c_344, plain, (i29!=i15)). % 22.93/10.44 tff(c_248, plain, (i27!=i19)). % 22.93/10.44 tff(c_790, plain, (i4!=i26)). % 22.93/10.44 tff(c_984, plain, (i10!=i1)). % 22.93/10.44 tff(c_718, plain, (i6!=i13)). % 22.93/10.44 tff(c_578, plain, (i9!=i17)). % 22.93/10.44 tff(c_566, plain, (i9!=i23)). % 22.93/10.44 tff(c_446, plain, (i26!=i12)). % 22.93/10.44 tff(c_414, plain, (i25!=i13)). % 22.93/10.44 tff(c_408, plain, (i28!=i13)). % 22.93/10.44 tff(c_734, plain, (i5!=i29)). % 22.93/10.44 tff(c_592, plain, (i9!=i10)). % 22.93/10.44 tff(c_764, plain, (i5!=i14)). % 22.93/10.44 tff(c_680, plain, (i9!=i7)). % 22.93/10.44 tff(c_688, plain, (i6!=i28)). % 22.93/10.44 tff(c_738, plain, (i5!=i27)). % 22.93/10.44 tff(c_716, plain, (i6!=i14)). % 22.93/10.44 tff(c_858, plain, (i3!=i18)). % 22.93/10.44 tff(c_352, plain, (i25!=i15)). % 22.93/10.44 tff(c_296, plain, (i26!=i17)). % 22.93/10.44 tff(c_144, plain, (i30!=i26)). % 22.93/10.44 tff(c_396, plain, (i18!=i14)). % 22.93/10.44 tff(c_498, plain, (i18!=i11)). % 22.93/10.44 tff(c_948, plain, (i28!=i1)). % 22.93/10.44 tff(c_990, plain, (i7!=i1)). % 22.93/10.44 tff(c_762, plain, (i5!=i15)). % 22.93/10.44 tff(c_724, plain, (i6!=i10)). % 22.93/10.44 tff(c_936, plain, (i6!=i2)). % 22.93/10.44 tff(c_596, plain, (i8!=i29)). % 22.93/10.44 tff(c_826, plain, (i8!=i4)). % 22.93/10.44 tff(c_722, plain, (i6!=i11)). % 22.93/10.44 tff(c_320, plain, (i27!=i16)). % 22.93/10.44 tff(c_864, plain, (i3!=i15)). % 22.93/10.44 tff(c_512, plain, (i30!=i10)). % 22.93/10.44 tff(c_750, plain, (i5!=i21)). % 22.93/10.44 tff(c_306, plain, (i21!=i17)). % 22.93/10.44 tff(c_894, plain, (i27!=i2)). % 22.93/10.44 tff(c_760, plain, (i5!=i16)). % 22.93/10.44 tff(c_262, plain, (i20!=i19)). % 22.93/10.44 tff(c_708, plain, (i6!=i18)). % 22.93/10.44 tff(c_992, plain, (i6!=i1)). % 22.93/10.44 tff(c_930, plain, (i9!=i2)). % 22.93/10.44 tff(c_150, plain, (i27!=i26)). % 22.93/10.44 tff(c_648, plain, (i7!=i25)). % 22.93/10.44 tff(c_186, plain, (i24!=i23)). % 22.93/10.44 tff(c_918, plain, (i2!=i15)). % 22.93/10.44 tff(c_702, plain, (i6!=i21)). % 22.93/10.44 tff(c_782, plain, (i4!=i30)). % 22.93/10.44 tff(c_354, plain, (i24!=i15)). % 22.93/10.44 tff(c_882, plain, (i6!=i3)). % 22.93/10.44 tff(c_770, plain, (i5!=i11)). % 22.93/10.44 tff(c_336, plain, (i19!=i16)). % 22.93/10.44 tff(c_884, plain, (i5!=i3)). % 22.93/10.44 tff(c_552, plain, (i9!=i30)). % 22.93/10.44 tff(c_138, plain, (i30!=i27)). % 22.93/10.44 tff(c_636, plain, (i9!=i8)). % 22.93/10.44 tff(c_792, plain, (i4!=i25)). % 22.93/10.44 tff(c_250, plain, (i26!=i19)). % 22.93/10.44 tff(c_380, plain, (i26!=i14)). % 22.93/10.44 tff(c_334, plain, (i20!=i16)). % 22.93/10.44 tff(c_270, plain, (i27!=i18)). % 22.93/10.44 tff(c_946, plain, (i29!=i1)). % 22.93/10.44 tff(c_970, plain, (i17!=i1)). % 22.93/10.44 tff(c_184, plain, (i25!=i23)). % 22.93/10.44 tff(c_224, plain, (i29!=i20)). % 22.93/10.44 tff(c_696, plain, (i6!=i24)). % 22.93/10.44 tff(c_906, plain, (i21!=i2)). % 22.93/10.44 tff(c_968, plain, (i18!=i1)). % 22.93/10.44 tff(c_386, plain, (i23!=i14)). % 22.93/10.44 tff(c_676, plain, (i7!=i11)). % 22.93/10.44 tff(c_670, plain, (i7!=i14)). % 22.93/10.44 tff(c_594, plain, (i8!=i30)). % 22.93/10.44 tff(c_372, plain, (i30!=i14)). % 22.93/10.44 tff(c_462, plain, (i18!=i12)). % 22.93/10.44 tff(c_136, plain, (i29!=i28)). % 22.93/10.44 tff(c_640, plain, (i7!=i29)). % 22.93/10.44 tff(c_194, plain, (i27!=i22)). % 22.93/10.44 tff(c_608, plain, (i8!=i23)). % 22.93/10.44 tff(c_236, plain, (i23!=i20)). % 22.93/10.44 tff(c_472, plain, (i13!=i12)). % 22.93/10.44 tff(c_142, plain, (i28!=i27)). % 22.93/10.44 tff(c_576, plain, (i9!=i18)). % 22.93/10.44 tff(c_534, plain, (i19!=i10)). % 22.93/10.44 tff(c_466, plain, (i16!=i12)). % 22.93/10.44 tff(c_516, plain, (i28!=i10)). % 22.93/10.44 tff(c_912, plain, (i2!=i18)). % 22.93/10.44 tff(c_494, plain, (i20!=i11)). % 22.93/10.44 tff(c_158, plain, (i27!=i25)). % 22.93/10.44 tff(c_286, plain, (i19!=i18)). % 22.93/10.44 tff(c_560, plain, (i9!=i26)). % 22.93/10.44 tff(c_818, plain, (i4!=i12)). % 22.93/10.44 tff(c_574, plain, (i9!=i19)). % 22.93/10.44 tff(c_610, plain, (i8!=i22)). % 22.93/10.44 tff(c_588, plain, (i9!=i12)). % 22.93/10.44 tff(c_978, plain, (i13!=i1)). % 22.93/10.44 tff(c_590, plain, (i9!=i11)). % 22.93/10.44 tff(c_324, plain, (i25!=i16)). % 22.93/10.44 tff(c_514, plain, (i29!=i10)). % 22.93/10.44 tff(c_384, plain, (i24!=i14)). % 22.93/10.44 tff(c_406, plain, (i29!=i13)). % 22.93/10.44 tff(c_348, plain, (i27!=i15)). % 22.93/10.44 tff(c_890, plain, (i29!=i2)). % 22.93/10.44 tff(c_886, plain, (i4!=i3)). % 22.93/10.44 tff(c_800, plain, (i4!=i21)). % 22.93/10.44 tff(c_504, plain, (i15!=i11)). % 22.93/10.44 tff(c_604, plain, (i8!=i25)). % 22.93/10.44 tff(c_562, plain, (i9!=i25)). % 22.93/10.44 tff(c_862, plain, (i3!=i16)). % 22.93/10.44 tff(c_822, plain, (i4!=i10)). % 22.93/10.44 tff(c_914, plain, (i2!=i17)). % 22.93/10.44 tff(c_732, plain, (i5!=i30)). % 22.93/10.44 tff(c_606, plain, (i8!=i24)). % 22.93/10.44 tff(c_600, plain, (i8!=i27)). % 22.93/10.44 tff(c_644, plain, (i7!=i27)). % 22.93/10.44 tff(c_632, plain, (i8!=i11)). % 22.93/10.44 tff(c_776, plain, (i8!=i5)). % 22.93/10.44 tff(c_714, plain, (i6!=i15)). % 22.93/10.44 tff(c_812, plain, (i4!=i15)). % 22.93/10.44 tff(c_622, plain, (i8!=i16)). % 22.93/10.44 tff(c_318, plain, (i28!=i16)). % 22.93/10.44 tff(c_788, plain, (i4!=i27)). % 22.93/10.45 tff(c_706, plain, (i6!=i19)). % 22.93/10.45 tff(c_346, plain, (i28!=i15)). % 22.93/10.45 tff(c_278, plain, (i23!=i18)). % 22.93/10.45 tff(c_134, plain, (i30!=i28)). % 22.93/10.45 tff(c_366, plain, (i18!=i15)). % 22.93/10.45 tff(c_628, plain, (i8!=i13)). % 22.93/10.45 tff(c_508, plain, (i13!=i11)). % 22.93/10.45 tff(c_542, plain, (i15!=i10)). % 22.93/10.45 tff(c_944, plain, (i30!=i1)). % 22.93/10.45 tff(c_182, plain, (i26!=i23)). % 22.93/10.45 tff(c_174, plain, (i30!=i23)). % 22.93/10.45 tff(c_586, plain, (i9!=i13)). % 22.93/10.45 tff(c_314, plain, (i30!=i16)). % 22.93/10.45 tff(c_922, plain, (i2!=i13)). % 22.93/10.45 tff(c_572, plain, (i9!=i20)). % 22.93/10.45 tff(c_652, plain, (i7!=i23)). % 22.93/10.45 tff(c_536, plain, (i18!=i10)). % 22.93/10.45 tff(c_178, plain, (i28!=i23)). % 22.93/10.45 tff(c_650, plain, (i7!=i24)). % 22.93/10.45 tff(c_528, plain, (i22!=i10)). % 22.93/10.45 tff(c_420, plain, (i22!=i13)). % 22.93/10.45 tff(c_794, plain, (i4!=i24)). % 22.93/10.45 tff(c_300, plain, (i24!=i17)). % 22.93/10.45 tff(c_244, plain, (i29!=i19)). % 22.93/10.45 tff(c_330, plain, (i22!=i16)). % 22.93/10.45 tff(c_532, plain, (i20!=i10)). % 22.93/10.45 tff(c_316, plain, (i29!=i16)). % 22.93/10.45 tff(c_456, plain, (i21!=i12)). % 22.93/10.45 tff(c_208, plain, (i28!=i21)). % 22.93/10.45 tff(c_228, plain, (i27!=i20)). % 22.93/10.45 tff(c_302, plain, (i23!=i17)). % 22.93/10.45 tff(c_766, plain, (i5!=i13)). % 22.93/10.45 tff(c_880, plain, (i7!=i3)). % 22.93/10.45 tff(c_506, plain, (i14!=i11)). % 22.93/10.45 tff(c_430, plain, (i17!=i13)). % 22.93/10.45 tff(c_464, plain, (i17!=i12)). % 22.93/10.45 tff(c_642, plain, (i7!=i28)). % 22.93/10.45 tff(c_308, plain, (i20!=i17)). % 22.93/10.45 tff(c_612, plain, (i8!=i21)). % 22.93/10.45 tff(c_166, plain, (i28!=i24)). % 22.93/10.45 tff(c_204, plain, (i30!=i21)). % 22.93/10.45 tff(c_756, plain, (i5!=i18)). % 22.93/10.45 tff(c_214, plain, (i25!=i21)). % 22.93/10.45 tff(c_824, plain, (i9!=i4)). % 22.93/10.45 tff(c_524, plain, (i24!=i10)). % 22.93/10.45 tff(c_840, plain, (i3!=i27)). % 22.93/10.45 tff(c_212, plain, (i26!=i21)). % 22.93/10.45 tff(c_210, plain, (i27!=i21)). % 22.93/10.45 tff(c_726, plain, (i9!=i6)). % 22.93/10.45 tff(c_206, plain, (i29!=i21)). % 22.93/10.45 tff(c_878, plain, (i8!=i3)). % 22.93/10.45 tff(c_692, plain, (i6!=i26)). % 22.93/10.45 tff(c_520, plain, (i26!=i10)). % 22.93/10.45 tff(c_526, plain, (i23!=i10)). % 22.93/10.45 tff(c_558, plain, (i9!=i27)). % 22.93/10.45 tff(c_452, plain, (i23!=i12)). % 22.93/10.45 tff(c_378, plain, (i27!=i14)). % 22.93/10.45 tff(c_768, plain, (i5!=i12)). % 22.93/10.45 tff(c_360, plain, (i21!=i15)). % 22.93/10.45 tff(c_916, plain, (i2!=i16)). % 22.93/10.45 tff(c_868, plain, (i3!=i13)). % 22.93/10.45 tff(c_450, plain, (i24!=i12)). % 22.93/10.45 tff(c_218, plain, (i23!=i21)). % 22.93/10.45 tff(c_216, plain, (i24!=i21)). % 22.93/10.45 tff(c_326, plain, (i24!=i16)). % 22.93/10.45 tff(c_246, plain, (i28!=i19)). % 22.93/10.45 tff(c_982, plain, (i11!=i1)). % 22.93/10.45 tff(c_448, plain, (i25!=i12)). % 22.93/10.45 tff(c_376, plain, (i28!=i14)). % 22.93/10.45 tff(c_844, plain, (i3!=i25)). % 22.93/10.45 tff(c_932, plain, (i8!=i2)). % 22.93/10.45 tff(c_480, plain, (i27!=i11)). % 22.93/10.45 tff(c_924, plain, (i2!=i12)). % 22.93/10.45 tff(c_362, plain, (i20!=i15)). % 22.93/10.45 tff(c_436, plain, (i14!=i13)). % 22.93/10.45 tff(c_582, plain, (i9!=i15)). % 22.93/10.45 tff(c_816, plain, (i4!=i13)). % 22.93/10.45 tff(c_626, plain, (i8!=i14)). % 22.93/10.45 tff(c_712, plain, (i6!=i16)). % 22.93/10.45 tff(c_672, plain, (i7!=i13)). % 22.93/10.45 tff(c_834, plain, (i30!=i3)). % 22.93/10.45 tff(c_356, plain, (i23!=i15)). % 22.93/10.45 tff(c_668, plain, (i7!=i15)). % 22.93/10.45 tff(c_394, plain, (i19!=i14)). % 22.93/10.45 tff(c_564, plain, (i9!=i24)). % 22.93/10.45 tff(c_170, plain, (i26!=i24)). % 22.93/10.45 tff(c_846, plain, (i3!=i24)). % 22.93/10.45 tff(c_392, plain, (i20!=i14)). % 22.93/10.45 tff(c_232, plain, (i25!=i20)). % 22.93/10.45 tff(c_928, plain, (i2!=i10)). % 22.93/10.45 tff(c_568, plain, (i9!=i22)). % 22.93/10.45 tff(c_538, plain, (i17!=i10)). % 22.93/10.45 tff(c_474, plain, (i30!=i11)). % 22.93/10.45 tff(c_476, plain, (i29!=i11)). % 22.93/10.45 tff(c_740, plain, (i5!=i26)). % 22.93/10.45 tff(c_810, plain, (i4!=i16)). % 22.93/10.45 tff(c_814, plain, (i4!=i14)). % 22.93/10.45 tff(c_956, plain, (i24!=i1)). % 22.93/10.45 tff(c_896, plain, (i26!=i2)). % 22.93/10.45 tff(c_388, plain, (i22!=i14)). % 22.93/10.45 tff(c_570, plain, (i9!=i21)). % 22.93/10.45 tff(c_958, plain, (i23!=i1)). % 22.93/10.45 tff(c_482, plain, (i26!=i11)). % 22.93/10.45 tff(c_484, plain, (i25!=i11)). % 22.93/10.45 tff(c_744, plain, (i5!=i24)). % 22.93/10.45 tff(c_234, plain, (i24!=i20)). % 22.93/10.45 tff(c_686, plain, (i6!=i29)). % 22.93/10.45 tff(c_892, plain, (i28!=i2)). % 22.93/10.45 tff(c_488, plain, (i23!=i11)). % 22.93/10.45 tff(c_746, plain, (i5!=i23)). % 22.93/10.45 tff(c_490, plain, (i22!=i11)). % 22.93/10.45 tff(c_980, plain, (i12!=i1)). % 22.93/10.45 tff(c_492, plain, (i21!=i11)). % 22.93/10.45 tff(c_748, plain, (i5!=i22)). % 22.93/10.45 tff(c_876, plain, (i9!=i3)). % 22.93/10.45 tff(c_998, plain, (i3!=i1)). % 22.93/10.45 tff(c_940, plain, (i4!=i2)). % 22.93/10.45 tff(c_972, plain, (i16!=i1)). % 22.93/10.45 tff(c_988, plain, (i8!=i1)). % 22.93/10.45 tff(c_996, plain, (i4!=i1)). % 22.93/10.45 tff(c_1000, plain, (i2!=i1)). % 22.93/10.45 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.93/10.45 %------------------------------------------------------------------------------