%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW470+2 : 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 : n021.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:18 PM UTC 2026 % Result : Unknown 0.57s 0.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW470+2 : 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.16/0.34 % Computer : n021.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:36:13 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.24/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Execution normal ended with status: gaveup % 0.47/0.62 Execution resolution_1 ended with status: gaveup % 0.47/0.62 Execution resolution_2 ended with status: gaveup % 0.47/0.62 Execution resolution_3 ended with status: gaveup % 0.47/0.62 Execution lmodel_grow ended with status: gaveup % 0.47/0.62 No successful execution. % 0.47/0.62 % 0.47/0.62 Input Clauses: % 0.47/0.63 % 0.47/0.63 Predicates: is_bool is_glb is_vname is_loc 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 % 0.47/0.63 Fol Constants: glb_1 loc_1 bot_bot_bool fFalse fTrue bot_bo1181479936a_bool bot_bo1055319631e_bool insert873085594iple_a insert1835143293_state cOMBC_41962815e_bool cOMBB_1348041619bool_a cOMBC_231445413l_bool cOMBB_1355796797bool_a cOMBB_188601460_state fconj cOMBC_471052088e_bool cOMBB_1757942702_state cOMBB_1759179140_state cOMBK_1458035955bool_a cOMBC_2027030106e_bool fequal_state cOMBK_631994958_state member1713797107iple_a member_nat insert_nat member1758697444_state bot_bot_fun_nat_bool fequal879838495iple_a fequal_nat fequal_fun_nat_bool insert_fun_nat_bool bot_bo1701429464l_bool fequal1531560888_state cOMBC_839220826a_bool cOMBC_nat_nat_bool cOMBC_1693257480l_bool cOMBC_1424981238e_bool cOMBS_1148211387l_bool cOMBB_1782929690iple_a cOMBS_nat_bool_bool cOMBB_1015721476ol_nat cOMBS_1187019125l_bool cOMBB_444170502t_bool cOMBS_1248383340l_bool cOMBB_1382207997_state cOMBK_bool_nat cOMBK_151824839iple_a cOMBK_1994329625t_bool cOMBK_1079618832_state fimplies cOMBB_1799513916iple_a fNot cOMBB_bool_bool_nat cOMBB_238756964t_bool cOMBB_416661851_state fdisj cOMBC_1552014468l_bool cOMBC_226598744l_bool cOMBC_1245412066l_bool member_fun_nat_bool cOMBC_764456866l_bool the_el1436340927iple_a the_elem_nat the_el23965208_state skip the_Ho746640593iple_a cOMBB_1501709507iple_a fequal1258664663a_bool cOMBC_708118077a_bool the_nat cOMBB_955900739ol_nat cOMBC_178881787t_bool the_Ho10452358_state cOMBB_1653402815_state fequal1746921144e_bool cOMBC_488258100e_bool cOMBC_524597097e_bool cOMBB_2139825703bool_a cOMBB_844853809_state cOMBS_777315357_state cOMBC_1193272608_state update cOMBC_867582640e_bool cOMBB_1941618714_state cOMBK_1505147640_a_nat cOMBK_2022976521_state cOMBK_944981412iple_a cOMBK_547979437iple_a cOMBK_nat_nat cOMBK_690957994_state cOMBK_1824972302iple_a cOMBK_1950023923_state cOMBI_nat cOMBI_1367665338_state cOMBI_1218222237iple_a cOMBC_1777403949_state cOMBB_572666224_state cOMBS_1378840469l_bool cOMBB_237455441bool_a finite_finite_nat finite784854244_state finite1655202547iple_a minus_2067140911t_bool minus_2076558538e_bool minus_469558085a_bool cOMBB_1654519265ol_nat cOMBC_646315179t_bool cOMBB_946224375_state cOMBC_872426556e_bool cOMBB_2080540641iple_a cOMBC_314077933a_bool times_times_nat ord_le1568362934t_bool ord_le1720872323e_bool ord_le1908022732a_bool ord_less_eq_nat semila1498788770a_bool semila465093516t_bool finite2012431853t_bool semila972727038up_nat semila1168014441p_bool semila447562797e_bool ord_less_eq_bool bot_bot_nat cOMBB_800536526ol_nat big_la43341705in_nat semila840543986t_bool semila671163144a_bool semila80283416nf_nat semila2145357127e_bool semila310582991f_bool cOMBK_bool_state cOMBB_160679318_state cOMBC_892787026e_bool cOMBB_145932198bool_a g c p b skc1149 skc1150 skc1165 skc1166 % 0.47/0.63 Fol Functions: big_se275732192ig_nat glb loc finite1200705745iple_a finite419198954a_bool finite1317819144e_bool finite1956789438t_bool finite1669978781iple_a finite774711482_state finite988810631ne_nat finite950012314iple_a finite506823037_state finite795500164em_nat undefined_glb undefined_loc evaln hAPP_state_bool hAPP_bool_bool hAPP_H1421470952a_bool hAPP_H513860823e_bool hAPP_nat_bool hAPP_f540970102l_bool hAPP_f1760790145l_bool hAPP_f54304608l_bool hAPP_f1637334154l_bool hoare_606018542rivs_a hoare_659004819_state hoare_1575745797_state hoare_1760757500iple_a hAPP_H1641355846a_bool hAPP_f1591852335a_bool hAPP_H727730819e_bool hAPP_f921536533e_bool hAPP_f1006724181e_bool hAPP_f1561913689l_bool hAPP_f1178339559l_bool hAPP_f1509969235l_bool hAPP_f340725611e_bool hAPP_f1824947087e_bool hAPP_b540892988e_bool hAPP_f1398071125e_bool hAPP_f1345202233l_bool hAPP_f1283379615l_bool hAPP_f873506917e_bool hAPP_f701449317e_bool hAPP_b1095269219e_bool hAPP_a2036067514e_bool hAPP_f817621513e_bool hAPP_s1806633685e_bool hAPP_f762886889e_bool hAPP_f1863945078e_bool hAPP_H1840393229l_bool hAPP_n215258509l_bool hAPP_n1512601776t_bool hAPP_f800510211t_bool hAPP_H248360617l_bool hAPP_H1190454433a_bool collec268032053iple_a hAPP_n1699378549t_bool collect_nat hAPP_f103356543l_bool collect_fun_nat_bool hAPP_f633452666l_bool hAPP_f1246832597l_bool hAPP_H1645666623e_bool collec727977250_state hAPP_f1371755681a_bool hAPP_f229349961t_bool hAPP_f643944041l_bool hAPP_f262880489e_bool hAPP_f439164429l_bool hAPP_f997599971l_bool hAPP_f1203760810a_bool hAPP_f1080886329l_bool hAPP_f1146629647l_bool hAPP_f561022312t_bool hAPP_f857404385l_bool hAPP_f1974927549l_bool hAPP_f1743029098l_bool hAPP_f1442918689l_bool hAPP_f1558728829l_bool hAPP_f760664097e_bool hAPP_b1013836512t_bool hAPP_b119575286a_bool hAPP_b1630757474l_bool hAPP_b1245957081e_bool hAPP_f34030599a_bool hAPP_f894608603t_bool hAPP_f1164891443l_bool hAPP_f1037965299e_bool hAPP_f672239281a_bool hAPP_f1722879237t_bool hAPP_f1443436725l_bool hAPP_f1262649863e_bool hAPP_f124283079iple_a hAPP_f22106695ol_nat hAPP_f2143211163_state semi hAPP_f430043647l_bool hAPP_f390613447a_bool hAPP_f549683569a_bool hAPP_f1665407592a_bool hAPP_f772297704a_bool hAPP_f1777703707t_bool hAPP_f688831301t_bool hAPP_f1570313510t_bool hAPP_f158894502t_bool hAPP_f854625363l_bool hAPP_f1548785833e_bool hAPP_f964290431e_bool hAPP_f762269719e_bool hAPP_f1456107715e_bool hAPP_f635443597e_bool hAPP_f1406200875e_bool hAPP_f1460451647e_bool hAPP_f1542232213_state hAPP_v365393659_state hAPP_f851239890_state hAPP_f871651461_state hAPP_f100967412e_bool ass hAPP_f1151843515e_bool hAPP_f289738463e_bool hAPP_f1706273077e_bool hAPP_f1838002347e_bool hAPP_H1450464520iple_a image_1782127643iple_a hAPP_H377435237iple_a image_129517430iple_a hAPP_n1800114674_a_nat image_194810223_a_nat hAPP_H558669354_state image_1604514514_state hAPP_nat_fun_nat_nat image_nat_nat hAPP_H521649881_state image_650584225_state hAPP_H1455657330iple_a image_306007685iple_a hAPP_n436597305te_nat image_1410872416te_nat hAPP_H563960305_state hAPP_n1126952044_state image_1821565372_state hAPP_H928324994_state hAPP_nat_nat hAPP_H738206399_a_nat hAPP_H716259088te_nat hAPP_H678412245iple_a hAPP_H1600811558iple_a hAPP_n178040171iple_a hAPP_b589554111l_bool finite9525415_state finite_fold1Set_nat finite1537818352iple_a hAPP_f1848060885_state getlocs hAPP_n1547241352_state hAPP_f1259673775l_bool hAPP_f644196280e_bool hAPP_f512427579e_bool local hAPP_f1159960589e_bool hAPP_f769584981e_bool evalc hAPP_s712361723_state hAPP_v594194232_state hAPP_state_nat hAPP_nat_state finite1935632226_state finite929467206at_nat finite2010942150iple_a hoare_Mirabelle_MGT hoare_592710359_state hoare_560051114alid_a hAPP_f1730770594t_bool hAPP_f1583986009e_bool hAPP_f1026156344a_bool hAPP_f1311642927t_bool hAPP_f1115950719t_bool hAPP_f10625010t_bool hAPP_f2049746453e_bool hAPP_f1470644835e_bool hAPP_f531275309e_bool hAPP_f450029403a_bool hAPP_f2085120383a_bool hAPP_f485051996a_bool finite_fold1_nat finite_fold_nat_nat finite1346402327_state finite1382394752iple_a finite978536264iple_a finite202520804_state finite1578363458t_bool finite512563852e_bool finite1979045230a_bool partia1866111638iple_a partial_flat_lub_nat partia415982977_state hAPP_f1505651103t_bool hAPP_f618557131t_bool hAPP_b2019457360e_bool hAPP_n1006566506l_bool hAPP_f2073279419e_bool hAPP_f1759915619e_bool hAPP_f167292325e_bool hAPP_s58564346l_bool hAPP_state_state hAPP_s1892499976_state hAPP_f162060345e_bool hAPP_f746301080e_bool hAPP_a723219176e_bool hAPP_f1748468828l_bool hAPP_s1874344717e_bool hAPP_H1017515220l_bool hAPP_f1261923407e_bool hAPP_a1200519163e_bool hAPP_a1224971408e_bool hAPP_H226398757l_bool hAPP_s286259371e_bool hAPP_a849909144l_bool hAPP_f1951378235l_bool hAPP_s2001034685l_bool hAPP_f375255701e_bool hAPP_f963367678e_bool 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 skf1151 skf1152 skf1153 skf1154 skf1155 skf1156 skf1157 skf1158 skf1159 skf1160 skf1161 skf1162 skf1163 skf1164 skf1167 skf1168 skf1169 skf1170 skf1171 skf1172 % 0.47/0.63 Problem Properties: % 0.47/0.63 This is a full first-order problem with equality. % 0.47/0.63 SZS status GaveUp % 0.47/0.63 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.47/0.63 %------------------------------------------------------------------------------