%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PLA044+1 : TPTP v9.2.1. Bugfixed v5.5.1. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n022.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:31:16 PM UTC 2026 % Result : Unknown 2.79s 1.20s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PLA044+1 : TPTP v9.2.1. Bugfixed v5.5.1. % 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.36 % Computer : n022.cluster.edu % 0.16/0.36 % Model : x86_64 x86_64 % 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.36 % Memory : 8042.1875MB % 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.36 % CPULimit : 300 % 0.16/0.36 % WCLimit : 300 % 0.16/0.36 % DateTime : Thu May 7 12:56:52 EDT 2026 % 0.16/0.36 % CPUTime : % 0.16/0.36 SPASS-SCL-FOL version: % 0.29/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 2.78/1.16 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.78/1.16 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.78/1.16 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.78/1.16 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.78/1.16 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.78/1.16 Execution resolution_2 ended with status: gaveup % 2.78/1.16 Execution normal ended with status: gaveup % 2.78/1.16 Execution resolution_1 ended with status: gaveup % 2.78/1.16 Execution resolution_3 ended with status: gaveup % 2.78/1.16 Execution lmodel_grow ended with status: gaveup % 2.78/1.16 No successful execution. % 2.78/1.16 % 2.78/1.16 Input Clauses: % 2.78/1.19 % 2.78/1.19 Predicates: p = % 2.78/1.19 Fol Constants: true false skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc21 skc22 skc23 skc24 skc25 skc26 skc27 skc28 skc29 skc30 skc31 skc32 skc33 skc34 skc35 skc36 skc37 skc38 skc39 skc40 skc41 skc42 skc43 skc44 skc45 skc46 skc47 skc48 skc49 skc50 skc51 skc52 skc53 skc54 skc55 skc56 skc57 skc58 skc59 skc60 skc61 skc62 skc63 skc64 skc65 skc66 skc67 skc68 skc69 skc70 skc71 skc72 skc73 skc74 skc75 skc76 skc77 skc78 skc79 skc80 skc81 skc82 skc83 skc84 skc85 skc86 skc87 skc88 skc89 skc90 skc91 skc92 skc93 skc94 skc95 skc96 skc97 skc98 skc99 skc100 skc101 skc102 skc103 skc104 skc105 skc106 skc107 skc108 skc109 skc110 skc111 skc112 skc113 skc114 skc115 skc116 skc117 skc118 skc119 skc120 skc121 % 2.78/1.19 Fol Functions: 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 skf200 skf201 skf202 skf203 skf204 skf205 skf206 skf207 skf208 skf209 skf210 skf211 skf212 skf213 skf214 skf215 skf216 skf217 skf218 skf219 skf220 skf221 skf222 skf223 skf224 skf225 skf226 skf227 skf228 skf229 skf230 skf231 skf232 skf233 skf234 skf235 skf236 skf237 skf238 skf239 skf240 skf241 skf242 skf243 skf244 skf245 skf246 skf247 skf248 skf249 skf250 skf251 skf252 skf253 skf254 skf255 skf256 skf257 skf258 skf259 skf260 skf261 skf262 skf263 skf264 skf265 skf266 skf267 skf268 skf269 skf270 skf271 skf272 skf273 skf274 skf275 skf276 skf277 skf278 skf279 skf280 skf281 skf282 skf283 skf284 skf285 skf286 skf287 skf288 skf289 skf290 skf291 skf292 skf293 skf294 skf295 skf296 skf297 skf298 skf299 skf300 skf301 skf302 skf303 skf304 skf305 skf306 skf307 skf308 skf309 skf310 skf311 skf312 skf313 skf314 skf315 skf316 skf317 skf318 skf319 skf320 skf321 skf322 skf323 skf324 skf325 skf326 skf327 skf328 skf329 skf330 skf331 skf332 skf333 skf334 skf335 skf336 skf337 skf338 skf339 skf340 skf341 skf342 skf343 skf344 skf345 skf346 skf347 skf348 skf349 skf350 skf351 skf352 % 2.78/1.19 Problem Properties: % 2.78/1.19 This is a full first-order problem with equality. % 2.78/1.19 SZS status GaveUp % 2.78/1.19 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 2.78/1.19 %------------------------------------------------------------------------------