%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW474+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 : n002.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.58s 0.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW474+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.17/0.34 % Computer : n002.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 13:35:17 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.58/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.58/0.67 Execution normal ended with status: gaveup % 0.58/0.67 Execution resolution_1 ended with status: gaveup % 0.58/0.67 Execution resolution_2 ended with status: gaveup % 0.58/0.67 Execution lmodel_grow ended with status: gaveup % 0.58/0.67 Execution resolution_3 ended with status: gaveup % 0.58/0.67 No successful execution. % 0.58/0.67 % 0.58/0.67 Input Clauses: % 0.58/0.68 % 0.58/0.68 Predicates: is_bool is_fun_pname_bool is_fun1661590463l_bool is_pname 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 % 0.58/0.68 Fol Constants: wT_bodies finite_finite_pname pname bool hoare_298929751gleton bot_bot_bool bot_bo844097828e_bool bot_bo1649642514l_bool fFalse fTrue pn bot_bo1055319631e_bool ord_le1720872323e_bool insert1835143293_state hoare_Mirabelle_MGT body_1 the_com body finite595471783e_bool finite786885583l_bool collec1613912337l_bool cOMBC_7971162l_bool ord_le675606854l_bool finite899049100e_bool finite1586217244l_bool collec1277803610l_bool cOMBC_1084925030l_bool ord_le1076702565l_bool finite784854244_state collec111528142e_bool cOMBC_1018307482l_bool collec1974731493e_bool cOMBC_1284144636l_bool ord_le313189616e_bool insert1325755072e_bool insert1991711667e_bool insert_pname bot_bo1325454745l_bool cOMBS_350070575l_bool fconj cOMBS_2138645332l_bool collec727977250_state cOMBS_1248383340l_bool collect_pname cOMBS_568398431l_bool member1758697444_state member_pname wt fimplies fNot cOMBC_1149511130e_bool fequal_pname fequal533582459e_bool fequal1746921144e_bool cOMBC_1424981238e_bool fequal1531560888_state fdisj cOMBC_1058051404l_bool cOMBC_1988546018l_bool member799430823e_bool cOMBC_1166591542l_bool member402455436e_bool cOMBC_764456866l_bool cOMBC_2140141647l_bool cOMBC_2107548985e_bool cOMBC_1305755390e_bool cOMBC_725526061e_bool cOMBC_1004116266e_bool cOMBC_367297061e_bool cOMBC_498627897l_bool cOMBC_290948233e_bool semila447562797e_bool the_elem_pname the_el23965208_state hoare_1575745797_state semila278973382e_bool semila1782091504l_bool semila2055205435l_bool cOMBS_1615712031_state cOMBS_1401555724_state cOMBC_471052088e_bool cOMBC_231445413l_bool ord_less_eq_bool cOMBC_2027030106e_bool fequal_state insert_com bot_bot_fun_com_bool member_com semila1168014441p_bool skip cOMBC_952831051e_bool cOMBS_1378840469l_bool the_pname cOMBC_1123258281e_bool the_Ho10452358_state cOMBC_488258100e_bool fAll_state semila1130628874l_bool semila1410775201l_bool semila1635148844e_bool semila2145357127e_bool cOMBS_843273363_state cOMBS_381334199_state if_Hoa533980679_state cOMBS_904531235on_com cOMBS_1529518335on_com if_option_com minus_1015773161e_bool minus_2076558538e_bool minus_1290075917l_bool minus_164259166l_bool fa y skc1103 skc1104 skc1167 skc1168 skc1169 skc1170 skc1171 skc1172 % 0.58/0.68 Fol Functions: cOMBK_bool_pname cOMBK_1857069011e_bool finite1282449217_pname finite774711482_state finite1626890877e_bool finite132673334e_bool finite89670078_pname finite506823037_state finite1268145088e_bool finite959343283e_bool undefined_pname fun undefi17486888e_bool undefi64961550l_bool dom_pname_com some_pname set_pname hAPP_com_bool hAPP_pname_pname hAPP_pname_bool hAPP_p61793385e_bool hAPP_p338031245l_bool hAPP_state_bool hAPP_bool_bool hAPP_H1344248906_pname hAPP_H513860823e_bool hAPP_H1632039476e_bool hAPP_H737849090l_bool hAPP_f990396704l_bool hAPP_f1297739591_pname hAPP_f1664156314l_bool hAPP_f759274231e_bool hAPP_f434788991l_bool hAPP_f42430548e_bool hAPP_f327114704l_bool hAPP_f1008690464_pname hAPP_f1760790145l_bool hAPP_f1745235422e_bool hAPP_f748867288l_bool hAPP_f1935102916l_bool hAPP_f674760225e_bool hAPP_f559147733l_bool hAPP_f239102607l_bool hAPP_f280588268e_bool hAPP_f389811538l_bool hAPP_f1904669497l_bool hoare_659004819_state hAPP_f854625363l_bool hAPP_H727730819e_bool hAPP_f921536533e_bool hAPP_pname_com hAPP_c1546227244_state hAPP_p799580910on_com hAPP_option_com_com hAPP_f1879335953l_bool hAPP_f510955609l_bool hAPP_f783502055l_bool hAPP_f1508257257l_bool hAPP_f1269496639l_bool hAPP_f1987093l_bool hAPP_f2119687429l_bool hAPP_f1970439265l_bool hAPP_f1297925993l_bool image_1259634916e_bool image_277167759e_bool image_47868345e_bool image_505480954e_bool hAPP_f1874607724l_bool image_936554724_state hAPP_f780887186e_bool image_774712299_state hAPP_f772567431e_bool image_1283814551_pname image_636285904_pname image_275883510_state hAPP_f631639356e_bool hAPP_f1320879424l_bool hAPP_f601642911l_bool hAPP_p905327722e_bool cOMBB_2095475776e_bool hAPP_f143162813l_bool hAPP_f624840228l_bool cOMBB_2020112947e_bool hAPP_f482022705l_bool hAPP_f1850463605l_bool cOMBB_1382207997_state hAPP_f1558728829l_bool hAPP_f760664097e_bool cOMBB_675860798_pname hAPP_f1402196763l_bool hAPP_f649174806e_bool cOMBK_588224941_state image_1925245338_pname cOMBK_90103121_pname hAPP_H248360617l_bool some_com image_pname_pname hAPP_p1842370726_state cOMBK_564432736e_bool cOMBK_1079618832_state cOMBB_647938656_pname hAPP_f22061361e_bool cOMBB_307249310e_bool cOMBB_1957242197e_bool cOMBB_416661851_state hAPP_f262880489e_bool hAPP_H1645666623e_bool hAPP_f661147897e_bool hAPP_f1145991873l_bool hAPP_f517001763l_bool hAPP_f1262649863e_bool hAPP_f556039215l_bool hAPP_f105100493l_bool cOMBB_408569982_pname hAPP_f567934427l_bool cOMBB_44445098_pname hAPP_f2081555625l_bool hAPP_f1558052123e_bool hAPP_p877885514e_bool image_650584225_state cOMBB_291471741_state hAPP_f1844318385e_bool hAPP_H563960305_state cOMBB_1170234304e_bool hAPP_f547518321e_bool hAPP_f261382953l_bool hAPP_f1308959284_state cOMBB_1099197107e_bool hAPP_f481659057e_bool hAPP_f492098723l_bool hAPP_f2143211163_state cOMBB_542850580_pname hAPP_f1336811455e_bool cOMBB_1456120487_state hAPP_f833390165e_bool hAPP_f294904177e_bool cOMBB_598082538e_bool hAPP_f1385420507e_bool hAPP_f2082757169l_bool cOMBB_1671808265e_bool hAPP_f1973135743e_bool hAPP_f2070658331l_bool hAPP_p1617973726l_bool cOMBB_1722165949_state hAPP_f376825399l_bool hAPP_f1721106985e_bool cOMBB_1239130257_state hAPP_f1862834069l_bool cOMBB_799949246_pname hAPP_f998786331e_bool hAPP_f167506745e_bool hAPP_f1583986009e_bool cOMBB_422605457_pname hAPP_f1758910594_state cOMBB_923936821_pname hAPP_f96342628me_com hAPP_f1949912908_state hAPP_c408625258_state hAPP_f588507005_state hAPP_f1388330588e_bool hAPP_f230953622l_bool hAPP_f1587382801l_bool cOMBB_2123334001_pname hAPP_f950918952_state hAPP_f1777033564_state hAPP_f2136041130_state hAPP_f358330902_state hAPP_f1296386871_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_b589554111l_bool hAPP_s1806633685e_bool hAPP_f817621513e_bool cOMBK_631994958_state hoare_1065416081_state some_H1133819688_state set_Ho1831989999_state set_com hAPP_c566651504m_bool hAPP_f1682609283m_bool hAPP_c667411853l_bool hAPP_p1170154830_pname hAPP_H521649881_state image_2063528359e_bool image_505022149e_bool cOMBB_20296667_state hAPP_f1138284024e_bool hAPP_f915354021e_bool cOMBB_160679318_state hAPP_f1759915619e_bool hAPP_f1863945078e_bool while semi cOMBB_530759491_pname hAPP_f698292281e_bool hAPP_f180827860e_bool cOMBB_1653402815_state hAPP_f964290431e_bool hAPP_f762269719e_bool hAPP_f1456107715e_bool cOMBB_1911358915_state cOMBB_1036740637_state evalc cOMBB_1476898461_state hAPP_f249262236e_bool hAPP_f1935169308e_bool cOMBB_707293872_pname hAPP_f1405979047_state hAPP_f939130838_state hAPP_f2101567797_state hAPP_f137248406_state hAPP_f1661207211_state cOMBB_1394247784_pname hAPP_f755519727on_com hAPP_f2093196134on_com hAPP_f648377725on_com hAPP_f1673966486on_com hAPP_f2123220539on_com hAPP_b1679505845on_com hAPP_o334540577on_com hAPP_o356497025on_com hAPP_f167292325e_bool hAPP_b2019457360e_bool hAPP_s58564346l_bool hAPP_p393069232l_bool hAPP_f644196280e_bool hAPP_b798484845_state hAPP_f1259673775l_bool hAPP_f1476298914l_bool hAPP_f1012183542e_bool hAPP_s1874344717e_bool hAPP_p1086945780on_com hAPP_H226398757l_bool hAPP_s1226857760e_bool hAPP_f1508101115l_bool hAPP_s2001034685l_bool hAPP_s336103912e_bool hAPP_p1164893188on_com hAPP_p80247908_state hAPP_p1712839024_state hAPP_p2032835427_state 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 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 % 0.58/0.68 Problem Properties: % 0.58/0.68 This is a full first-order problem with equality. % 0.58/0.68 SZS status GaveUp % 0.58/0.68 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.58/0.68 %------------------------------------------------------------------------------