%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PLA045+1 : TPTP v9.2.1. Bugfixed v5.5.1. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n027.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.83s 1.27s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PLA045+1 : TPTP v9.2.1. Bugfixed v5.5.1. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.36 % Computer : n027.cluster.edu % 0.17/0.36 % Model : x86_64 x86_64 % 0.17/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.36 % Memory : 8042.1875MB % 0.17/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.36 % CPULimit : 300 % 0.17/0.36 % WCLimit : 300 % 0.17/0.36 % DateTime : Thu May 7 12:57:05 EDT 2026 % 0.17/0.36 % CPUTime : % 0.17/0.36 SPASS-SCL-FOL version: % 0.17/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 2.83/1.22 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.83/1.22 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.83/1.22 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.83/1.22 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.83/1.22 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.83/1.22 Execution resolution_2 ended with status: gaveup % 2.83/1.22 Execution normal ended with status: gaveup % 2.83/1.22 Execution lmodel_grow ended with status: gaveup % 2.83/1.22 Execution resolution_3 ended with status: gaveup % 2.83/1.22 Execution resolution_1 ended with status: gaveup % 2.83/1.22 No successful execution. % 2.83/1.22 % 2.83/1.22 Input Clauses: % 2.83/1.26 % 2.83/1.26 Predicates: p = % 2.83/1.26 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 skc122 skc123 skc124 skc125 skc126 skc127 skc128 skc129 skc130 skc131 skc132 skc133 skc134 skc135 skc136 skc137 skc138 skc139 skc140 skc141 skc142 skc143 skc144 skc145 skc146 skc147 skc148 skc149 skc150 skc151 skc152 skc153 skc154 skc155 skc156 skc157 skc158 skc159 skc160 skc161 skc162 skc163 skc164 skc165 skc166 skc167 skc168 skc169 skc170 skc171 skc172 skc173 skc174 skc175 skc176 skc177 skc178 skc179 skc180 skc181 skc182 skc183 skc184 skc185 skc186 skc187 skc188 skc189 skc190 skc191 skc192 skc193 skc194 skc195 skc196 skc197 skc198 skc199 skc200 skc201 skc202 skc203 skc204 skc205 skc206 skc207 skc208 skc209 skc210 skc211 skc212 skc213 skc214 skc215 skc216 skc217 skc218 skc219 skc220 % 2.83/1.26 Fol Functions: 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 % 2.83/1.26 Problem Properties: % 2.83/1.26 This is a full first-order problem with equality. % 2.83/1.26 SZS status GaveUp % 2.83/1.26 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 2.83/1.26 %------------------------------------------------------------------------------