%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW474+3 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n009.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:21 PM UTC 2026 % Result : Unknown 0.72s 0.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW474+3 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n009.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 13:34:57 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.72/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.72/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.72/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.72/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.72/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.72/0.67 Execution normal ended with status: gaveup % 0.72/0.67 Execution resolution_1 ended with status: gaveup % 0.72/0.67 Execution resolution_2 ended with status: gaveup % 0.72/0.67 Execution resolution_3 ended with status: gaveup % 0.72/0.67 Execution lmodel_grow ended with status: gaveup % 0.72/0.67 No successful execution. % 0.72/0.67 % 0.72/0.67 Input Clauses: % 0.72/0.68 % 0.72/0.68 Predicates: is_bool is_fun1661590463l_bool is_pname is_fun_pname_bool is_option_pname hBOOL = 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 ren1224 ren1225 ren1226 ren1227 ren1228 ren1229 ren1230 ren1231 ren1232 ren1233 ren1234 ren1235 ren1236 ren1237 ren1238 ren1239 ren1240 ren1241 ren1242 ren1243 ren1244 ren1245 ren1246 ren1247 ren1248 ren1249 ren1250 ren1251 ren1252 ren1253 ren1254 ren1255 ren1256 ren1257 ren1258 ren1259 ren1260 ren1261 ren1262 ren1263 ren1264 ren1265 ren1266 ren1267 ren1268 ren1269 ren1270 ren1271 ren1272 ren1273 ren1274 ren1275 ren1276 ren1277 ren1278 ren1279 ren1280 ren1281 ren1282 ren1283 ren1284 ren1285 ren1286 ren1287 ren1288 % 0.72/0.68 Fol Constants: wT_bodies finite_finite_pname pname bool hoare_1795711768gleton none_pname bot_bot_bool bot_bo844097828e_bool bot_bo1649642514l_bool top_to2127735616e_bool fFalse fTrue pn bot_bo784226126e_bool ord_le1449778818e_bool insert1744391420_state hoare_Mirabelle_MGT body_1 the_com body finite595471783e_bool finite786885583l_bool collec1613912337l_bool cOMBC_7971162l_bool ord_le675606854l_bool finite627955595e_bool finite1203709595l_bool collec895295961l_bool cOMBC_991209188l_bool ord_le694194916l_bool finite694102371_state collec1987918285e_bool cOMBC_1350613978l_bool collec1974731493e_bool cOMBC_1284144636l_bool ord_le313189616e_bool ord_le1708315510m_bool bot_bot_fun_com_bool finite_finite_com insert_com insert1325755072e_bool insert1720618162e_bool insert_pname bot_bo942947096l_bool cOMBS_350070575l_bool fconj cOMBS_1162100051l_bool collec637225377_state cOMBS_865875691l_bool collect_pname cOMBS_568398431l_bool cOMBK_497473068_state cOMBK_131063602_state cOMBK_869602456te_com cOMBK_2086841362_pname member1667945571_state member_pname cOMBK_pname_pname cOMBK_com_pname member_com some_com some_pname some_H1043067815_state wt collect_com cOMBK_bool_pname cOMBK_1857069011e_bool cOMBK_293339231e_bool cOMBK_bool_com cOMBK_988866959_state fimplies fNot cOMBC_1149511130e_bool fequal_pname cOMBS_com_bool_bool cOMBC_com_com_bool fequal_com fequal533582459e_bool fequal1475827639e_bool cOMBC_1967329268e_bool fequal1440809015_state fdisj cOMBC_1904837336l_bool cOMBC_1988546018l_bool member799430823e_bool cOMBC_1484018740l_bool member131361931e_bool cOMBC_1058051404l_bool cOMBC_538205282l_bool cOMBC_114640782e_bool cOMBC_1836455480e_bool cOMBC_754402940e_bool cOMBC_com_pname_bool cOMBC_1952686190e_bool cOMBC_1004116266e_bool cOMBC_1558112230e_bool cOMBC_1984545208l_bool cOMBC_1757633998l_bool cOMBC_19854728e_bool semila176469292e_bool the_elem_pname the_elem_com the_el2080696983_state ord_less_eq_bool the_pname_1 the_Ho32424093_state hoare_1191504582_state semila605046092m_bool semila278973382e_bool semila1782091504l_bool semila1672697786l_bool cOMBS_1524960158_state cOMBS_1020065803_state cOMBC_471052088e_bool cOMBC_231445413l_bool cOMBS_858986606_state cOMBS_384351451_state cOMBS_57685138_state cOMBS_1164062463_state cOMBK_631994958_state cOMBC_2027030106e_bool fequal_state semila1168014441p_bool skip cOMBC_952831051e_bool cOMBS_1378840469l_bool semi the_com_1 fequal_fun_com_bool cOMBC_1977231931m_bool the_pname cOMBC_1123258281e_bool the_Ho2067184133_state cOMBC_1229155955e_bool fAll_state semila1130628874l_bool semila1028267552l_bool semila1635148844e_bool semila1874263622e_bool semila980496562m_bool minus_59609839m_bool minus_1015773161e_bool minus_1805465033e_bool minus_1290075917l_bool minus_1929235165l_bool semila310582991f_bool cOMBS_853737105_state cOMBS_140201078_state if_Hoa443228806_state cOMBS_904531235on_com cOMBS_1529518335on_com if_option_com cOMBC_788185579m_bool cOMBC_1880008793e_bool cOMBC_528733435e_bool cOMBK_413306633_pname none_com cOMBC_694979519l_bool cOMBC_772615479l_bool cOMBC_1377256501l_bool cOMBC_1639502213l_bool cOMBC_59067399e_bool none_H175086635_state cOMBC_1381995473m_bool fequal_option_com finite_finite_bool member_bool insert_bool big_la28065288e_bool big_la236972906e_bool top_top_fun_com_bool top_to215444530e_bool fa y skc1109 skc1110 skc1235 skc1236 skc1237 skc1238 skc1239 skc1240 skc1241 skc1242 skc1243 skc1244 skc1245 skc1246 skc1247 skc1248 skc1249 skc1250 skc1251 skc1252 % 0.72/0.68 Fol Functions: finite1653727294m_bool finite2017903282e_bool finite318301748l_bool finite2036162504e_bool finite367769966e_bool finite1765632844e_bool finite860057415ne_com finite1282449217_pname finite683959609_state finite1626890877e_bool finite2009063477e_bool finite666746948em_com finite89670078_pname finite416071164_state finite1268145088e_bool finite688249778e_bool inj_on_pname_pname inj_on621632009_state inj_on737724108_pname undefined_pname undefined_bool fun undefi17486888e_bool undefi64961550l_bool dom_pname_com dom_pname_pname dom_pn480909800_state is_none_com is_none_pname is_non1379144176_state set_pname vimage1011814463_state hAPP_com_pname hAPP_com_bool hAPP_c1967741679e_bool hAPP_pname_pname hAPP_pname_bool hAPP_p1252095976_pname hAPP_p61793385e_bool hAPP_p338031245l_bool hAPP_state_bool hAPP_bool_bool hAPP_b76515610e_bool hAPP_b357632156l_bool hAPP_H1193503499_pname hAPP_H242767318e_bool hAPP_H1671063474_pname hAPP_H1776011827e_bool hAPP_H358531139l_bool hAPP_option_com_bool hAPP_o1092643708e_bool hAPP_o593586696_pname hAPP_f990396704l_bool hAPP_f1438183293e_bool hAPP_f1297739591_pname hAPP_f1664156314l_bool hAPP_f759274231e_bool hAPP_f434788991l_bool hAPP_f42430548e_bool hAPP_f327114704l_bool hAPP_f387058535l_bool hAPP_f88366945_pname hAPP_f1378282496l_bool hAPP_f1083669085e_bool hAPP_f1709493145l_bool hAPP_f1935102916l_bool hAPP_f674760225e_bool hAPP_f559147733l_bool hAPP_f1410040974l_bool hAPP_f306376939e_bool hAPP_f389811538l_bool hAPP_f1178960312l_bool hoare_512830354_state hAPP_f849457489l_bool hAPP_H1902130436e_bool hAPP_f806699093e_bool hAPP_pname_com hAPP_c1455475371_state hAPP_p799580910on_com hAPP_option_com_com hAPP_f1879335953l_bool hAPP_f510955609l_bool hAPP_f783502055l_bool hAPP_f1901243753l_bool hAPP_f1516997247l_bool hAPP_f347786453l_bool hAPP_f1348212993l_bool hAPP_f734420447l_bool hAPP_f1297925993l_bool image_1403607267e_bool image_995511119e_bool image_47868345e_bool image_234387449e_bool hAPP_f1492100075l_bool image_845802851_state hAPP_f509793681e_bool image_1497401961_state hAPP_f1216288071e_bool image_1283814551_pname image_1863446033_pname image_185131637_state hAPP_f360545851e_bool hAPP_f273696895l_bool hAPP_c566651504m_bool hAPP_f1682609283m_bool hAPP_f1320879424l_bool hAPP_f1472090462l_bool hAPP_p905327722e_bool cOMBB_2095475776e_bool hAPP_f143162813l_bool hAPP_f624840228l_bool cOMBB_1749019442e_bool hAPP_f118042163l_bool hAPP_f524831474l_bool cOMBB_1291456124_state hAPP_f832587837l_bool hAPP_f1702629984e_bool cOMBB_675860798_pname hAPP_f1402196763l_bool hAPP_f649174806e_bool hAPP_p1227118702_pname image_1774499931_pname hAPP_c57939194te_com image_741143905te_com hAPP_f1815646051m_bool hAPP_H275587026_state image_2605051_state hAPP_f457085749e_bool hAPP_H1938877132_state hAPP_H2039996199l_bool hAPP_p1170154830_pname image_pname_pname hAPP_c1494068046me_com image_pname_com hAPP_f1206115581m_bool hAPP_c667411853l_bool hAPP_com_option_com dom_com_com dom_Ho2070278094_pname hAPP_H1633077406_state dom_Ho1607160812_state hAPP_H46530577te_com image_com_pname hAPP_p1751618853_state hAPP_b167205134l_bool hAPP_b1153789088m_bool hAPP_b974863576e_bool cOMBB_647938656_pname hAPP_f22061361e_bool cOMBB_886968260ol_com cOMBB_bool_bool_com hAPP_f908845385m_bool hAPP_c1396316405m_bool hAPP_f954469007l_bool hAPP_f328772264m_bool cOMBB_307249310e_bool cOMBB_1686148692e_bool cOMBB_325909978_state hAPP_f1902016361e_bool hAPP_H216526335e_bool hAPP_f578650245m_bool hAPP_f1145991873l_bool hAPP_f1236719585l_bool hAPP_f661147897e_bool hAPP_f1184122441e_bool hAPP_p485182952_state hAPP_f556039215l_bool hAPP_f631019661l_bool cOMBB_1327031172ol_com hAPP_f475997903e_bool hAPP_f235185669m_bool hAPP_H313059897m_bool image_661047967_state cOMBB_1563888316_state hAPP_f596278895e_bool hAPP_H574424047_state cOMBB_1724041344e_bool hAPP_f2113567599e_bool hAPP_f1186253673l_bool hAPP_f1218207411_state cOMBB_1840094962e_bool hAPP_f610934515e_bool hAPP_f1463049441l_bool hAPP_f718417177_state cOMBB_1083901850ol_com hAPP_f835719487e_bool hAPP_f734198589m_bool hAPP_p1639923567m_bool cOMBB_1365368614_state hAPP_f777604691e_bool hAPP_f1720171569e_bool hAPP_p606792009e_bool cOMBB_542850580_pname hAPP_f1336811455e_bool cOMBB_598082538e_bool hAPP_f1385420507e_bool hAPP_f2082757169l_bool cOMBB_1400714760e_bool hAPP_f700046015e_bool hAPP_f780571929l_bool hAPP_p1235466077l_bool cOMBB_1631414076_state hAPP_f381060343l_bool hAPP_f591683433e_bool cOMBB_639263758_state hAPP_f1191357267l_bool cOMBB_408569982_pname hAPP_f567934427l_bool cOMBB_949755692_pname hAPP_f1143533991l_bool hAPP_f568104217e_bool cOMBB_181781758_pname hAPP_f472107739e_bool hAPP_f343137017e_bool hAPP_f1794460506e_bool cOMBB_271860050_pname hAPP_f1377420673_state cOMBB_923936821_pname hAPP_f96342628me_com hAPP_f1276420679ol_com hAPP_b589554111l_bool hAPP_o1912464824_state hAPP_f274181323_state hAPP_c27135337_state hAPP_f497755132_state hAPP_f1120618594m_bool hAPP_f1388330588e_bool hAPP_f230953622l_bool hAPP_f1847120l_bool cOMBB_2084106034_pname hAPP_f804744487_state hAPP_f1922754332_state hAPP_f460309545_state hAPP_f1811131990_state hAPP_f914896950_state cOMBB_1757942702_state cOMBB_188601460_state cOMBB_1759179140_state hAPP_f1283379615l_bool hAPP_f873506917e_bool hAPP_f701449317e_bool hAPP_b1095269219e_bool hAPP_p1637813682e_bool hAPP_f887530048e_bool hAPP_f792846925ol_com cOMBB_1794358604e_bool hAPP_f1633046421_state hAPP_f578932784_state hAPP_f240260249_state hAPP_f815143704_state hAPP_f819036232_state hAPP_f1487042470e_bool hAPP_f1547517799ol_com cOMBB_2049797414e_bool hAPP_f250550847_state hAPP_f37848848_state hAPP_f824259881_state hAPP_f886846002_state hAPP_f578501918_state hAPP_s1806633685e_bool hAPP_f817621513e_bool hAPP_f1863945078e_bool hoare_919241616_state set_com set_Ho1741238126_state hAPP_com_fun_com_com hAPP_com_com hAPP_H280516760_state cOMBB_20296667_state hAPP_f1138284024e_bool hAPP_f915354021e_bool cOMBB_160679318_state hAPP_f1759915619e_bool while image_2063528359e_bool image_390184709e_bool image_com_com cOMBB_298914627ol_com hAPP_f947797701m_bool hAPP_f721468006m_bool hAPP_f1998868198m_bool cOMBB_530759491_pname hAPP_f698292281e_bool hAPP_f180827860e_bool cOMBB_1282391997_state hAPP_f1802364479e_bool hAPP_f874203478e_bool hAPP_f1900156034e_bool cOMBB_1911358915_state cOMBB_1036740637_state evalc cOMBB_1476898461_state hAPP_f249262236e_bool hAPP_f1935169308e_bool cOMBB_143651633_pname hAPP_f1836930278_state hAPP_f2119427284_state hAPP_f1655792756_state hAPP_f799842582_state hAPP_f1343550633_state cOMBB_1394247784_pname hAPP_f755519727on_com hAPP_f2093196134on_com hAPP_f648377725on_com hAPP_f1673966486on_com hAPP_f2123220539on_com overri1496249029on_com partial_flat_lub_com partia752020666_pname partia325231104_state hAPP_f1898485935m_bool cOMBB_2112550369ol_com hAPP_f57617970m_bool hAPP_f182188835e_bool cOMBB_1919352417_pname hAPP_f647826488e_bool hAPP_f2061951445e_bool cOMBB_604855927_state hAPP_f241329646e_bool fun_up1055265789_state hAPP_o129566686on_com fun_up879233478on_com finite1275301314m_bool finite315386934e_bool finite1230907212e_bool hAPP_f1477350485l_bool cOMBB_631815671e_bool hAPP_f836143551l_bool hAPP_f417341722l_bool hAPP_f1149191722l_bool finite1627341516l_bool hAPP_f1573805579l_bool cOMBB_494346593e_bool hAPP_f476955937l_bool hAPP_f2059879088l_bool hAPP_f1316144452l_bool finite1943735070l_bool cOMBB_667059641_pname hAPP_f2028971360e_bool hAPP_f376349141e_bool hAPP_f103229774e_bool finite1443934175_pname inj_on264996226_state inj_on11367768on_com cOMBB_418828222_pname hAPP_f919496731m_bool hAPP_f837293113e_bool finite446335722e_bool hAPP_f246190092e_bool finite391880392e_bool hAPP_f1712138014e_bool hAPP_b1787118453l_bool finite1909292976l_bool hAPP_b496459037l_bool hAPP_f961197973l_bool inj_on1490514707e_bool inj_on2143431281e_bool inj_on535898123_state finite_fold_com_com hAPP_c1546426672ol_com finite1657623752_pname hAPP_p1630511146_pname finite212984546_state hAPP_H1440241088_state inj_on63516655_pname restri1382200118me_com hAPP_b1679505845on_com hAPP_o334540577on_com hAPP_o356497025on_com hAPP_o1684370239m_bool hAPP_c1580157610l_bool hAPP_f167292325e_bool hAPP_b2019457360e_bool hAPP_s58564346l_bool hAPP_p393069232l_bool hAPP_f644196280e_bool hAPP_b993469484_state hAPP_p558118546m_bool hAPP_f1259673775l_bool hAPP_f1476298914l_bool hAPP_f1012183542e_bool hAPP_s1874344717e_bool hAPP_p1086945780on_com hAPP_c1311333443e_bool hAPP_H1270401638l_bool hAPP_s1226857760e_bool hAPP_f2067558332l_bool hAPP_s2001034685l_bool hAPP_s336103912e_bool hAPP_p1164893188on_com hAPP_p1947457250_state hAPP_p1331349103_state hAPP_p357103842_state hAPP_f1867816801_state hAPP_p105983054e_bool hAPP_f2099268820_state hAPP_p1159359355_state hAPP_f1554347387_state hAPP_f403544558_state 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 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 skf1180 skf1181 skf1182 skf1183 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 skf1253 skf1254 skf1255 skf1256 skf1257 skf1258 skf1259 skf1260 skf1261 skf1262 skf1263 skf1264 skf1265 skf1266 skf1267 skf1268 skf1269 skf1270 skf1271 skf1272 skf1273 skf1274 skf1275 skf1276 skf1277 skf1278 skf1279 skf1280 skf1281 skf1282 skf1283 % 0.72/0.68 Problem Properties: % 0.72/0.68 This is a full first-order problem with equality. % 0.72/0.68 SZS status GaveUp % 0.72/0.68 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.72/0.68 %------------------------------------------------------------------------------