%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW472+3 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n026.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 : Thu May 7 07:38:20 PM UTC 2026 % Result : Unknown 0.69s 0.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW472+3 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n026.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 13:35:39 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.69/0.68 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.68 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.68 Execution normal ended with status: gaveup % 0.69/0.68 Execution resolution_1 ended with status: gaveup % 0.69/0.68 Execution resolution_2 ended with status: gaveup % 0.69/0.68 Execution resolution_3 ended with status: gaveup % 0.69/0.68 Execution lmodel_grow ended with status: gaveup % 0.69/0.68 No successful execution. % 0.69/0.68 % 0.69/0.68 Input Clauses: % 0.69/0.68 % 0.69/0.68 Predicates: is_bool hBOOL = is_loc ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 ren125 ren126 ren127 ren128 ren129 ren130 ren131 ren132 ren133 ren134 ren135 ren136 ren137 ren138 ren139 ren140 ren141 ren142 ren143 ren144 ren145 ren146 ren147 ren148 ren149 ren150 ren151 ren152 ren153 ren154 ren155 ren156 ren157 ren158 ren159 ren160 ren161 ren162 ren163 ren164 ren165 ren166 ren167 ren168 ren169 ren170 ren171 ren172 ren173 ren174 ren175 ren176 ren177 ren178 ren179 ren180 ren181 ren182 ren183 ren184 ren185 ren186 ren187 ren188 ren189 ren190 ren191 ren192 ren193 ren194 ren195 ren196 ren197 ren198 ren199 ren1100 ren1101 ren1102 ren1103 ren1104 ren1105 ren1106 ren1107 ren1108 ren1109 ren1110 ren1111 ren1112 ren1113 ren1114 ren1115 ren1116 ren1117 ren1118 ren1119 ren1120 ren1121 ren1122 ren1123 ren1124 ren1125 ren1126 ren1127 ren1128 ren1129 ren1130 ren1131 ren1132 ren1133 ren1134 ren1135 ren1136 ren1137 ren1138 ren1139 ren1140 ren1141 ren1142 ren1143 ren1144 ren1145 ren1146 ren1147 ren1148 ren1149 ren1150 ren1151 ren1152 ren1153 ren1154 ren1155 ren1156 ren1157 ren1158 ren1159 ren1160 ren1161 ren1162 ren1163 ren1164 ren1165 ren1166 ren1167 ren1168 ren1169 ren1170 ren1171 ren1172 ren1173 ren1174 ren1175 ren1176 ren1177 ren1178 ren1179 ren1180 ren1181 ren1182 ren1183 ren1184 ren1185 ren1186 ren1187 ren1188 ren1189 ren1190 ren1191 ren1192 ren1193 ren1194 ren1195 ren1196 ren1197 ren1198 ren1199 ren1200 ren1201 ren1202 ren1203 ren1204 ren1205 ren1206 ren1207 ren1208 ren1209 ren1210 ren1211 ren1212 ren1213 ren1214 ren1215 ren1216 ren1217 ren1218 ren1219 ren1220 ren1221 ren1222 ren1223 % 0.69/0.68 Fol Constants: bot_bot_bool fFalse fTrue bot_bo784226126e_bool insert1744391420_state member_int insert_int member_nat insert_nat member1667945571_state bot_bot_fun_int_bool bot_bot_fun_nat_bool collect_int collect_nat collec637225377_state fimplies fNot fequal_int fequal_nat fequal1440809015_state fdisj the_elem_int the_elem_nat the_el2080696983_state skip ord_le951220754t_bool ord_le1568362934t_bool ord_le1449778818e_bool ord_less_eq_nat ord_less_eq_int ord_less_eq_bool bot_bot_nat finite_finite_int finite_finite_nat finite694102371_state ord_le694194916l_bool minus_1449998731t_bool minus_2067140911t_bool minus_1805465033e_bool fconj minus_minus_bool minus_minus_int times_times_nat times_times_int ord_le1912455174t_bool ord_le382113706t_bool ord_le2137177998e_bool finite_card_int finite_card_nat finite1401757860_state ord_less_nat ord_less_int ord_less_bool minus_minus_nat one_one_nat one_one_int plus_plus_nat plus_plus_int zero_zero_int suc zero_zero_nat number_number_of_nat ord_min_nat number_number_of_int nat_tsub abs_abs_int semiri1621563631at_int c p q skc1180 skc1181 skc1182 skc1183 % 0.69/0.68 Fol Functions: big_se1212619424_state big_se913005884ig_int big_se275732192ig_nat finite1720675051_state finite1973466193nt_int finite2130160977at_nat finite2036162504e_bool finite58652534t_bool finite1956789438t_bool finite683959609_state finite1626084323ne_int finite988810631ne_nat finite416071164_state finite1432773856em_int finite795500164em_nat hAPP_state_bool hAPP_bool_bool hAPP_H242767318e_bool hAPP_int_bool hAPP_nat_bool hAPP_f1378282496l_bool hAPP_f448129468l_bool hAPP_f54304608l_bool hAPP_f1410040974l_bool hoare_512830354_state hoare_1191504582_state hoare_919241616_state hAPP_H1902130436e_bool hAPP_f806699093e_bool hAPP_s1806633685e_bool hAPP_i2112223885l_bool hAPP_i1529485324t_bool hAPP_f1805168059t_bool hAPP_n215258509l_bool hAPP_n1512601776t_bool hAPP_f800510211t_bool hAPP_H2039996199l_bool cOMBK_bool_int cOMBK_bool_nat cOMBK_988866959_state cOMBB_1652995168ol_int cOMBB_bool_bool_int cOMBC_int_int_bool hAPP_i1948725293t_bool hAPP_f2144054103l_bool cOMBS_int_bool_bool cOMBB_1015721476ol_nat cOMBB_bool_bool_nat cOMBC_nat_nat_bool hAPP_n1699378549t_bool hAPP_f1146629647l_bool cOMBS_nat_bool_bool cOMBB_1291456124_state cOMBB_325909978_state cOMBC_1967329268e_bool hAPP_H216526335e_bool hAPP_f832587837l_bool cOMBS_865875691l_bool cOMBC_94739984l_bool cOMBC_226598744l_bool cOMBC_538205282l_bool hAPP_f1594865479ol_int hAPP_f22106695ol_nat hAPP_f718417177_state semi finite_fold1Set_int finite_fold1Set_nat finite2066257190_state finite_fold1_int finite_fold1_nat finite1255650454_state hAPP_f284875647l_bool hAPP_f103356543l_bool hAPP_f849457489l_bool hAPP_b589554111l_bool hAPP_f1676271015ol_nat hAPP_f166061059ol_int hAPP_n1497837059e_bool hAPP_i468480167e_bool hAPP_nat_nat hAPP_int_int finite772772422nt_int finite929467206at_nat finite1946095968_state hAPP_int_fun_int_int hAPP_nat_fun_nat_nat hAPP_H280516760_state hAPP_H574424047_state powp_H1405539888_state hAPP_f1516997247l_bool hAPP_f1223193598t_bool hAPP_f1730770594t_bool hAPP_f1794460506e_bool hAPP_f957591787ol_nat finite_fold_int_int finite_fold_nat_nat finite212984546_state com_size size_size_com cond local while hAPP_int_nat hAPP_nat_int if_nat hAPP_i68813070l_bool hAPP_n1006566506l_bool hAPP_H1270401638l_bool hoare_Mirabelle_MGT skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf110 skf111 skf112 skf113 skf114 skf115 skf116 skf117 skf118 skf119 skf120 skf121 skf122 skf123 skf124 skf125 skf126 skf127 skf128 skf129 skf130 skf131 skf132 skf133 skf134 skf135 skf136 skf137 skf138 skf139 skf140 skf141 skf142 skf143 skf144 skf145 skf146 skf147 skf148 skf149 skf150 skf151 skf152 skf153 skf154 skf155 skf156 skf157 skf158 skf159 skf160 skf161 skf162 skf163 skf164 skf165 skf166 skf167 skf168 skf169 skf170 skf171 skf172 skf173 skf174 skf175 skf176 skf177 skf178 skf179 skf180 skf181 skf182 skf183 skf184 skf185 skf186 skf187 skf188 skf189 skf190 skf191 skf192 skf193 skf194 skf195 skf196 skf197 skf198 skf199 skf1100 skf1101 skf1102 skf1103 skf1104 skf1105 skf1106 skf1107 skf1108 skf1109 skf1110 skf1111 skf1112 skf1113 skf1114 skf1115 skf1116 skf1117 skf1118 skf1119 skf1120 skf1121 skf1122 skf1123 skf1124 skf1125 skf1126 skf1127 skf1128 skf1129 skf1130 skf1131 skf1132 skf1133 skf1134 skf1135 skf1136 skf1137 skf1138 skf1139 skf1140 skf1141 skf1142 skf1143 skf1144 skf1145 skf1146 skf1147 skf1148 skf1149 skf1150 skf1151 skf1152 skf1153 skf1154 skf1155 skf1156 skf1157 skf1158 skf1159 skf1160 skf1161 skf1162 skf1163 skf1164 skf1165 skf1166 skf1167 skf1168 skf1169 skf1170 skf1171 skf1172 skf1173 skf1174 skf1175 skf1176 skf1177 skf1178 skf1179 skf1184 skf1185 skf1186 skf1187 skf1188 skf1189 skf1190 skf1191 skf1192 skf1193 skf1194 skf1195 skf1196 skf1197 skf1198 skf1199 skf1200 skf1201 skf1202 skf1203 skf1204 skf1205 skf1206 skf1207 skf1208 skf1209 skf1210 skf1211 skf1212 skf1213 skf1214 skf1215 skf1216 skf1217 skf1218 skf1219 skf1220 skf1221 skf1222 skf1223 skf1224 skf1225 skf1226 skf1227 skf1228 skf1229 skf1230 skf1231 skf1232 skf1233 skf1234 skf1235 skf1236 skf1237 skf1238 skf1239 skf1240 skf1241 skf1242 skf1243 skf1244 skf1245 skf1246 skf1247 % 0.69/0.68 Problem Properties: % 0.69/0.68 This is a full first-order problem with equality. % 0.69/0.68 SZS status GaveUp % 0.69/0.68 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.69/0.68 %------------------------------------------------------------------------------