%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYO581+1 : TPTP v9.2.1. Released v5.5.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n029.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:41:09 PM UTC 2026 % Result : CounterSatisfiable 31.43s 6.89s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SYO581+1 : TPTP v9.2.1. Released v5.5.0. % 0.11/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.35 % Computer : n029.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Thu May 7 13:55:30 EDT 2026 % 0.16/0.35 % CPUTime : % 0.16/0.35 SPASS-SCL-FOL version: % 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 31.43/6.88 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.43/6.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.43/6.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.43/6.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.43/6.88 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.43/6.88 Execution lmodel_grow ended with status: satisfiable % 31.43/6.88 Used heuristic: lmodel_grow % 31.43/6.88 % 31.43/6.88 Input Clauses: % 31.43/6.88 % 31.43/6.88 Predicates: k04_buttercup10049 k04_buttercup10048 k04_buttercup10051 k04_buttercup10096 k04_buttercup10095 k04_buttercup10097 k04_buttercup10342 k04_buttercup10337 k04_buttercup10347 k04_buttercup10351 k04_buttercup10453 k04_buttercup10449 k04_buttercup10462 k04_buttercup10464 k04_buttercup10482 k04_buttercup10477 k04_buttercup10486 k04_buttercup10546 k04_buttercup10544 k04_buttercup10547 k04_buttercup10406 k04_buttercup10404 k04_buttercup10408 k04_buttercup10599 k04_buttercup10593 k04_buttercup10602 k04_buttercup10236 k04_buttercup10234 k04_buttercup10238 k04_buttercup10371 k04_buttercup10369 k04_buttercup10373 k04_buttercup10376 k04_buttercup10296 k04_buttercup10293 k04_buttercup10298 k04_buttercup10637 k04_buttercup10635 k04_buttercup10639 k04_buttercup10641 k04_buttercup10028 k04_buttercup10026 k04_buttercup10033 k04_buttercup10425 k04_buttercup10424 k04_buttercup10206 k04_buttercup10204 k04_buttercup10213 k04_buttercup10219 k04_buttercup10061 k04_buttercup10057 k04_buttercup10064 k04_buttercup10067 k04_buttercup10074 k04_buttercup10559 k04_buttercup10555 k04_buttercup10620 k04_buttercup10619 k04_buttercup10622 k04_buttercup10506 k04_buttercup10504 k04_buttercup10142 k04_buttercup10139 k04_buttercup10517 k04_buttercup10516 k04_buttercup10184 k04_buttercup10012 k04_buttercup10190 k04_buttercup10200 k04_buttercup10221 k04_buttercup10225 k04_buttercup10244 k04_buttercup10252 k04_buttercup10282 k04_buttercup10303 k04_buttercup10312 k04_buttercup10316 k04_buttercup10325 k04_buttercup10329 k04_buttercup10333 k04_buttercup10356 k04_buttercup10016 k04_buttercup10039 k04_buttercup10053 k04_buttercup10079 k04_buttercup10084 k04_buttercup10089 k04_buttercup10100 k04_buttercup10117 k04_buttercup10125 k04_buttercup10132 k04_buttercup10135 k04_buttercup10147 k04_buttercup10153 k04_buttercup10164 k04_buttercup10172 k04_buttercup10181 k04_buttercup10364 k04_buttercup10380 k04_buttercup10382 k04_buttercup10385 k04_buttercup10389 k04_buttercup10391 k04_buttercup10397 k04_buttercup10400 k04_buttercup10415 k04_buttercup10419 k04_buttercup10430 k04_buttercup10437 k04_buttercup10445 k04_buttercup10470 k04_buttercup10473 k04_buttercup10492 k04_buttercup10495 k04_buttercup10499 k04_buttercup10510 k04_buttercup10524 k04_buttercup10529 k04_buttercup10535 k04_buttercup10551 k04_buttercup10567 k04_buttercup10578 k04_buttercup10581 k04_buttercup10586 k04_buttercup10608 k04_buttercup10611 k04_buttercup10626 k04_buttercup10628 k04_buttercup10631 k04_buttercup10643 b48_buttercup10050 b48_buttercup10046 b48_buttercup10052 b48_buttercup10305 b48_buttercup10300 b48_buttercup10307 b48_buttercup10308 b48_buttercup10227 b48_buttercup10222 b48_buttercup10228 b48_buttercup10229 b48_buttercup10191 b48_buttercup10186 b48_buttercup10193 b48_buttercup10195 b48_buttercup10133 b48_buttercup10130 b48_buttercup10134 b48_buttercup10343 b48_buttercup10334 b48_buttercup10344 b48_buttercup10348 b48_buttercup10352 b48_buttercup10267 b48_buttercup10266 b48_buttercup10268 b48_buttercup10102 b48_buttercup10098 b48_buttercup10104 b48_buttercup10107 b48_buttercup10108 b48_buttercup10109 b48_buttercup10110 b48_buttercup10111 b48_buttercup10441 b48_buttercup10440 b48_buttercup10442 b48_buttercup10478 b48_buttercup10474 b48_buttercup10479 b48_buttercup10483 b48_buttercup10487 b48_buttercup10489 b48_buttercup10545 b48_buttercup10542 b48_buttercup10548 b48_buttercup10275 b48_buttercup10274 b48_buttercup10276 b48_buttercup10277 b48_buttercup10278 b48_buttercup10405 b48_buttercup10402 b48_buttercup10410 b48_buttercup10166 b48_buttercup10161 b48_buttercup10167 b48_buttercup10169 b48_buttercup10119 b48_buttercup10115 b48_buttercup10120 b48_buttercup10596 b48_buttercup10589 b48_buttercup10604 b48_buttercup10370 b48_buttercup10367 b48_buttercup10374 b48_buttercup10377 b48_buttercup10294 b48_buttercup10291 b48_buttercup10299 b48_buttercup10318 b48_buttercup10313 b48_buttercup10320 b48_buttercup10173 b48_buttercup10170 b48_buttercup10174 b48_buttercup10636 b48_buttercup10632 b48_buttercup10638 b48_buttercup10640 b48_buttercup10029 b48_buttercup10024 b48_buttercup10031 b48_buttercup10034 b48_buttercup10574 b48_buttercup10563 b48_buttercup10154 b48_buttercup10150 b48_buttercup10156 b48_buttercup10158 b48_buttercup10159 b48_buttercup10160 b48_buttercup10208 b48_buttercup10201 b48_buttercup10210 b48_buttercup10214 b48_buttercup10217 b48_buttercup10220 b48_buttercup10513 b48_buttercup10512 b48_buttercup10514 b48_buttercup10058 b48_buttercup10054 b48_buttercup10065 b48_buttercup10068 b48_buttercup10070 b48_buttercup10072 b48_buttercup10075 b48_buttercup10561 b48_buttercup10552 b48_buttercup10562 b48_buttercup10518 b48_buttercup10515 b48_buttercup10519 b48_buttercup10520 b48_buttercup10521 b48_buttercup10273 b48_buttercup10271 b48_buttercup10007 b48_buttercup10196 b48_buttercup10197 b48_buttercup10198 b48_buttercup10199 b48_buttercup10231 b48_buttercup10240 b48_buttercup10247 b48_buttercup10248 b48_buttercup10269 b48_buttercup10272 b48_buttercup10279 b48_buttercup10309 b48_buttercup10322 b48_buttercup10326 b48_buttercup10332 b48_buttercup10353 b48_buttercup10362 b48_buttercup10013 b48_buttercup10035 b48_buttercup10076 b48_buttercup10082 b48_buttercup10085 b48_buttercup10086 b48_buttercup10092 b48_buttercup10121 b48_buttercup10143 b48_buttercup10176 b48_buttercup10180 b48_buttercup10182 b48_buttercup10365 b48_buttercup10378 b48_buttercup10381 b48_buttercup10383 b48_buttercup10386 b48_buttercup10394 b48_buttercup10398 b48_buttercup10411 b48_buttercup10417 b48_buttercup10420 b48_buttercup10427 b48_buttercup10433 b48_buttercup10434 b48_buttercup10443 b48_buttercup10446 b48_buttercup10450 b48_buttercup10469 b48_buttercup10471 b48_buttercup10490 b48_buttercup10493 b48_buttercup10496 b48_buttercup10502 b48_buttercup10507 b48_buttercup10522 b48_buttercup10526 b48_buttercup10530 b48_buttercup10531 b48_buttercup10549 b48_buttercup10570 b48_buttercup10572 b48_buttercup10575 b48_buttercup10579 b48_buttercup10582 b48_buttercup10605 b48_buttercup10606 b48_buttercup10609 b48_buttercup10612 b48_buttercup10616 b48_buttercup10624 b48_buttercup10629 b48_buttercup10642 b48_buttercup10646 b48_buttercup10465 b48_buttercup10466 b48_buttercup10467 b48_buttercup10456 b48_buttercup10458 b48_buttercup10022 b48_buttercup10021 b48_buttercup10019 k04_buttercup10288 b48_buttercup10290 k04_buttercup10357 b48_buttercup10361 b48_buttercup10289 b48_buttercup10421 b48_buttercup10454 b48_buttercup10460 b48_buttercup10179 k04_buttercup10004 k04_buttercup10286 b48_buttercup10283 k04_buttercup10000 k04_buttercup10360 b48_buttercup10359 k04_buttercup10540 b48_buttercup10541 k04_buttercup10539 b48_buttercup10538 b48_buttercup10451 k04_buttercup10044 b48_buttercup10043 k04_buttercup10042 b48_buttercup10045 b48_buttercup10261 k04_buttercup10259 k04_buttercup10255 b48_buttercup10253 b48_buttercup10260 b48_buttercup10422 b48_buttercup10358 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 % 31.43/6.88 Fol Constants: 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 skc221 skc222 skc223 skc224 skc225 skc226 skc227 skc228 skc229 skc230 skc231 skc232 skc233 skc234 skc235 skc236 skc237 skc238 skc239 skc240 skc241 skc242 skc243 skc244 skc245 skc246 skc247 skc248 skc249 skc250 skc251 skc252 skc253 skc254 skc255 skc256 skc257 skc258 skc259 skc260 skc261 skc262 skc263 skc264 skc265 skc266 skc267 skc268 skc269 skc270 skc271 skc272 skc273 skc274 skc275 skc276 skc277 skc278 skc279 skc280 skc281 skc282 skc283 skc284 skc285 skc286 skc287 skc288 skc289 skc290 skc291 skc292 skc293 skc294 skc295 skc296 skc297 skc298 skc299 skc300 skc301 skc302 skc303 skc304 skc305 skc306 skc307 skc308 skc309 skc310 skc311 skc312 skc313 skc314 skc315 skc316 skc317 skc318 skc319 skc320 skc321 skc322 skc323 skc324 skc325 skc326 skc327 skc328 skc329 skc330 skc331 skc332 skc333 skc334 skc335 skc336 skc337 skc338 skc339 skc340 skc341 skc342 skc343 skc344 skc345 skc346 skc347 skc348 skc349 skc350 skc351 skc352 skc353 skc354 skc355 skc356 skc357 skc358 skc359 skc360 skc361 skc362 skc363 skc364 skc365 skc366 skc367 skc368 skc369 skc370 skc371 skc372 skc373 skc374 skc375 skc376 skc377 skc378 skc379 skc380 skc381 skc382 skc383 skc384 skc385 skc386 skc387 skc388 skc389 skc390 skc391 skc392 skc393 skc394 skc395 skc396 skc397 skc398 skc399 skc400 skc401 skc402 skc403 skc404 skc405 skc406 skc407 skc408 skc409 skc410 skc411 skc412 skc413 skc414 skc415 skc416 skc417 skc418 skc419 skc420 skc421 skc422 skc423 skc424 skc425 skc426 skc427 skc428 skc429 skc430 skc431 skc432 skc433 skc434 skc435 skc436 skc437 skc438 skc439 skc440 skc441 skc442 skc443 skc444 skc445 skc446 skc447 skc448 skc449 skc450 skc451 skc452 skc453 skc454 skc455 skc456 skc457 skc458 skc459 skc460 skc461 skc462 skc463 skc464 skc465 skc466 skc467 skc468 skc469 skc470 skc471 skc472 skc473 skc474 skc475 skc476 skc477 skc478 skc479 skc480 skc481 skc482 skc483 skc484 skc485 skc486 skc487 skc488 skc489 skc490 skc491 skc492 skc493 skc494 skc495 skc496 skc497 skc498 skc499 skc500 skc501 skc502 skc503 skc504 skc505 skc506 skc507 skc508 skc509 skc510 skc511 skc512 skc513 % 31.43/6.88 Fol Functions: % 31.43/6.88 Problem Properties: % 31.43/6.88 This is a Bernays Schoenfinkel problem. % 31.43/6.88 % 31.43/6.88 After reduction: Problem Properties: % 31.43/6.88 This is a Bernays Schoenfinkel problem. % 31.43/6.88 % 31.43/6.88 % 31.43/6.88 Reduced Input Clauses: % 31.43/6.89 1326:1:0:[320.1,1320.1]:: b48_buttercup10305(skc511) -> % 31.43/6.89 1327:1:0:[320.0,1321.0]:: -> k04_buttercup10303(skc511) % 31.43/6.89 % 31.43/6.89 Most General Atoms: k04_buttercup10049(x0) k04_buttercup10048(x0) k04_buttercup10051(x0) k04_buttercup10096(x0) k04_buttercup10095(x0) k04_buttercup10097(x0) k04_buttercup10342(x0) k04_buttercup10337(x0) k04_buttercup10347(x0) k04_buttercup10351(x0) k04_buttercup10453(x0) k04_buttercup10449(x0) k04_buttercup10462(x0) k04_buttercup10464(x0) k04_buttercup10482(x0) k04_buttercup10477(x0) k04_buttercup10486(x0) k04_buttercup10546(x0) k04_buttercup10544(x0) k04_buttercup10547(x0) k04_buttercup10406(x0) k04_buttercup10404(x0) k04_buttercup10408(x0) k04_buttercup10599(x0) k04_buttercup10593(x0) k04_buttercup10602(x0) k04_buttercup10236(x0) k04_buttercup10234(x0) k04_buttercup10238(x0) k04_buttercup10371(x0) k04_buttercup10369(x0) k04_buttercup10373(x0) k04_buttercup10376(x0) k04_buttercup10296(x0) k04_buttercup10293(x0) k04_buttercup10298(x0) k04_buttercup10637(x0) k04_buttercup10635(x0) k04_buttercup10639(x0) k04_buttercup10641(x0) k04_buttercup10028(x0) k04_buttercup10033(x0) k04_buttercup10425(x0) k04_buttercup10424(x0) k04_buttercup10206(x0) k04_buttercup10213(x0) k04_buttercup10219(x0) k04_buttercup10061(x0) k04_buttercup10057(x0) k04_buttercup10064(x0) k04_buttercup10067(x0) k04_buttercup10074(x0) k04_buttercup10559(x0) k04_buttercup10555(x0) k04_buttercup10620(x0) k04_buttercup10622(x0) k04_buttercup10506(x0) k04_buttercup10504(x0) k04_buttercup10142(x0) k04_buttercup10139(x0) k04_buttercup10517(x0) k04_buttercup10516(x0) k04_buttercup10184(x0) k04_buttercup10012(x0) k04_buttercup10190(x0) k04_buttercup10200(x0) k04_buttercup10221(x0) k04_buttercup10225(x0) k04_buttercup10244(x0) k04_buttercup10252(x0) k04_buttercup10303(x0) k04_buttercup10312(x0) k04_buttercup10316(x0) k04_buttercup10325(x0) k04_buttercup10329(x0) k04_buttercup10333(x0) k04_buttercup10356(x0) k04_buttercup10016(x0) k04_buttercup10039(x0) k04_buttercup10053(x0) k04_buttercup10079(x0) k04_buttercup10084(x0) k04_buttercup10089(x0) k04_buttercup10117(x0) k04_buttercup10125(x0) k04_buttercup10132(x0) k04_buttercup10135(x0) k04_buttercup10147(x0) k04_buttercup10153(x0) k04_buttercup10164(x0) k04_buttercup10172(x0) k04_buttercup10181(x0) k04_buttercup10364(x0) k04_buttercup10380(x0) k04_buttercup10382(x0) k04_buttercup10385(x0) k04_buttercup10389(x0) k04_buttercup10391(x0) k04_buttercup10397(x0) k04_buttercup10400(x0) k04_buttercup10415(x0) k04_buttercup10430(x0) k04_buttercup10437(x0) k04_buttercup10445(x0) k04_buttercup10470(x0) k04_buttercup10473(x0) k04_buttercup10492(x0) k04_buttercup10495(x0) k04_buttercup10499(x0) k04_buttercup10510(x0) k04_buttercup10524(x0) k04_buttercup10529(x0) k04_buttercup10535(x0) k04_buttercup10551(x0) k04_buttercup10567(x0) k04_buttercup10578(x0) k04_buttercup10581(x0) k04_buttercup10586(x0) k04_buttercup10608(x0) k04_buttercup10611(x0) k04_buttercup10626(x0) k04_buttercup10628(x0) k04_buttercup10631(x0) k04_buttercup10643(x0) b48_buttercup10050(x0) b48_buttercup10046(x0) b48_buttercup10052(x0) b48_buttercup10305(x0) b48_buttercup10300(x0) b48_buttercup10307(x0) b48_buttercup10308(x0) b48_buttercup10227(x0) b48_buttercup10222(x0) b48_buttercup10228(x0) b48_buttercup10229(x0) b48_buttercup10191(x0) b48_buttercup10186(x0) b48_buttercup10193(x0) b48_buttercup10195(x0) b48_buttercup10133(x0) b48_buttercup10130(x0) b48_buttercup10134(x0) b48_buttercup10343(x0) b48_buttercup10334(x0) b48_buttercup10344(x0) b48_buttercup10348(x0) b48_buttercup10352(x0) b48_buttercup10267(x0) b48_buttercup10266(x0) b48_buttercup10268(x0) b48_buttercup10098(x0) b48_buttercup10441(x0) b48_buttercup10440(x0) b48_buttercup10442(x0) b48_buttercup10478(x0) b48_buttercup10474(x0) b48_buttercup10479(x0) b48_buttercup10483(x0) b48_buttercup10487(x0) b48_buttercup10489(x0) b48_buttercup10545(x0) b48_buttercup10542(x0) b48_buttercup10548(x0) b48_buttercup10275(x0) b48_buttercup10274(x0) b48_buttercup10276(x0) b48_buttercup10277(x0) b48_buttercup10278(x0) b48_buttercup10405(x0) b48_buttercup10402(x0) b48_buttercup10410(x0) b48_buttercup10166(x0) b48_buttercup10161(x0) b48_buttercup10167(x0) b48_buttercup10169(x0) b48_buttercup10119(x0) b48_buttercup10115(x0) b48_buttercup10120(x0) b48_buttercup10596(x0) b48_buttercup10589(x0) b48_buttercup10604(x0) b48_buttercup10370(x0) b48_buttercup10367(x0) b48_buttercup10374(x0) b48_buttercup10377(x0) b48_buttercup10294(x0) b48_buttercup10291(x0) b48_buttercup10299(x0) b48_buttercup10318(x0) b48_buttercup10313(x0) b48_buttercup10320(x0) b48_buttercup10173(x0) b48_buttercup10170(x0) b48_buttercup10174(x0) b48_buttercup10636(x0) b48_buttercup10632(x0) b48_buttercup10638(x0) b48_buttercup10640(x0) b48_buttercup10024(x0) b48_buttercup10031(x0) b48_buttercup10034(x0) b48_buttercup10574(x0) b48_buttercup10563(x0) b48_buttercup10154(x0) b48_buttercup10150(x0) b48_buttercup10156(x0) b48_buttercup10158(x0) b48_buttercup10159(x0) b48_buttercup10160(x0) b48_buttercup10201(x0) b48_buttercup10210(x0) b48_buttercup10217(x0) b48_buttercup10220(x0) b48_buttercup10513(x0) b48_buttercup10512(x0) b48_buttercup10514(x0) b48_buttercup10058(x0) b48_buttercup10054(x0) b48_buttercup10065(x0) b48_buttercup10068(x0) b48_buttercup10070(x0) b48_buttercup10072(x0) b48_buttercup10075(x0) b48_buttercup10561(x0) b48_buttercup10552(x0) b48_buttercup10562(x0) b48_buttercup10518(x0) b48_buttercup10515(x0) b48_buttercup10519(x0) b48_buttercup10520(x0) b48_buttercup10521(x0) b48_buttercup10273(x0) b48_buttercup10271(x0) b48_buttercup10007(x0) b48_buttercup10196(x0) b48_buttercup10197(x0) b48_buttercup10198(x0) b48_buttercup10199(x0) b48_buttercup10231(x0) b48_buttercup10240(x0) b48_buttercup10247(x0) b48_buttercup10248(x0) b48_buttercup10269(x0) b48_buttercup10272(x0) b48_buttercup10279(x0) b48_buttercup10309(x0) b48_buttercup10322(x0) b48_buttercup10326(x0) b48_buttercup10332(x0) b48_buttercup10353(x0) b48_buttercup10362(x0) b48_buttercup10013(x0) b48_buttercup10035(x0) b48_buttercup10076(x0) b48_buttercup10082(x0) b48_buttercup10085(x0) b48_buttercup10086(x0) b48_buttercup10092(x0) b48_buttercup10121(x0) b48_buttercup10143(x0) b48_buttercup10176(x0) b48_buttercup10180(x0) b48_buttercup10182(x0) b48_buttercup10365(x0) b48_buttercup10378(x0) b48_buttercup10381(x0) b48_buttercup10383(x0) b48_buttercup10386(x0) b48_buttercup10394(x0) b48_buttercup10398(x0) b48_buttercup10411(x0) b48_buttercup10417(x0) b48_buttercup10420(x0) b48_buttercup10427(x0) b48_buttercup10433(x0) b48_buttercup10434(x0) b48_buttercup10443(x0) b48_buttercup10446(x0) b48_buttercup10450(x0) b48_buttercup10469(x0) b48_buttercup10471(x0) b48_buttercup10490(x0) b48_buttercup10493(x0) b48_buttercup10496(x0) b48_buttercup10502(x0) b48_buttercup10507(x0) b48_buttercup10522(x0) b48_buttercup10526(x0) b48_buttercup10530(x0) b48_buttercup10531(x0) b48_buttercup10549(x0) b48_buttercup10570(x0) b48_buttercup10572(x0) b48_buttercup10575(x0) b48_buttercup10579(x0) b48_buttercup10582(x0) b48_buttercup10605(x0) b48_buttercup10606(x0) b48_buttercup10609(x0) b48_buttercup10612(x0) b48_buttercup10616(x0) b48_buttercup10624(x0) b48_buttercup10629(x0) b48_buttercup10642(x0) b48_buttercup10646(x0) b48_buttercup10465(x0) b48_buttercup10466(x0) b48_buttercup10467(x0) b48_buttercup10456(x0) ren1(x0,x1,x2) k04_buttercup10026(x2) b48_buttercup10029(x2) ren2 ren3 b48_buttercup10022(x0) b48_buttercup10021(x0) b48_buttercup10019(x0) k04_buttercup10288(x0) b48_buttercup10290(x0) ren4(x0,x1,x2) k04_buttercup10619(x2) b48_buttercup10111(x2) ren5 ren6 ren7(x0,x1,x2) b48_buttercup10109(x2) ren8 ren9 ren10(x0,x1,x2) k04_buttercup10100(x2) b48_buttercup10108(x2) ren11 ren12 ren13(x0,x1,x2) b48_buttercup10107(x2) ren14 ren15 ren16(x0,x1,x2) b48_buttercup10104(x2) ren17 ren18 ren19(x0,x1,x2) b48_buttercup10110(x2) ren20 ren21 k04_buttercup10357(x0) b48_buttercup10361(x0) ren22(x0,x1,x2) k04_buttercup10204(x2) b48_buttercup10214(x2) ren23 ren24 ren25(x0,x1,x2) b48_buttercup10208(x2) ren26 ren27 b48_buttercup10454(x0) b48_buttercup10460(x0) b48_buttercup10179(x0) b48_buttercup10458(x0) k04_buttercup10004(x0) ren28(x0,x1,x2) k04_buttercup10282(x2) b48_buttercup10289(x2) ren29 ren30 k04_buttercup10286(x0) b48_buttercup10283(x0) k04_buttercup10000(x0) ren31(x0,x1,x2) b48_buttercup10102(x2) ren32 ren33 k04_buttercup10360(x0) b48_buttercup10359(x0) k04_buttercup10540(x0) b48_buttercup10541(x0) k04_buttercup10539(x0) b48_buttercup10538(x0) b48_buttercup10451(x0) k04_buttercup10044(x0) b48_buttercup10043(x0) k04_buttercup10042(x0) b48_buttercup10045(x0) b48_buttercup10261(x0) k04_buttercup10259(x0) k04_buttercup10255(x0) b48_buttercup10253(x0) b48_buttercup10260(x0) b48_buttercup10422(x0) ren34(x0,x1,x2) k04_buttercup10419(x2) b48_buttercup10421(x2) ren35 ren36 b48_buttercup10358(skc317) ren37(x0) % 31.43/6.89 % 31.43/6.89 === Starting SPASS-SCL-FOL A Little Less Naive, considering 1000 atoms initially, heuristics mode: lmodel_grow === % 31.43/6.89 % 31.43/6.89 === Backtracking. Learning clause 1328:2:5:[612.2,614.2]:TopTopTopTopTop: ren25(x0,x1,x2),ren25(x3,x4,x1) -> % 31.43/6.89 === Backtracking. Learning clause 1329:2:5:[599.2,601.2]:TopTopTopTopTop: ren22(x0,x1,x2),ren22(x3,x4,x1) -> % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1252 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1432 % 31.43/6.89 === Backtracking. Learning clause 1330:2:3:[514.2,507.2,508.2]:TopTopTop: ren15,ren13(x0,x1,x2) -> % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1613 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1724 % 31.43/6.89 === Backtracking. Learning clause 1331:2:3:[602.3,600.2,601.2]:TopTopTop: ren23,ren22(x0,x1,x2) -> % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1802 % 31.43/6.89 === Backtracking. Learning clause 1332:2:1:[488.2,40.1]:Top: b48_buttercup10107(x0) -> k04_buttercup10619(x0) % 31.43/6.89 === Backtracking. Learning clause 1333:2:5:[505.2,509.2]:TopTopTopTopTop: ren13(x0,x1,x2),ren13(x3,x4,x0) -> % 31.43/6.89 === Backtracking. Learning clause 1334:1:0:[28.2,128.1,333.2,661.1]:: b48_buttercup10640(skc87) -> % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1869 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1912 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1935 % 31.43/6.89 === Backtracking. Learning clause 1335:2:3:[936.3,934.2,935.2]:TopTopTop: ren35,ren34(x0,x1,x2) -> % 31.43/6.89 === Backtracking. Learning clause 1336:2:3:[467.2,466.2,465.2]:TopTopTop: ren5,ren4(x0,x1,x2) -> % 31.43/6.89 === Backtracking. Learning clause 1337:2:3:[671.2,664.2,665.2]:TopTopTop: ren30,ren28(x0,x1,x2) -> % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 1979 % 31.43/6.89 === Backtracking. Learning clause 1338:2:3:[498.3,496.2,497.2]:TopTopTop: ren11,ren10(x0,x1,x2) -> % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2009 % 31.43/6.89 === Backtracking. Learning clause 1339:2:3:[480.3,478.2,479.2]:TopTopTop: ren8,ren7(x0,x1,x2) -> % 31.43/6.89 === Backtracking. Learning clause 1340:4:3:[621.1,609.2,610.2]:TopTopTop: ren25(x0,x1,x2) -> ren25(skc77,skc78,skc79),ren26,ren27 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2027 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2032 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2037 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2041 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2043 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2045 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2047 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2049 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2051 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2053 % 31.43/6.89 === Clause set with instances from active satisfied. Growing active. New size: 2055 % 31.43/6.89 % 31.43/6.89 Linear Model Building succeeded. % 31.43/6.89 SZS status Satisfiable % 31.43/6.89 % 31.43/6.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.43/6.89 % 31.43/6.89 SPASS-SCL-FOL Statistics: % 31.43/6.89 Number of learned clauses: 13 % 31.43/6.89 Number of propagations: 7791 % 31.43/6.89 Number of decisions: 2655 % 31.43/6.89 Number of resolutions: 23 % 31.43/6.89 Number of condensations: 8 % 31.43/6.89 Number of sub resolutions: 2 % 31.43/6.89 Number of input literals (deduplicated): 1000 % 31.43/6.89 Number of grows: 21 % 31.43/6.89 Number of considered ground atoms: 2055 % 31.43/6.89 % 31.43/6.89 Needed: 0:00:06.24 % 31.43/6.89 %------------------------------------------------------------------------------