%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV508-1.030 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n006.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:56 PM UTC 2025 % Result : Satisfiable 6.54s 2.61s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SWV508-1.030 : TPTP v9.0.0. Released v4.0.0. % 0.04/0.14 % 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.15/0.35 % Computer : n006.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Wed Apr 9 03:39:52 EDT 2025 % 0.15/0.35 % CPUTime : % 6.54/2.61 % 6.54/2.61 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.54/2.61 % 6.54/2.61 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.54/2.62 %$ store > sk > select > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n30 > n3 > n29 > n28 > n27 > n26 > n25 > n24 > n23 > n22 > n21 > n20 > n2 > n19 > n18 > n17 > n16 > n15 > n14 > n13 > n12 > n11 > n10 > n1 > i_1129 > 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 % 6.54/2.62 % 6.54/2.62 %Foreground sorts: % 6.54/2.62 % 6.54/2.62 % 6.54/2.62 %Background operators: % 6.54/2.62 % 6.54/2.62 % 6.54/2.62 %Foreground operators: % 6.54/2.62 tff(e29, type, e29: $i). % 6.54/2.62 tff(a_1096, type, a_1096: $i). % 6.54/2.62 tff(a1, type, a1: $i). % 6.54/2.62 tff(n22, type, n22: $i). % 6.54/2.62 tff(n27, type, n27: $i). % 6.54/2.62 tff(n16, type, n16: $i). % 6.54/2.62 tff(n12, type, n12: $i). % 6.54/2.62 tff(e1, type, e1: $i). % 6.54/2.62 tff(a_1092, type, a_1092: $i). % 6.54/2.62 tff(e8, type, e8: $i). % 6.54/2.62 tff(e_1130, type, e_1130: $i). % 6.54/2.62 tff(a_1094, type, a_1094: $i). % 6.54/2.62 tff(a_1089, type, a_1089: $i). % 6.54/2.62 tff(a_1116, type, a_1116: $i). % 6.54/2.62 tff(e21, type, e21: $i). % 6.54/2.62 tff(a_1107, type, a_1107: $i). % 6.54/2.62 tff(n24, type, n24: $i). % 6.54/2.62 tff(a_1109, type, a_1109: $i). % 6.54/2.62 tff(a_1100, type, a_1100: $i). % 6.54/2.62 tff(a_1084, type, a_1084: $i). % 6.54/2.62 tff(a_1074, type, a_1074: $i). % 6.54/2.62 tff(e15, type, e15: $i). % 6.54/2.62 tff(a_1087, type, a_1087: $i). % 6.54/2.62 tff(a_1103, type, a_1103: $i). % 6.54/2.62 tff(a_1108, type, a_1108: $i). % 6.54/2.62 tff(e18, type, e18: $i). % 6.54/2.62 tff(a_1101, type, a_1101: $i). % 6.54/2.62 tff(e24, type, e24: $i). % 6.54/2.62 tff(a_1105, type, a_1105: $i). % 6.54/2.62 tff(a_1085, type, a_1085: $i). % 6.54/2.62 tff(a_1121, type, a_1121: $i). % 6.54/2.62 tff(a_1102, type, a_1102: $i). % 6.54/2.62 tff(store, type, store: ($i * $i * $i) > $i). % 6.54/2.62 tff(n23, type, n23: $i). % 6.54/2.62 tff(n8, type, n8: $i). % 6.54/2.62 tff(a_1070, type, a_1070: $i). % 6.54/2.62 tff(a_1111, type, a_1111: $i). % 6.54/2.62 tff(e20, type, e20: $i). % 6.54/2.62 tff(e19, type, e19: $i). % 6.54/2.62 tff(e16, type, e16: $i). % 6.54/2.62 tff(n30, type, n30: $i). % 6.54/2.62 tff(e2, type, e2: $i). % 6.54/2.62 tff(a_1120, type, a_1120: $i). % 6.54/2.62 tff(n28, type, n28: $i). % 6.54/2.62 tff(a_1099, type, a_1099: $i). % 6.54/2.62 tff(n9, type, n9: $i). % 6.54/2.62 tff(a_1072, type, a_1072: $i). % 6.54/2.62 tff(a_1110, type, a_1110: $i). % 6.54/2.62 tff(e13, type, e13: $i). % 6.54/2.62 tff(n3, type, n3: $i). % 6.54/2.62 tff(a_1081, type, a_1081: $i). % 6.54/2.62 tff(e22, type, e22: $i). % 6.54/2.62 tff(n1, type, n1: $i). % 6.54/2.62 tff(a_1104, type, a_1104: $i). % 6.54/2.62 tff(n29, type, n29: $i). % 6.54/2.62 tff(e9, type, e9: $i). % 6.54/2.62 tff(a_1090, type, a_1090: $i). % 6.54/2.62 tff(a_1126, type, a_1126: $i). % 6.54/2.62 tff(a_1091, type, a_1091: $i). % 6.54/2.62 tff(a_1077, type, a_1077: $i). % 6.54/2.62 tff(n7, type, n7: $i). % 6.54/2.62 tff(e25, type, e25: $i). % 6.54/2.62 tff(e26, type, e26: $i). % 6.54/2.62 tff(n6, type, n6: $i). % 6.54/2.62 tff(e_1131, type, e_1131: $i). % 6.54/2.62 tff(e17, type, e17: $i). % 6.54/2.62 tff(n26, type, n26: $i). % 6.54/2.62 tff(e27, type, e27: $i). % 6.54/2.62 tff(a_1127, type, a_1127: $i). % 6.54/2.62 tff(e10, type, e10: $i). % 6.54/2.62 tff(e7, type, e7: $i). % 6.54/2.62 tff(a_1098, type, a_1098: $i). % 6.54/2.62 tff(a_1095, type, a_1095: $i). % 6.54/2.62 tff(n13, type, n13: $i). % 6.54/2.62 tff(sk, type, sk: ($i * $i) > $i). % 6.54/2.62 tff(n4, type, n4: $i). % 6.54/2.62 tff(a_1075, type, a_1075: $i). % 6.54/2.62 tff(n10, type, n10: $i). % 6.54/2.62 tff(a_1069, type, a_1069: $i). % 6.54/2.62 tff(a_1113, type, a_1113: $i). % 6.54/2.62 tff(n14, type, n14: $i). % 6.54/2.62 tff(a_1071, type, a_1071: $i). % 6.54/2.62 tff(n15, type, n15: $i). % 6.54/2.62 tff(n17, type, n17: $i). % 6.54/2.62 tff(e30, type, e30: $i). % 6.54/2.62 tff(select, type, select: ($i * $i) > $i). % 6.54/2.62 tff(a_1097, type, a_1097: $i). % 6.54/2.62 tff(a_1122, type, a_1122: $i). % 6.54/2.62 tff(a_1125, type, a_1125: $i). % 6.54/2.62 tff(a_1093, type, a_1093: $i). % 6.54/2.62 tff(a_1112, type, a_1112: $i). % 6.54/2.62 tff(a_1114, type, a_1114: $i). % 6.54/2.62 tff(n20, type, n20: $i). % 6.54/2.62 tff(e23, type, e23: $i). % 6.54/2.62 tff(n18, type, n18: $i). % 6.54/2.62 tff(a_1118, type, a_1118: $i). % 6.54/2.62 tff(e14, type, e14: $i). % 6.54/2.62 tff(a_1115, type, a_1115: $i). % 6.54/2.62 tff(n11, type, n11: $i). % 6.54/2.62 tff(a_1086, type, a_1086: $i). % 6.54/2.62 tff(e12, type, e12: $i). % 6.54/2.62 tff(e4, type, e4: $i). % 6.54/2.62 tff(a_1083, type, a_1083: $i). % 6.54/2.62 tff(a_1076, type, a_1076: $i). % 6.54/2.62 tff(a_1106, type, a_1106: $i). % 6.54/2.62 tff(a_1123, type, a_1123: $i). % 6.54/2.62 tff(a_1119, type, a_1119: $i). % 6.54/2.62 tff(a_1124, type, a_1124: $i). % 6.54/2.62 tff(e6, type, e6: $i). % 6.54/2.62 tff(i_1129, type, i_1129: $i). % 6.54/2.62 tff(n19, type, n19: $i). % 6.54/2.62 tff(n2, type, n2: $i). % 6.54/2.62 tff(e11, type, e11: $i). % 6.54/2.62 tff(a_1082, type, a_1082: $i). % 6.54/2.62 tff(e28, type, e28: $i). % 6.54/2.62 tff(n5, type, n5: $i). % 6.54/2.62 tff(a_1079, type, a_1079: $i). % 6.54/2.62 tff(e3, type, e3: $i). % 6.54/2.62 tff(a_1073, type, a_1073: $i). % 6.54/2.62 tff(a_1080, type, a_1080: $i). % 6.54/2.62 tff(n25, type, n25: $i). % 6.54/2.62 tff(e5, type, e5: $i). % 6.54/2.62 tff(a_1088, type, a_1088: $i). % 6.54/2.62 tff(a_1117, type, a_1117: $i). % 6.54/2.62 tff(a_1078, type, a_1078: $i). % 6.54/2.62 tff(n21, type, n21: $i). % 6.54/2.62 tff(a_1128, type, a_1128: $i). % 6.54/2.62 % 6.54/2.62 %Saturated clause set: % 6.54/2.62 tff(c_2095, plain, (![J_14]: (select(a_1100, J_14)=select(a_1099, J_14) | i_1129=J_14))). % 6.54/2.62 tff(c_2094, plain, (![J_14]: (select(a_1098, J_14)=select(a_1097, J_14) | i_1129=J_14))). % 6.54/2.62 tff(c_2139, plain, (![J_5]: (select(a_1069, J_5)=select(a1, J_5) | i_1129=J_5))). % 6.54/2.62 tff(c_1921, plain, (![J_14]: (select(a_1128, J_14)=select(a_1127, J_14) | i_1129=J_14))). % 6.54/2.62 tff(c_1922, plain, (![J_14]: (select(a_1078, J_14)=select(a_1077, J_14) | i_1129=J_14))). % 6.54/2.62 tff(c_2101, plain, (store(a_1099, i_1129, e1)=a_1100)). % 6.54/2.62 tff(c_2102, plain, (store(a1, i_1129, e1)=a_1069)). % 6.54/2.62 tff(c_2130, plain, (e10!=e1)). % 6.54/2.62 tff(c_2125, plain, (e_1130=e1)). % 6.87/2.62 tff(c_2099, plain, (select(a_1098, i_1129)=e1)). % 6.87/2.62 tff(c_2100, plain, (store(a_1097, i_1129, e1)=a_1098)). % 6.87/2.62 tff(c_2098, plain, (select(a_1100, i_1129)=e1)). % 6.87/2.62 tff(c_2097, plain, (select(a_1069, i_1129)=e1)). % 6.87/2.62 tff(c_2076, plain, (n1=i_1129)). % 6.87/2.62 tff(c_687, plain, (![J_14]: (select(a_1091, J_14)=select(a_1090, J_14) | n23=J_14))). % 6.87/2.62 tff(c_756, plain, (![J_14]: (select(a_1073, J_14)=select(a_1072, J_14) | n5=J_14))). % 6.87/2.62 tff(c_672, plain, (![J_14]: (select(a_1109, J_14)=select(a_1108, J_14) | n20=J_14))). % 6.87/2.62 tff(c_666, plain, (![J_14]: (select(a_1115, J_14)=select(a_1114, J_14) | n29=J_14))). % 6.87/2.62 tff(c_696, plain, (![J_14]: (select(a_1089, J_14)=select(a_1088, J_14) | n21=J_14))). % 6.87/2.62 tff(c_1926, plain, (store(a_1127, i_1129, e10)=a_1128)). % 6.87/2.62 tff(c_1925, plain, (store(a_1077, i_1129, e10)=a_1078)). % 6.87/2.62 tff(c_651, plain, (![J_14]: (select(a_1101, J_14)=select(a_1100, J_14) | n19=J_14))). % 6.87/2.62 tff(c_1935, plain, (e_1131=e10)). % 6.87/2.62 tff(c_1924, plain, (select(a_1128, i_1129)=e10)). % 6.87/2.62 tff(c_1923, plain, (select(a_1078, i_1129)=e10)). % 6.87/2.62 tff(c_1920, plain, (n10=i_1129)). % 6.87/2.62 tff(c_678, plain, (![J_14]: (select(a_1111, J_14)=select(a_1110, J_14) | n21=J_14))). % 6.87/2.62 tff(c_702, plain, (![J_14]: (select(a_1123, J_14)=select(a_1122, J_14) | n28=J_14))). % 6.87/2.62 tff(c_633, plain, (![J_14]: (select(a_1106, J_14)=select(a_1105, J_14) | n15=J_14))). % 6.87/2.62 tff(c_684, plain, (![J_14]: (select(a_1092, J_14)=select(a_1091, J_14) | n24=J_14))). % 6.87/2.62 tff(c_717, plain, (![J_14]: (select(a_1083, J_14)=select(a_1082, J_14) | n15=J_14))). % 6.87/2.62 tff(c_657, plain, (![J_14]: (select(a_1117, J_14)=select(a_1116, J_14) | n26=J_14))). % 6.87/2.62 tff(c_660, plain, (![J_14]: (select(a_1120, J_14)=select(a_1119, J_14) | n3=J_14))). % 6.87/2.62 tff(c_645, plain, (![J_14]: (select(a_1103, J_14)=select(a_1102, J_14) | n9=J_14))). % 6.87/2.63 tff(c_708, plain, (![J_14]: (select(a_1086, J_14)=select(a_1085, J_14) | n18=J_14))). % 6.87/2.63 tff(c_636, plain, (![J_14]: (select(a_1105, J_14)=select(a_1104, J_14) | n2=J_14))). % 6.87/2.63 tff(c_726, plain, (![J_14]: (select(a_1081, J_14)=select(a_1080, J_14) | n13=J_14))). % 6.87/2.63 tff(c_669, plain, (![J_14]: (select(a_1114, J_14)=select(a_1113, J_14) | n14=J_14))). % 6.87/2.63 tff(c_597, plain, (![J_14]: (select(a_1097, J_14)=select(a_1096, J_14) | n29=J_14))). % 6.87/2.63 tff(c_729, plain, (![J_14]: (select(a_1080, J_14)=select(a_1079, J_14) | n12=J_14))). % 6.87/2.63 tff(c_693, plain, (![J_14]: (select(a_1090, J_14)=select(a_1089, J_14) | n22=J_14))). % 6.87/2.63 tff(c_699, plain, (![J_14]: (select(a_1088, J_14)=select(a_1087, J_14) | n20=J_14))). % 6.87/2.63 tff(c_648, plain, (![J_14]: (select(a_1102, J_14)=select(a_1101, J_14) | n4=J_14))). % 6.87/2.63 tff(c_750, plain, (![J_14]: (select(a_1121, J_14)=select(a_1120, J_14) | n12=J_14))). % 6.87/2.63 tff(c_768, plain, (![J_14]: (select(a_1070, J_14)=select(a_1069, J_14) | n2=J_14))). % 6.87/2.63 tff(c_663, plain, (![J_14]: (select(a_1116, J_14)=select(a_1115, J_14) | n5=J_14))). % 6.87/2.63 tff(c_714, plain, (![J_14]: (select(a_1084, J_14)=select(a_1083, J_14) | n16=J_14))). % 6.87/2.63 tff(c_723, plain, (![J_14]: (select(a_1082, J_14)=select(a_1081, J_14) | n14=J_14))). % 6.87/2.63 tff(c_690, plain, (![J_14]: (select(a_1122, J_14)=select(a_1121, J_14) | n16=J_14))). % 6.87/2.63 tff(c_618, plain, (![J_14]: (select(a_1112, J_14)=select(a_1111, J_14) | n6=J_14))). % 6.87/2.63 tff(c_624, plain, (![J_14]: (select(a_1085, J_14)=select(a_1084, J_14) | n17=J_14))). % 6.87/2.63 tff(c_720, plain, (![J_14]: (select(a_1124, J_14)=select(a_1123, J_14) | n17=J_14))). % 6.87/2.63 tff(c_765, plain, (![J_14]: (select(a_1071, J_14)=select(a_1070, J_14) | n3=J_14))). % 6.87/2.63 tff(c_735, plain, (![J_14]: (select(a_1079, J_14)=select(a_1078, J_14) | n11=J_14))). % 6.87/2.63 tff(c_732, plain, (![J_14]: (select(a_1126, J_14)=select(a_1125, J_14) | n24=J_14))). % 6.87/2.63 tff(c_642, plain, (![J_14]: (select(a_1119, J_14)=select(a_1118, J_14) | n27=J_14))). % 6.87/2.63 tff(c_747, plain, (![J_14]: (select(a_1075, J_14)=select(a_1074, J_14) | n7=J_14))). % 6.87/2.63 tff(c_606, plain, (![J_14]: (select(a_1108, J_14)=select(a_1107, J_14) | n18=J_14))). % 6.87/2.63 tff(c_609, plain, (![J_14]: (select(a_1095, J_14)=select(a_1094, J_14) | n27=J_14))). % 6.87/2.63 tff(c_591, plain, (![J_14]: (select(a_1127, J_14)=select(a_1126, J_14) | n7=J_14))). % 6.87/2.63 tff(c_744, plain, (![J_14]: (select(a_1076, J_14)=select(a_1075, J_14) | n8=J_14))). % 6.87/2.63 tff(c_603, plain, (![J_14]: (select(a_1096, J_14)=select(a_1095, J_14) | n28=J_14))). % 6.87/2.63 tff(c_753, plain, (![J_14]: (select(a_1074, J_14)=select(a_1073, J_14) | n6=J_14))). % 6.87/2.63 tff(c_615, plain, (![J_14]: (select(a_1094, J_14)=select(a_1093, J_14) | n26=J_14))). % 6.87/2.63 tff(c_711, plain, (![J_14]: (select(a_1125, J_14)=select(a_1124, J_14) | n23=J_14))). % 6.87/2.63 tff(c_630, plain, (![J_14]: (select(a_1118, J_14)=select(a_1117, J_14) | n22=J_14))). % 6.87/2.63 tff(c_681, plain, (![J_14]: (select(a_1093, J_14)=select(a_1092, J_14) | n25=J_14))). % 6.87/2.63 tff(c_621, plain, (![J_14]: (select(a_1110, J_14)=select(a_1109, J_14) | n8=J_14))). % 6.87/2.63 tff(c_600, plain, (![J_14]: (select(a_1099, J_14)=select(a1, J_14) | n13=J_14))). % 6.87/2.63 tff(c_705, plain, (![J_14]: (select(a_1087, J_14)=select(a_1086, J_14) | n19=J_14))). % 6.87/2.63 tff(c_741, plain, (![J_14]: (select(a_1077, J_14)=select(a_1076, J_14) | n9=J_14))). % 6.87/2.63 tff(c_627, plain, (![J_14]: (select(a_1107, J_14)=select(a_1106, J_14) | n25=J_14))). % 6.87/2.63 tff(c_759, plain, (![J_14]: (select(a_1072, J_14)=select(a_1071, J_14) | n4=J_14))). % 6.87/2.63 tff(c_675, plain, (![J_14]: (select(a_1113, J_14)=select(a_1112, J_14) | n11=J_14))). % 6.87/2.63 tff(c_639, plain, (![J_14]: (select(a_1104, J_14)=select(a_1103, J_14) | n30=J_14))). % 6.87/2.63 tff(c_481, plain, (select(a_1111, n21)=e21)). % 6.87/2.63 tff(c_571, plain, (select(a_1070, n2)=e2)). % 6.87/2.63 tff(c_400, plain, (select(a_1097, n29)=e29)). % 6.87/2.63 tff(c_526, plain, (select(a_1082, n14)=e14)). % 6.87/2.63 tff(c_529, plain, (select(a_1081, n13)=e13)). % 6.87/2.63 tff(c_463, plain, (select(a_1120, n3)=e3)). % 6.87/2.63 tff(c_454, plain, (select(a_1101, n19)=e19)). % 6.87/2.63 tff(c_484, plain, (select(a_1093, n25)=e25)). % 6.87/2.63 tff(c_466, plain, (select(a_1116, n5)=e5)). % 6.87/2.63 tff(c_532, plain, (select(a_1080, n12)=e12)). % 6.87/2.63 tff(c_409, plain, (select(a_1108, n18)=e18)). % 6.87/2.63 tff(c_427, plain, (select(a_1085, n17)=e17)). % 6.87/2.63 tff(c_460, plain, (select(a_1117, n26)=e26)). % 6.87/2.63 tff(c_520, plain, (select(a_1083, n15)=e15)). % 6.87/2.63 tff(c_535, plain, (select(a_1126, n24)=e24)). % 6.87/2.63 tff(c_451, plain, (select(a_1102, n4)=e4)). % 6.87/2.63 tff(c_523, plain, (select(a_1124, n17)=e17)). % 6.87/2.63 tff(c_424, plain, (select(a_1110, n8)=e8)). % 6.87/2.63 tff(c_538, plain, (select(a_1079, n11)=e11)). % 6.87/2.63 tff(c_517, plain, (select(a_1084, n16)=e16)). % 6.87/2.63 tff(c_514, plain, (select(a_1125, n23)=e23)). % 6.87/2.63 tff(c_544, plain, (select(a_1077, n9)=e9)). % 6.87/2.63 tff(c_511, plain, (select(a_1086, n18)=e18)). % 6.87/2.63 tff(c_421, plain, (select(a_1112, n6)=e6)). % 6.87/2.63 tff(c_508, plain, (select(a_1087, n19)=e19)). % 6.87/2.63 tff(c_505, plain, (select(a_1123, n28)=e28)). % 6.87/2.63 tff(c_430, plain, (select(a_1107, n25)=e25)). % 6.87/2.63 tff(c_499, plain, (select(a_1089, n21)=e21)). % 6.87/2.63 tff(c_469, plain, (select(a_1115, n29)=e29)). % 6.87/2.63 tff(c_547, plain, (select(a_1076, n8)=e8)). % 6.87/2.63 tff(c_550, plain, (select(a_1075, n7)=e7)). % 6.87/2.63 tff(c_448, plain, (select(a_1103, n9)=e9)). % 6.87/2.63 tff(c_406, plain, (select(a_1096, n28)=e28)). % 6.87/2.63 tff(c_553, plain, (select(a_1121, n12)=e12)). % 6.87/2.63 tff(c_472, plain, (select(a_1114, n14)=e14)). % 6.87/2.63 tff(c_418, plain, (select(a_1094, n26)=e26)). % 6.87/2.63 tff(c_493, plain, (select(a_1122, n16)=e16)). % 6.87/2.63 tff(c_436, plain, (select(a_1106, n15)=e15)). % 6.87/2.63 tff(c_556, plain, (select(a_1074, n6)=e6)). % 6.87/2.63 tff(c_445, plain, (select(a_1119, n27)=e27)). % 6.87/2.64 tff(c_502, plain, (select(a_1088, n20)=e20)). % 6.87/2.64 tff(c_433, plain, (select(a_1118, n22)=e22)). % 6.87/2.64 tff(c_475, plain, (select(a_1109, n20)=e20)). % 6.87/2.64 tff(c_496, plain, (select(a_1090, n22)=e22)). % 6.87/2.64 tff(c_442, plain, (select(a_1104, n30)=e30)). % 6.87/2.64 tff(c_490, plain, (select(a_1091, n23)=e23)). % 6.87/2.64 tff(c_487, plain, (select(a_1092, n24)=e24)). % 6.87/2.64 tff(c_439, plain, (select(a_1105, n2)=e2)). % 6.87/2.64 tff(c_559, plain, (select(a_1073, n5)=e5)). % 6.87/2.64 tff(c_562, plain, (select(a_1072, n4)=e4)). % 6.87/2.64 tff(c_478, plain, (select(a_1113, n11)=e11)). % 6.87/2.64 tff(c_568, plain, (select(a_1071, n3)=e3)). % 6.87/2.64 tff(c_412, plain, (select(a_1095, n27)=e27)). % 6.87/2.64 tff(c_403, plain, (select(a_1099, n13)=e13)). % 6.87/2.64 tff(c_394, plain, (select(a_1127, n7)=e7)). % 6.87/2.64 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))). % 6.87/2.64 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 6.87/2.64 tff(c_122, plain, (store(a_1126, n7, e7)=a_1127)). % 6.87/2.64 tff(c_62, plain, (store(a_1096, n29, e29)=a_1097)). % 6.87/2.64 tff(c_66, plain, (store(a1, n13, e13)=a_1099)). % 6.87/2.64 tff(c_60, plain, (store(a_1095, n28, e28)=a_1096)). % 6.87/2.64 tff(c_84, plain, (store(a_1107, n18, e18)=a_1108)). % 6.87/2.64 tff(c_58, plain, (store(a_1094, n27, e27)=a_1095)). % 6.87/2.64 tff(c_56, plain, (store(a_1093, n26, e26)=a_1094)). % 6.87/2.64 tff(c_92, plain, (store(a_1111, n6, e6)=a_1112)). % 6.87/2.64 tff(c_88, plain, (store(a_1109, n8, e8)=a_1110)). % 6.87/2.64 tff(c_38, plain, (store(a_1084, n17, e17)=a_1085)). % 6.87/2.64 tff(c_82, plain, (store(a_1106, n25, e25)=a_1107)). % 6.87/2.64 tff(c_104, plain, (store(a_1117, n22, e22)=a_1118)). % 6.87/2.64 tff(c_80, plain, (store(a_1105, n15, e15)=a_1106)). % 6.87/2.64 tff(c_78, plain, (store(a_1104, n2, e2)=a_1105)). % 6.87/2.64 tff(c_76, plain, (store(a_1103, n30, e30)=a_1104)). % 6.87/2.64 tff(c_106, plain, (store(a_1118, n27, e27)=a_1119)). % 6.87/2.64 tff(c_74, plain, (store(a_1102, n9, e9)=a_1103)). % 6.87/2.64 tff(c_72, plain, (store(a_1101, n4, e4)=a_1102)). % 6.87/2.64 tff(c_70, plain, (store(a_1100, n19, e19)=a_1101)). % 6.87/2.64 tff(c_102, plain, (store(a_1116, n26, e26)=a_1117)). % 6.87/2.64 tff(c_108, plain, (store(a_1119, n3, e3)=a_1120)). % 6.87/2.64 tff(c_100, plain, (store(a_1115, n5, e5)=a_1116)). % 6.87/2.64 tff(c_98, plain, (store(a_1114, n29, e29)=a_1115)). % 6.87/2.64 tff(c_96, plain, (store(a_1113, n14, e14)=a_1114)). % 6.87/2.64 tff(c_86, plain, (store(a_1108, n20, e20)=a_1109)). % 6.87/2.64 tff(c_94, plain, (store(a_1112, n11, e11)=a_1113)). % 6.87/2.64 tff(c_90, plain, (store(a_1110, n21, e21)=a_1111)). % 6.87/2.64 tff(c_54, plain, (store(a_1092, n25, e25)=a_1093)). % 6.87/2.64 tff(c_52, plain, (store(a_1091, n24, e24)=a_1092)). % 6.87/2.64 tff(c_50, plain, (store(a_1090, n23, e23)=a_1091)). % 6.87/2.64 tff(c_112, plain, (store(a_1121, n16, e16)=a_1122)). % 6.87/2.64 tff(c_48, plain, (store(a_1089, n22, e22)=a_1090)). % 6.87/2.64 tff(c_46, plain, (store(a_1088, n21, e21)=a_1089)). % 6.87/2.64 tff(c_44, plain, (store(a_1087, n20, e20)=a_1088)). % 6.87/2.64 tff(c_114, plain, (store(a_1122, n28, e28)=a_1123)). % 6.87/2.64 tff(c_42, plain, (store(a_1086, n19, e19)=a_1087)). % 6.87/2.64 tff(c_40, plain, (store(a_1085, n18, e18)=a_1086)). % 6.87/2.64 tff(c_118, plain, (store(a_1124, n23, e23)=a_1125)). % 6.87/2.64 tff(c_36, plain, (store(a_1083, n16, e16)=a_1084)). % 6.87/2.64 tff(c_34, plain, (store(a_1082, n15, e15)=a_1083)). % 6.87/2.64 tff(c_116, plain, (store(a_1123, n17, e17)=a_1124)). % 6.87/2.64 tff(c_32, plain, (store(a_1081, n14, e14)=a_1082)). % 6.87/2.64 tff(c_30, plain, (store(a_1080, n13, e13)=a_1081)). % 6.87/2.64 tff(c_28, plain, (store(a_1079, n12, e12)=a_1080)). % 6.87/2.64 tff(c_120, plain, (store(a_1125, n24, e24)=a_1126)). % 6.87/2.64 tff(c_26, plain, (store(a_1078, n11, e11)=a_1079)). % 6.87/2.64 tff(c_22, plain, (store(a_1076, n9, e9)=a_1077)). % 6.87/2.64 tff(c_20, plain, (store(a_1075, n8, e8)=a_1076)). % 6.87/2.64 tff(c_18, plain, (store(a_1074, n7, e7)=a_1075)). % 6.87/2.64 tff(c_110, plain, (store(a_1120, n12, e12)=a_1121)). % 6.87/2.64 tff(c_16, plain, (store(a_1073, n6, e6)=a_1074)). % 6.87/2.64 tff(c_14, plain, (store(a_1072, n5, e5)=a_1073)). % 6.87/2.64 tff(c_12, plain, (store(a_1071, n4, e4)=a_1072)). % 6.87/2.64 tff(c_10, plain, (store(a_1070, n3, e3)=a_1071)). % 6.87/2.64 tff(c_8, plain, (store(a_1069, n2, e2)=a_1070)). % 6.87/2.64 tff(c_130, plain, (sk(a_1098, a_1128)=i_1129)). % 6.87/2.64 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.87/2.64 %------------------------------------------------------------------------------