%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW472+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 : n017.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:19 PM UTC 2026 % Result : Unknown 0.45s 0.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW472+2 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.33 % Computer : n017.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Thu May 7 13:33:58 EDT 2026 % 0.16/0.33 % CPUTime : % 0.16/0.33 SPASS-SCL-FOL version: % 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Execution normal ended with status: gaveup % 0.45/0.63 Execution resolution_1 ended with status: gaveup % 0.45/0.63 Execution resolution_2 ended with status: gaveup % 0.45/0.63 Execution resolution_3 ended with status: gaveup % 0.45/0.63 Execution lmodel_grow ended with status: gaveup % 0.45/0.63 No successful execution. % 0.45/0.63 % 0.45/0.63 Input Clauses: % 0.45/0.63 % 0.45/0.63 Predicates: is_bool 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 % 0.45/0.63 Fol Constants: bool bot_bot_bool fFalse fTrue bot_bo1055319631e_bool insert1835143293_state member1758697444_state collec727977250_state cOMBK_1079618832_state fimplies fNot fequal1531560888_state fdisj the_el23965208_state skip finite784854244_state ord_le1720872323e_bool ord_less_eq_bool fconj ord_min_bool ord_mi777828298e_bool ord_max_bool ord_ma295552312e_bool c p q % 0.45/0.63 Fol Functions: big_se1303371297_state finite1710211309_state finite372259688_state finite1317819144e_bool finite774711482_state finite506823037_state undefined_bool hAPP_state_bool hAPP_bool_bool hAPP_H513860823e_bool hAPP_nat_bool hAPP_f1760790145l_bool hoare_659004819_state hoare_1575745797_state hoare_1065416081_state hAPP_H727730819e_bool hAPP_f921536533e_bool hAPP_s1806633685e_bool hAPP_H248360617l_bool hAPP_b1245957081e_bool cOMBB_1382207997_state cOMBB_416661851_state cOMBC_1424981238e_bool hAPP_H1645666623e_bool hAPP_f1558728829l_bool cOMBS_1248383340l_bool cOMBC_764456866l_bool hAPP_f2143211163_state semi finite9525415_state finite1346402327_state finite1935632226_state hAPP_H521649881_state hAPP_H563960305_state hAPP_f854625363l_bool hAPP_b589554111l_bool minus_2076558538e_bool minus_minus_bool hAPP_f1583986009e_bool min_bool min_fu513160078e_bool finite202520804_state finite512563852e_bool big_co272093296te_nat minus_minus_nat hAPP_H716259088te_nat hAPP_nat_nat max_bool max_fu30884092e_bool plus_plus_nat ord_le260787855e_bool ord_less_bool ord_less_nat hAPP_H226398757l_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 % 0.45/0.63 Problem Properties: % 0.45/0.63 This is a full first-order problem with equality. % 0.45/0.63 SZS status GaveUp % 0.45/0.63 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.45/0.63 %------------------------------------------------------------------------------