%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWV127+1 : TPTP v9.2.1. Bugfixed v3.3.0. % 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:36:50 PM UTC 2026 % Result : Unknown 0.70s 0.68s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV127+1 : TPTP v9.2.1. Bugfixed v3.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n022.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 13:26:52 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.70/0.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.70/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.70/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.70/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.70/0.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.70/0.66 Execution normal ended with status: gaveup % 0.70/0.66 Execution resolution_1 ended with status: gaveup % 0.70/0.66 Execution resolution_2 ended with status: gaveup % 0.70/0.66 Execution resolution_3 ended with status: gaveup % 0.70/0.66 Execution lmodel_grow ended with status: gaveup % 0.70/0.66 No successful execution. % 0.70/0.66 % 0.70/0.66 Input Clauses: % 0.70/0.68 % 0.70/0.68 Predicates: gt = leq lt geq true 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 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 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 ren200 ren201 ren202 ren203 ren204 ren205 ren206 ren207 ren208 ren209 ren210 ren211 ren212 ren213 ren214 ren215 ren216 ren217 ren218 ren219 ren220 ren221 ren222 ren223 ren224 ren225 ren226 ren227 ren228 ren229 ren230 ren231 ren232 ren233 ren234 ren235 ren236 ren237 ren238 ren239 ren240 ren241 ren242 ren243 ren244 ren245 ren246 ren247 ren248 ren249 ren250 ren251 ren252 ren253 ren254 ren255 ren256 ren257 ren258 ren259 ren260 ren261 ren262 ren263 ren264 ren265 ren266 ren267 ren268 ren269 ren270 ren271 ren272 ren273 ren274 ren275 ren276 ren277 ren278 ren279 ren280 ren281 ren282 ren283 ren284 ren285 ren286 ren287 ren288 ren289 ren290 ren291 ren292 ren293 ren294 ren295 ren296 ren297 ren298 ren299 ren300 ren301 ren302 ren303 ren304 ren305 ren306 ren307 ren308 ren309 ren310 ren311 ren312 ren313 ren314 ren315 ren316 ren317 ren318 ren319 ren320 ren321 ren322 ren323 ren324 ren325 ren326 ren327 ren328 ren329 ren330 ren331 ren332 ren333 ren334 ren335 ren336 ren337 ren338 ren339 ren340 ren341 ren342 ren343 ren344 ren345 ren346 ren347 ren348 ren349 ren350 ren351 ren352 ren353 ren354 ren355 ren356 ren357 ren358 ren359 ren360 ren361 ren362 ren363 ren364 ren365 ren366 ren367 ren368 ren369 ren370 ren371 ren372 ren373 ren374 ren375 ren376 ren377 ren378 ren379 ren380 ren381 ren382 ren383 ren384 ren385 ren386 ren387 ren388 ren389 ren390 ren391 ren392 ren393 ren394 ren395 ren396 ren397 ren398 ren399 ren400 ren401 ren402 ren403 ren404 ren405 ren406 ren407 ren408 ren409 ren410 ren411 ren412 ren413 ren414 ren415 ren416 ren417 ren418 ren419 ren420 ren421 ren422 ren423 ren424 ren425 ren426 ren427 ren428 ren429 ren430 ren431 ren432 ren433 ren434 ren435 ren436 ren437 ren438 ren439 ren440 ren441 ren442 ren443 ren444 ren445 ren446 ren447 ren448 ren449 ren450 ren451 ren452 ren453 ren454 ren455 ren456 ren457 ren458 ren459 ren460 ren461 ren462 ren463 ren464 ren465 ren466 ren467 ren468 ren469 ren470 ren471 ren472 ren473 ren474 ren475 ren476 ren477 ren478 ren479 ren480 ren481 ren482 ren483 ren484 ren485 ren486 ren487 ren488 ren489 ren490 ren491 ren492 ren493 ren494 ren495 ren496 ren497 ren498 ren499 ren500 ren501 ren502 ren503 ren504 ren505 ren506 ren507 ren508 ren509 ren510 ren511 ren512 ren513 ren514 ren515 ren516 ren517 ren518 ren519 ren520 ren521 ren522 ren523 ren524 ren525 ren526 ren527 ren528 ren529 ren530 ren531 ren532 ren533 ren534 ren535 ren536 ren537 ren538 ren539 ren540 ren541 ren542 ren543 ren544 ren545 ren546 ren547 ren548 ren549 ren550 ren551 ren552 ren553 ren554 ren555 ren556 ren557 ren558 ren559 ren560 ren561 ren562 ren563 ren564 ren565 ren566 ren567 ren568 ren569 ren570 ren571 ren572 ren573 ren574 ren575 ren576 ren577 ren578 ren579 ren580 ren581 ren582 ren583 ren584 ren585 ren586 ren587 ren588 ren589 ren590 ren591 ren592 ren593 ren594 ren595 ren596 ren597 ren598 ren599 ren600 ren601 ren602 ren603 % 0.70/0.68 Fol Constants: n0 tptp_minus_1 tptp_float_0_0 n1 n2 n3 n4 n5 def use n1000 init n7 n6 h_thruster_filter_init pv5 pv21 n588 phi_thruster_filter_init dv_thruster_filter_init q_thruster_filter_init r_thruster_filter_init xhatmin_thruster_filter_init id_thruster_filter_init pv45 pv46 pminus_thruster_filter_init zhat_thruster_filter_init zpred_thruster_filter_init pv23 sigma skc28 skc29 skc31 skc32 skc33 skc34 skc35 skc36 skc37 skc38 skc39 skc40 skc41 skc42 skc43 skc44 skc45 skc47 skc48 skc49 skc50 skc51 skc52 skc53 skc54 skc55 skc56 skc57 skc58 skc59 skc60 skc61 skc62 skc63 skc65 skc66 skc67 skc68 skc69 skc70 skc71 skc72 skc73 skc74 skc75 skc76 skc77 skc78 skc79 skc80 skc81 skc83 skc84 skc85 skc86 skc87 skc88 skc89 skc90 skc91 skc92 skc93 skc94 skc95 skc96 skc97 skc98 skc99 skc101 skc102 skc103 skc104 skc105 skc106 skc107 skc108 skc109 skc110 skc111 skc112 skc113 skc114 skc115 skc117 skc118 skc119 skc120 skc121 skc122 skc123 skc124 skc125 skc126 skc127 skc128 skc129 skc130 skc131 skc132 skc133 skc135 skc136 skc137 skc138 skc139 skc140 skc141 skc142 skc143 skc144 skc145 skc146 skc147 skc148 skc149 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 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 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 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 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 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 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 skc515 skc516 skc517 skc518 skc519 skc520 skc521 skc522 skc523 skc524 skc525 skc526 skc527 skc528 skc529 skc530 skc531 skc532 skc533 skc534 skc535 skc536 skc537 skc538 skc539 skc540 skc541 skc542 skc543 skc544 skc545 skc546 skc547 skc548 skc549 skc550 skc551 skc552 skc553 skc554 skc555 skc556 skc557 skc558 skc559 skc560 skc561 skc562 skc563 skc564 skc565 skc567 skc568 skc569 skc570 skc571 skc572 skc573 skc574 skc575 skc576 skc577 skc578 skc579 skc580 skc581 skc582 skc583 skc584 skc585 skc586 skc587 skc588 skc589 skc590 skc591 skc592 skc593 skc594 skc595 skc596 skc597 skc598 skc599 skc600 skc601 skc602 skc603 skc604 skc605 skc606 skc607 skc608 skc609 skc610 skc611 skc612 skc613 skc614 skc615 skc616 skc617 skc619 skc620 skc621 skc622 skc623 skc624 skc625 skc626 skc627 skc628 skc629 skc630 skc631 skc632 skc633 skc634 skc635 skc636 skc637 skc638 skc639 skc640 skc641 skc642 skc643 skc644 skc645 skc646 skc647 skc648 skc649 skc650 skc651 skc652 skc653 skc654 skc655 skc656 skc657 skc658 skc659 skc660 skc661 skc662 skc663 skc664 skc665 skc666 skc667 skc668 skc669 skc671 skc672 skc673 skc674 skc675 skc676 skc677 skc678 skc679 skc680 skc681 skc682 skc683 skc684 skc685 skc686 skc687 skc688 skc689 skc690 skc691 skc692 skc693 skc694 skc695 skc696 skc697 skc698 skc699 skc700 skc701 skc702 skc703 skc704 skc705 skc706 skc707 skc708 skc709 skc710 skc711 skc712 skc713 skc714 skc715 skc716 skc717 skc718 skc719 skc720 skc721 skc723 skc724 skc725 skc726 skc727 skc728 skc729 skc730 skc731 skc732 skc733 skc734 skc735 skc736 skc737 skc738 skc739 skc740 skc741 skc742 skc743 skc744 skc745 skc746 skc747 skc748 skc749 skc750 skc751 skc752 skc753 skc754 skc755 skc756 skc757 skc758 skc759 skc760 skc761 skc762 skc763 skc764 skc765 skc766 skc767 skc768 skc769 skc770 skc771 skc772 skc773 skc775 skc776 skc777 skc778 skc779 skc780 skc781 skc782 skc783 skc784 skc785 skc786 skc787 skc788 skc789 skc790 skc791 skc792 skc793 skc794 skc795 skc796 skc797 skc798 skc799 skc800 skc801 skc802 skc803 skc804 skc805 skc806 skc807 skc808 skc809 skc810 skc811 skc812 skc813 skc814 skc815 skc816 skc817 skc818 skc819 skc820 skc821 skc822 skc823 skc824 skc825 skc827 skc828 skc829 skc830 skc831 skc832 skc833 skc834 skc835 skc836 skc837 skc838 skc839 skc840 skc841 skc842 skc843 skc844 skc845 skc846 skc847 skc848 skc849 skc850 skc851 skc852 skc853 skc854 skc855 skc856 skc857 skc858 skc859 skc860 skc861 skc862 skc863 skc864 skc865 skc866 skc867 skc868 skc869 skc870 skc871 skc872 skc873 skc874 skc875 skc876 skc877 skc879 skc880 skc881 skc882 skc883 skc884 skc885 skc886 skc887 skc888 skc889 skc890 skc891 skc892 skc893 skc894 skc895 skc896 skc897 skc898 skc899 skc900 skc901 skc902 skc903 skc904 skc905 skc906 skc907 skc908 skc909 skc910 skc911 skc912 skc913 skc914 skc915 skc916 skc917 skc918 skc919 skc920 skc921 skc922 skc923 skc924 skc925 skc926 skc927 skc928 skc929 skc931 skc932 skc933 skc934 skc935 skc936 skc937 skc938 skc939 skc940 skc941 skc942 skc943 skc944 skc945 skc946 skc947 skc948 skc949 skc950 skc951 skc952 skc953 skc954 skc955 skc956 skc957 skc958 skc959 skc960 skc961 skc962 skc963 skc964 skc965 skc966 skc967 skc968 skc969 skc970 skc971 skc972 skc973 skc974 skc975 skc976 skc977 skc978 skc979 skc980 skc981 skc982 skc983 skc984 skc985 skc986 skc987 skc988 skc989 skc990 skc991 skc992 skc993 skc994 skc995 skc997 skc998 skc999 skc1000 skc1001 skc1002 skc1003 skc1004 skc1005 skc1006 skc1007 skc1008 skc1009 skc1010 skc1011 skc1012 skc1013 skc1014 skc1015 skc1016 skc1017 skc1018 skc1019 skc1020 skc1021 skc1022 skc1023 skc1024 skc1025 skc1026 skc1027 skc1028 skc1029 skc1030 skc1031 skc1032 skc1033 skc1034 skc1035 skc1036 skc1037 skc1038 skc1039 skc1040 skc1041 skc1042 skc1043 skc1044 skc1045 skc1046 skc1047 skc1048 skc1049 skc1050 skc1051 skc1052 skc1053 skc1054 skc1055 skc1056 skc1057 skc1058 skc1059 skc1060 skc1061 skc1062 skc1063 skc1064 skc1065 skc1066 skc1067 skc1068 skc1069 skc1070 skc1071 skc1072 skc1073 skc1074 skc1075 skc1076 skc1077 skc1078 skc1079 % 0.70/0.68 Fol Functions: pred succ uniform_int_rnd dim tptp_const_array1 a_select2 tptp_const_array2 a_select3 trans inv tptp_update3 tptp_madd tptp_msub tptp_mmul sum plus minus tptp_update2 skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 skf25 skf26 skf27 skf30 skf46 skf64 skf82 skf100 skf116 skf134 skf150 skf202 skf254 skf306 skf358 skf410 skf462 skf514 skf566 skf618 skf670 skf722 skf774 skf826 skf878 skf930 skf996 % 0.70/0.68 Problem Properties: % 0.70/0.68 This is a full first-order problem with equality. % 0.70/0.68 SZS status GaveUp % 0.70/0.68 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.70/0.68 %------------------------------------------------------------------------------