%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW471+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 : n005.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.55s 0.61s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW471+2 : TPTP v9.2.1. Released v5.3.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n005.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:16 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.55/0.59 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.59 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.59 Execution normal ended with status: gaveup % 0.55/0.59 Execution resolution_1 ended with status: gaveup % 0.55/0.59 Execution resolution_2 ended with status: gaveup % 0.55/0.59 Execution resolution_3 ended with status: gaveup % 0.55/0.59 Execution lmodel_grow ended with status: gaveup % 0.55/0.59 No successful execution. % 0.55/0.59 % 0.55/0.59 Input Clauses: % 0.55/0.60 % 0.55/0.60 Predicates: is_fun_bool_bool is_bool is_fun1661590463l_bool is_fun_pname_bool is_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 % 0.55/0.60 Fol Constants: finite_finite_pname pname bool bot_bot_bool bot_bo844097828e_bool bot_bo806936373l_bool bot_bo1649642514l_bool fFalse fNot fTrue procs hoare_1760757500iple_a hoare_1575745797_state member1758697444_state member1713797107iple_a semila447562797e_bool cOMBS_1615712031_state cOMBS_1401555724_state body the_com body_1 semila1498788770a_bool cOMBS_260455419iple_a cOMBS_2104302062iple_a member_pname semila278973382e_bool semila1168014441p_bool collec727977250_state cOMBS_1248383340l_bool fdisj cOMBC_764456866l_bool collec268032053iple_a cOMBS_1148211387l_bool cOMBC_1552014468l_bool collect_pname cOMBS_568398431l_bool cOMBC_1058051404l_bool insert1835143293_state bot_bo1055319631e_bool insert873085594iple_a bot_bo1181479936a_bool zero_zero_nat insert_pname cOMBK_151824839iple_a cOMBK_bool_pname cOMBK_1079618832_state fequal1531560888_state fequal879838495iple_a fequal_pname cOMBC_1424981238e_bool cOMBC_839220826a_bool cOMBC_1149511130e_bool fconj fimplies cOMBK_90103121_pname cOMBK_1347789874_pname cOMBK_pname_pname cOMBC_41962815e_bool cOMBC_231445413l_bool cOMBC_471052088e_bool cOMBK_1458035955bool_a cOMBC_2027030106e_bool fequal_state cOMBK_631994958_state the_el23965208_state the_el1436340927iple_a the_elem_pname bot_bot_nat skip cOMBC_952831051e_bool cOMBS_1378840469l_bool cOMBC_892787026e_bool the_Ho10452358_state fequal1746921144e_bool cOMBC_488258100e_bool the_Ho746640593iple_a fequal1258664663a_bool cOMBC_708118077a_bool the_pname fequal533582459e_bool cOMBC_1123258281e_bool finite784854244_state finite1655202547iple_a cOMBC_290948233e_bool cOMBC_1693967286a_bool cOMBC_173904839e_bool cOMBC_1527561185a_bool finite_finite_bool semila1866150931l_bool finite595471783e_bool semila1782091504l_bool finite899049100e_bool bot_bo1325454745l_bool semila2055205435l_bool finite652815363a_bool bot_bo1325387246l_bool semila1827648460l_bool member_bool member799430823e_bool member402455436e_bool member1154012931a_bool insert_bool insert1325755072e_bool insert1991711667e_bool insert1805675420a_bool cOMBS_843273363_state cOMBS_381334199_state if_Hoa533980679_state cOMBS_1128650103iple_a cOMBS_546756116iple_a if_Hoa638970256iple_a cOMBI_nat one_one_nat g p q n skc1152 skc1153 skc1154 skc1155 skc1156 skc1157 skc1158 skc1159 skc1166 skc1167 skc1168 skc1169 skc1170 skc1171 skc1172 skc1173 skc1174 skc1175 skc1176 skc1177 skc1178 skc1179 skc1180 skc1181 skc1182 skc1183 skc1184 skc1185 skc1186 skc1187 skc1188 skc1189 skc1192 % 0.55/0.60 Fol Functions: big_la472677547n_bool big_la28065288e_bool big_la1480321694n_bool big_la841148155e_bool finite1282449217_pname finite1669978781iple_a finite774711482_state finite89670078_pname finite950012314iple_a finite506823037_state undefined_pname undefined_bool fun undefi17486888e_bool semila310582991f_bool hAPP_pname_pname hAPP_pname_bool hAPP_p61793385e_bool hAPP_p393069232l_bool hAPP_p338031245l_bool hAPP_state_bool hAPP_s58564346l_bool hAPP_bool_bool hAPP_b76515610e_bool hAPP_b589554111l_bool hAPP_H676960377_pname hAPP_H1421470952a_bool hAPP_H1991058245e_bool hAPP_H1017515220l_bool hAPP_H513860823e_bool hAPP_H1632039476e_bool hAPP_H226398757l_bool hAPP_nat_bool hAPP_f1297739591_pname hAPP_f1664156314l_bool hAPP_f759274231e_bool hAPP_f434788991l_bool hAPP_f42430548e_bool hAPP_f387058535l_bool hAPP_f961197973l_bool hAPP_f540970102l_bool hAPP_f1126670547e_bool hAPP_f1760790145l_bool hAPP_f1935102916l_bool hAPP_f559147733l_bool hAPP_f1557928608l_bool hAPP_f239102607l_bool hAPP_f1807945453iple_a hAPP_c1407587404iple_a hAPP_f150255961iple_a hAPP_f1949912908_state hAPP_c408625258_state hAPP_f588507005_state hoare_1065416081_state hAPP_H248360617l_bool hoare_592710359_state hoare_943851888lids_a hAPP_H1840393229l_bool hoare_560051114alid_a hAPP_f1583986009e_bool cOMBB_2123334001_pname hAPP_f950918952_state hAPP_f1777033564_state hAPP_f2136041130_state hAPP_f358330902_state hAPP_f1296386871_state image_275883510_state hAPP_f631639356e_bool hAPP_f921536533e_bool hoare_659004819_state cOMBB_923936821_pname hAPP_f96342628me_com hAPP_f1026156344a_bool cOMBB_109684016_pname hAPP_f1504849325iple_a hAPP_f1139368540iple_a hAPP_f773999884iple_a hAPP_f1821846428iple_a hAPP_f79369369iple_a image_1654749281iple_a hAPP_f271130963a_bool hAPP_f1591852335a_bool hoare_606018542rivs_a hAPP_f1388330588e_bool hAPP_p1842370726_state image_2068426537_pname hAPP_p263283121iple_a image_1604514514_state hAPP_f1182387808e_bool image_129517430iple_a hAPP_f75870650a_bool cOMBB_1382207997_state hAPP_f1262649863e_bool hAPP_f1558728829l_bool hAPP_f760664097e_bool cOMBB_1782929690iple_a hAPP_f672239281a_bool hAPP_f997599971l_bool hAPP_f1203760810a_bool cOMBB_675860798_pname hAPP_f661147897e_bool hAPP_f1402196763l_bool hAPP_f649174806e_bool cOMBB_2118237115_pname hAPP_f1026488024_state cOMBB_2015474199_pname hAPP_f113652738iple_a hAPP_p799580910on_com hAPP_option_com_com suc hAPP_pname_com hAPP_p1637813682e_bool hAPP_H727730819e_bool hAPP_p635540397e_bool hAPP_H1641355846a_bool evalc hAPP_s1806633685e_bool hAPP_p905327722e_bool hAPP_b119575286a_bool hAPP_b1245957081e_bool hAPP_H1645666623e_bool hAPP_H1190454433a_bool hAPP_f262880489e_bool hAPP_f1371755681a_bool hAPP_f22061361e_bool cOMBB_416661851_state cOMBB_1799513916iple_a cOMBB_647938656_pname hAPP_H1797237070_state hAPP_H1578029518iple_a hAPP_p1170154830_pname image_pname_pname cOMBB_1348041619bool_a cOMBB_188601460_state cOMBB_1355796797bool_a hAPP_f1509969235l_bool hAPP_f340725611e_bool hAPP_f1824947087e_bool hAPP_b540892988e_bool cOMBB_1757942702_state cOMBB_1759179140_state hAPP_f1283379615l_bool hAPP_f873506917e_bool hAPP_f701449317e_bool hAPP_b1095269219e_bool hAPP_a2036067514e_bool hAPP_f817621513e_bool hAPP_f762886889e_bool hAPP_f1863945078e_bool hoare_1674107620_state hoare_953425885size_a hoare_Mirabelle_MGT size_s346246881_state size_s315943222iple_a hAPP_f2143211163_state hAPP_f124283079iple_a evaln cOMBB_20296667_state hAPP_f1138284024e_bool hAPP_f915354021e_bool cOMBB_160679318_state hAPP_f1759915619e_bool while cOMBB_145932198bool_a hAPP_f963367678e_bool hAPP_f1261923407e_bool semi hAPP_f854625363l_bool cOMBB_1653402815_state hAPP_f964290431e_bool hAPP_f762269719e_bool hAPP_f1456107715e_bool hAPP_f430043647l_bool cOMBB_1501709507iple_a hAPP_f549683569a_bool hAPP_f1665407592a_bool hAPP_f772297704a_bool cOMBB_530759491_pname hAPP_f698292281e_bool hAPP_f180827860e_bool cOMBB_799949246_pname hAPP_f998786331e_bool hAPP_f167506745e_bool cOMBB_858699740_pname hAPP_f1311175287a_bool hAPP_f687460073e_bool hAPP_H1455657330iple_a hAPP_H678412245iple_a hAPP_H521649881_state hAPP_H563960305_state cOMBB_557071226_pname hAPP_f1191449183e_bool hAPP_f1505732693e_bool hAPP_f621094798e_bool finite216774046_pname cOMBB_1191710871_pname hAPP_f1728520198a_bool hAPP_f2022238777a_bool hAPP_f1646799884a_bool finite979333485_pname image_306007685iple_a image_650584225_state hAPP_f1172769267l_bool hAPP_f230953622l_bool hAPP_f1587382801l_bool hAPP_f1970439265l_bool big_la1640362552e_bool hAPP_f997688506l_bool hAPP_f960623701l_bool big_la1993344855a_bool hAPP_b1787118453l_bool hAPP_f556039215l_bool hAPP_f105100493l_bool hAPP_f1849264231l_bool hAPP_b496459037l_bool hAPP_f1320879424l_bool hAPP_f601642911l_bool hAPP_f1556354660l_bool image_bool_bool image_2063528359e_bool image_505022149e_bool image_119931871a_bool semila1551573549l_bool semila1130628874l_bool semila1410775201l_bool semila1746965734l_bool semila671163144a_bool semila1635148844e_bool semila2145357127e_bool cOMBB_707293872_pname hAPP_f1405979047_state hAPP_f939130838_state hAPP_f2101567797_state hAPP_f137248406_state hAPP_f1661207211_state cOMBB_1916528323_pname hAPP_f653022294iple_a hAPP_f428084316iple_a hAPP_f866544818iple_a hAPP_f1401255196iple_a hAPP_f1044063253iple_a big_la508066411e_bool big_la1164677860a_bool minus_469558085a_bool minus_1015773161e_bool minus_2076558538e_bool minus_minus_nat hAPP_nat_nat nat_case_nat plus_plus_nat com_size size_size_com cond hAPP_b385840250iple_a hAPP_f167292325e_bool hAPP_b2019457360e_bool hAPP_f644196280e_bool hAPP_b798484845_state hAPP_a723219176e_bool hAPP_f1259673775l_bool hAPP_s1874344717e_bool hAPP_p2127663045a_bool hAPP_a1200519163e_bool hAPP_p877885514e_bool hAPP_s1226857760e_bool hAPP_a849909144l_bool hAPP_p363087182iple_a hAPP_s2001034685l_bool hAPP_p344936018iple_a hAPP_H928324994_state hAPP_H1600811558iple_a hAPP_p80247908_state hAPP_p1712839024_state hAPP_p1263586117iple_a hAPP_p54391842a_bool hAPP_p2032835427_state hAPP_p321057131iple_a hAPP_p1682965390e_bool hAPP_p964374716_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 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 skf1160 skf1161 skf1162 skf1163 skf1164 skf1165 skf1190 skf1191 % 0.55/0.60 Problem Properties: % 0.55/0.60 This is a full first-order problem with equality. % 0.55/0.60 SZS status GaveUp % 0.55/0.60 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.55/0.60 %------------------------------------------------------------------------------