%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PLA034+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 : n024.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:15 PM UTC 2026 % Result : Unknown 0.97s 0.68s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : PLA034+1 : TPTP v9.2.1. Bugfixed v5.5.1. % 0.00/0.08 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.28 % Computer : n024.cluster.edu % 0.11/0.28 % Model : x86_64 x86_64 % 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.28 % Memory : 8042.1875MB % 0.11/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.28 % CPULimit : 300 % 0.11/0.28 % WCLimit : 300 % 0.11/0.28 % DateTime : Thu May 7 07:56:57 EDT 2026 % 0.11/0.28 % CPUTime : % 0.11/0.28 SPASS-SCL-FOL version: % 0.17/0.34 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.97/0.65 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.97/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.97/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.97/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.97/0.65 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.97/0.65 Execution resolution_1 ended with status: gaveup % 0.97/0.65 Execution resolution_2 ended with status: gaveup % 0.97/0.65 Execution resolution_3 ended with status: gaveup % 0.97/0.65 Execution lmodel_grow ended with status: gaveup % 0.97/0.65 Execution normal ended with status: gaveup % 0.97/0.65 No successful execution. % 0.97/0.65 % 0.97/0.65 Input Clauses: % 0.97/0.67 % 0.97/0.67 Predicates: p = % 0.97/0.67 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 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 % 0.97/0.67 Fol Functions: 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 skf353 skf354 skf355 skf356 skf357 skf358 skf359 skf360 skf361 skf362 skf363 skf364 skf365 skf366 skf367 skf368 skf369 skf370 skf371 skf372 skf373 skf374 skf375 skf376 skf377 skf378 skf379 skf380 skf381 skf382 skf383 skf384 skf385 skf386 skf387 skf388 skf389 skf390 skf391 skf392 skf393 skf394 skf395 skf396 skf397 skf398 skf399 skf400 skf401 skf402 skf403 skf404 skf405 skf406 skf407 skf408 skf409 skf410 skf411 skf412 skf413 skf414 skf415 skf416 skf417 skf418 skf419 skf420 skf421 skf422 skf423 skf424 skf425 skf426 skf427 skf428 skf429 skf430 skf431 skf432 skf433 skf434 skf435 skf436 skf437 skf438 skf439 skf440 skf441 skf442 skf443 skf444 skf445 skf446 skf447 skf448 skf449 skf450 skf451 skf452 skf453 skf454 skf455 skf456 skf457 skf458 skf459 skf460 skf461 skf462 skf463 skf464 skf465 skf466 skf467 skf468 skf469 skf470 skf471 skf472 skf473 skf474 skf475 skf476 skf477 skf478 skf479 skf480 skf481 skf482 skf483 skf484 skf485 skf486 skf487 skf488 skf489 skf490 skf491 skf492 skf493 skf494 skf495 skf496 skf497 skf498 skf499 skf500 skf501 skf502 skf503 skf504 skf505 skf506 skf507 skf508 skf509 skf510 skf511 skf512 skf513 skf514 skf515 skf516 skf517 skf518 skf519 skf520 skf521 skf522 skf523 skf524 skf525 skf526 skf527 skf528 skf529 skf530 skf531 skf532 skf533 skf534 skf535 skf536 skf537 skf538 skf539 skf540 skf541 skf542 skf543 skf544 skf545 skf546 skf547 skf548 skf549 skf550 skf551 skf552 skf553 skf554 skf555 skf556 skf557 skf558 skf559 skf560 skf561 skf562 skf563 skf564 skf565 skf566 skf567 skf568 skf569 skf570 skf571 skf572 skf573 skf574 skf575 skf576 skf577 skf578 skf579 skf580 skf581 skf582 skf583 skf584 skf585 skf586 skf587 skf588 skf589 skf590 skf591 skf592 skf593 skf594 skf595 skf596 skf597 skf598 skf599 skf600 skf601 skf602 skf603 skf604 skf605 skf606 skf607 skf608 skf609 skf610 skf611 skf612 skf613 skf614 skf615 skf616 skf617 skf618 skf619 skf620 skf621 skf622 skf623 skf624 skf625 skf626 skf627 skf628 skf629 skf630 skf631 skf632 skf633 skf634 skf635 skf636 skf637 skf638 skf639 skf640 skf641 skf642 skf643 skf644 skf645 skf646 skf647 skf648 skf649 skf650 skf651 skf652 skf653 skf654 skf655 skf656 skf657 skf658 skf659 skf660 skf661 skf662 skf663 skf664 skf665 skf666 skf667 skf668 skf669 skf670 skf671 skf672 skf673 skf674 skf675 skf676 skf677 skf678 skf679 skf680 skf681 skf682 skf683 skf684 skf685 skf686 skf687 skf688 skf689 skf690 skf691 skf692 skf693 skf694 skf695 skf696 skf697 skf698 skf699 skf700 skf701 skf702 skf703 skf704 skf705 skf706 skf707 skf708 skf709 skf710 skf711 skf712 skf713 skf714 skf715 skf716 skf717 skf718 skf719 skf720 skf721 skf722 skf723 skf724 skf725 skf726 skf727 skf728 skf729 skf730 skf731 skf732 skf733 skf734 skf735 skf736 skf737 skf738 skf739 skf740 skf741 skf742 skf743 skf744 skf745 skf746 skf747 skf748 skf749 skf750 skf751 skf752 skf753 skf754 skf755 skf756 skf757 skf758 skf759 skf760 skf761 skf762 skf763 skf764 skf765 skf766 skf767 skf768 skf769 skf770 skf771 skf772 skf773 skf774 skf775 skf776 skf777 skf778 skf779 skf780 skf781 skf782 skf783 skf784 skf785 skf786 skf787 skf788 skf789 skf790 skf791 skf792 skf793 skf794 skf795 skf796 skf797 skf798 skf799 skf800 skf801 skf802 skf803 skf804 skf805 skf806 skf807 skf808 skf809 skf810 skf811 skf812 skf813 skf814 skf815 skf816 skf817 skf818 skf819 skf820 skf821 skf822 skf823 skf824 skf825 skf826 skf827 skf828 skf829 skf830 skf831 skf832 skf833 skf834 skf835 skf836 skf837 skf838 skf839 skf840 skf841 skf842 skf843 skf844 skf845 skf846 skf847 skf848 % 0.97/0.67 Problem Properties: % 0.97/0.67 This is a full first-order problem with equality. % 0.97/0.67 SZS status GaveUp % 0.97/0.67 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.97/0.67 %------------------------------------------------------------------------------