%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : HWV095-1 : TPTP v9.2.1. Released v6.1.0. % 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:24:25 PM UTC 2026 % Result : Unsatisfiable 0.29s 0.78s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.25 % Problem : HWV095-1 : TPTP v9.2.1. Released v6.1.0. % 0.07/0.25 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.15/0.52 % Computer : n027.cluster.edu % 0.15/0.52 % Model : x86_64 x86_64 % 0.15/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.52 % Memory : 8042.1875MB % 0.15/0.52 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.52 % CPULimit : 300 % 0.15/0.52 % WCLimit : 300 % 0.15/0.52 % DateTime : Thu May 7 12:09:23 EDT 2026 % 0.15/0.52 % CPUTime : % 0.15/0.52 SPASS-SCL-FOL version: % 0.23/0.61 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.29/0.76 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.29/0.76 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.29/0.76 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.29/0.76 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.29/0.76 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.29/0.76 Execution resolution_1 ended with status: unsatisfiable % 0.29/0.76 Used heuristic: resolution_1 % 0.29/0.76 % 0.29/0.76 Input Clauses: % 0.29/0.77 % 0.29/0.77 Predicates: v97 sP292_aig_name = sP293_aig_name v495 sP294_aig_name nextState reachableState v1 v1000 v1007 v8 range_3_0 v981 v989 v987 v23 v20 v982 v983 v788 v746 v958 v959 v960 v966 v965 b1110 v950 v951 v954 v29 v952 v955 v706 v841 v953 v938 v946 v944 v31 v939 v941 v817 v931 v934 v930 v935 v75 v37 v914 v924 v922 v42 v915 v916 v918 v836 v838 v879 v881 v880 v840 v839 v882 v883 b01111 v890 v889 v888 v909 v842 v848 v843 range_5_0 v849 v855 v853 v851 range_4_0 v837 v829 v833 v830 v834 v831 v813 v823 v821 v814 v815 v801 v808 v800 v809 v784 v794 v792 v77 v785 v786 v701 v703 v745 v747 v705 v704 v748 v749 v756 v755 v754 v775 v707 v713 v708 v714 v721 v719 v717 v702 v685 v693 v691 v95 v686 v687 v347 v677 v101 v682 v283 v452 v679 v169 sP572 v134 v607 sP568 sP569 sP570 sP571 v661 b01 v652 v501 b10 range_1_0 v497 v499 v594 sP567 v596 v581 v597 v562 v599 v474 v551 v546 v550 v544 v504 v543 v541 v527 v529 v531 v533 v535 v537 v539 range_122_116 v553 sP443 sP444 sP445 sP446 sP447 sP448 sP449 sP450 sP451 sP452 sP453 sP454 sP455 sP456 sP457 sP458 sP459 sP460 sP461 sP462 sP463 sP464 sP465 sP466 sP467 sP468 sP469 sP470 sP471 sP472 sP473 sP474 sP475 sP476 sP477 sP478 sP479 sP480 sP481 sP482 sP483 sP484 sP485 sP486 sP487 sP488 sP489 sP490 sP491 sP492 sP493 sP494 sP495 sP496 sP497 sP498 sP499 sP500 sP501 sP502 sP503 sP504 sP505 sP506 sP507 sP508 sP509 sP510 sP511 sP512 sP513 sP514 sP515 sP516 sP517 sP518 sP519 sP520 sP521 sP522 sP523 sP524 sP525 sP526 sP527 sP528 sP529 sP530 sP531 sP532 sP533 sP534 sP535 sP536 sP537 sP538 sP539 sP540 sP541 sP542 sP543 sP544 sP545 sP546 sP547 sP548 sP549 sP550 sP551 sP552 sP553 sP554 sP555 sP556 sP557 sP558 sP559 sP560 sP561 sP562 sP563 sP564 sP565 sP566 v554 v579 v582 v568 v570 v571 sP319 sP320 sP321 sP322 sP323 sP324 sP325 sP326 sP327 sP328 sP329 sP330 sP331 sP332 sP333 sP334 sP335 sP336 sP337 sP338 sP339 sP340 sP341 sP342 sP343 sP344 sP345 sP346 sP347 sP348 sP349 sP350 sP351 sP352 sP353 sP354 sP355 sP356 sP357 sP358 sP359 sP360 sP361 sP362 sP363 sP364 sP365 sP366 sP367 sP368 sP369 sP370 sP371 sP372 sP373 sP374 sP375 sP376 sP377 sP378 sP379 sP380 sP381 sP382 sP383 sP384 sP385 sP386 sP387 sP388 sP389 sP390 sP391 sP392 sP393 sP394 sP395 sP396 sP397 sP398 sP399 sP400 sP401 sP402 sP403 sP404 sP405 sP406 sP407 sP408 sP409 sP410 sP411 sP412 sP413 sP414 sP415 sP416 sP417 sP418 sP419 sP420 sP421 sP422 sP423 sP424 sP425 sP426 sP427 sP428 sP429 sP430 sP431 sP432 sP433 sP434 sP435 sP436 sP437 sP438 sP439 sP440 sP441 sP442 v555 v573 sP318 v578 v569 v556 v510 sP317 range_122_0 v513 v512 v514 v516 v520 v464 v522 v521 v518 v517 range_8_0 sP13_aig_name v525 v515 v462 range_8_1 v463 v470 v490 v488 v491 v471 v480 sP11_v460_bitIndex1 v472 v446 v455 v448 v456 v458 v457 v167 v439 sP316 v441 v423 v433 v431 v139 v424 v425 v427 v369 v371 v400 v402 v401 v373 v372 v403 v404 b100 sP14_aig_name v409 v418 v374 v375 sP315 range_31_0 v381 v376 v382 v385 range_2_0 v370 v365 v361 sP314 v343 v353 v351 v172 b1000 v344 v345 v290 v313 v315 v314 v292 v291 v334 v332 v329 v320 v321 v297 v274 v276 v279 v285 v278 v286 sP313 v263 v270 v264 v265 b001 b010 v269 sP304 sP312 sP305 sP306 sP307 sP308 sP309 sP310 sP311 v256 v248 v221 v250 range_7_0 v252 v225 sP295 sP296 sP297 sP298 sP299 sP300 sP301 sP302 v238 sP303 v227 v232 sP9_v216_bitIndex6 sP6_v208_bitIndex2 v157 v64 v62 sP1_v54_bitIndex8 % 0.29/0.77 Fol Constants: bitIndex1 bitIndex0 bitIndex116 bitIndex117 bitIndex118 bitIndex119 bitIndex120 bitIndex121 bitIndex122 bitIndex3 bitIndex5 bitIndex6 constB19 constB20 constB18 constB17 constB16 constB15 constB14 constB13 constB12 constB11 constB10 constB9 constB8 constB7 constB6 constB5 constB4 constB3 constB2 constB1 constB0 bitIndex4 bitIndex2 bitIndex7 bitIndex8 bitIndex9 bitIndex10 bitIndex11 bitIndex12 bitIndex13 bitIndex14 bitIndex15 bitIndex16 bitIndex17 bitIndex18 bitIndex19 bitIndex20 bitIndex21 bitIndex22 bitIndex23 bitIndex24 bitIndex25 bitIndex26 bitIndex27 bitIndex28 bitIndex29 bitIndex30 bitIndex31 bitIndex696 bitIndex81 bitIndex737 bitIndex736 bitIndex735 bitIndex734 bitIndex733 bitIndex732 bitIndex731 bitIndex730 bitIndex115 bitIndex729 bitIndex114 bitIndex728 bitIndex113 bitIndex727 bitIndex112 bitIndex726 bitIndex111 bitIndex725 bitIndex110 bitIndex724 bitIndex109 bitIndex723 bitIndex108 bitIndex722 bitIndex107 bitIndex721 bitIndex106 bitIndex720 bitIndex105 bitIndex719 bitIndex104 bitIndex718 bitIndex103 bitIndex717 bitIndex102 bitIndex716 bitIndex101 bitIndex715 bitIndex100 bitIndex714 bitIndex99 bitIndex713 bitIndex98 bitIndex712 bitIndex97 bitIndex711 bitIndex96 bitIndex710 bitIndex95 bitIndex709 bitIndex94 bitIndex708 bitIndex93 bitIndex707 bitIndex92 bitIndex706 bitIndex91 bitIndex705 bitIndex90 bitIndex704 bitIndex89 bitIndex703 bitIndex88 bitIndex702 bitIndex87 bitIndex701 bitIndex86 bitIndex700 bitIndex85 bitIndex699 bitIndex84 bitIndex698 bitIndex83 bitIndex697 bitIndex82 bitIndex695 bitIndex80 bitIndex694 bitIndex79 bitIndex693 bitIndex78 bitIndex692 bitIndex77 bitIndex691 bitIndex76 bitIndex690 bitIndex75 bitIndex689 bitIndex74 bitIndex688 bitIndex73 bitIndex687 bitIndex72 bitIndex686 bitIndex71 bitIndex685 bitIndex70 bitIndex684 bitIndex69 bitIndex683 bitIndex68 bitIndex682 bitIndex67 bitIndex681 bitIndex66 bitIndex680 bitIndex65 bitIndex679 bitIndex64 bitIndex678 bitIndex63 bitIndex677 bitIndex62 bitIndex676 bitIndex61 bitIndex675 bitIndex60 bitIndex674 bitIndex59 bitIndex673 bitIndex58 bitIndex672 bitIndex57 bitIndex671 bitIndex56 bitIndex670 bitIndex55 bitIndex669 bitIndex54 bitIndex668 bitIndex53 bitIndex667 bitIndex52 bitIndex666 bitIndex51 bitIndex665 bitIndex50 bitIndex664 bitIndex49 bitIndex663 bitIndex48 bitIndex662 bitIndex47 bitIndex661 bitIndex46 bitIndex660 bitIndex45 bitIndex659 bitIndex44 bitIndex658 bitIndex43 bitIndex657 bitIndex42 bitIndex656 bitIndex41 bitIndex655 bitIndex40 bitIndex654 bitIndex39 bitIndex653 bitIndex38 bitIndex652 bitIndex37 bitIndex651 bitIndex36 bitIndex650 bitIndex35 bitIndex649 bitIndex34 bitIndex648 bitIndex33 bitIndex647 bitIndex32 bitIndex646 bitIndex645 bitIndex644 bitIndex643 bitIndex642 bitIndex641 bitIndex640 bitIndex639 bitIndex638 bitIndex637 bitIndex636 bitIndex635 bitIndex634 bitIndex633 bitIndex632 bitIndex631 bitIndex630 bitIndex629 bitIndex628 bitIndex627 bitIndex626 bitIndex625 bitIndex624 bitIndex623 bitIndex622 bitIndex621 bitIndex620 bitIndex619 bitIndex618 bitIndex617 bitIndex616 bitIndex615 bitIndex573 bitIndex614 bitIndex613 bitIndex612 bitIndex611 bitIndex610 bitIndex609 bitIndex608 bitIndex607 bitIndex606 bitIndex605 bitIndex604 bitIndex603 bitIndex602 bitIndex601 bitIndex600 bitIndex599 bitIndex598 bitIndex597 bitIndex596 bitIndex595 bitIndex594 bitIndex593 bitIndex592 bitIndex591 bitIndex590 bitIndex589 bitIndex588 bitIndex587 bitIndex586 bitIndex585 bitIndex584 bitIndex583 bitIndex582 bitIndex581 bitIndex580 bitIndex579 bitIndex578 bitIndex577 bitIndex576 bitIndex575 bitIndex574 bitIndex572 bitIndex571 bitIndex570 bitIndex569 bitIndex568 bitIndex567 bitIndex566 bitIndex565 bitIndex564 bitIndex563 bitIndex562 bitIndex561 bitIndex560 bitIndex559 bitIndex558 bitIndex557 bitIndex556 bitIndex555 bitIndex554 bitIndex553 bitIndex552 bitIndex551 bitIndex550 bitIndex549 bitIndex548 bitIndex547 bitIndex546 bitIndex545 bitIndex544 bitIndex543 bitIndex542 bitIndex541 bitIndex540 bitIndex539 bitIndex538 bitIndex537 bitIndex536 bitIndex535 bitIndex534 bitIndex533 bitIndex532 bitIndex531 bitIndex530 bitIndex529 bitIndex528 bitIndex527 bitIndex526 bitIndex525 bitIndex524 bitIndex523 bitIndex522 bitIndex521 bitIndex520 bitIndex519 bitIndex518 bitIndex517 bitIndex516 bitIndex515 bitIndex514 bitIndex513 bitIndex512 bitIndex511 bitIndex510 bitIndex509 bitIndex508 bitIndex507 bitIndex506 bitIndex505 bitIndex504 bitIndex503 bitIndex502 bitIndex501 bitIndex500 bitIndex499 bitIndex498 bitIndex497 bitIndex496 bitIndex495 bitIndex494 bitIndex493 bitIndex492 bitIndex400 bitIndex399 bitIndex398 bitIndex397 bitIndex396 bitIndex395 bitIndex394 bitIndex393 % 0.29/0.77 Fol Functions: % 0.29/0.77 Problem Properties: % 0.29/0.77 This is a Bernays Schoenfinkel Ramsey problem. % 0.29/0.77 % 0.29/0.77 % 0.29/0.77 Reduced Input Clauses: % 0.29/0.77 2653:2:2:[76.1,74.1]:TopTop: v987(x0,x1) -> v23(x0,x1) % 0.29/0.77 2654:2:1:[120.1,122.0]:Top: v746(x0,bitIndex0) -> v951(x0) % 0.29/0.77 2655:2:1:[129.1,128.1]:Top: v955(x0) -> v954(x0) % 0.29/0.77 2656:1:1:[131.1,130.1]:Top: v955(x0) -> % 0.29/0.77 2657:2:1:[134.1,132.1]:Top: v952(x0) -> v953(x0) % 0.29/0.77 2658:2:1:[145.1,144.1]:Top: v31(x0,bitIndex0) -> v944(x0) % 0.29/0.77 2659:1:1:[161.1,160.0]:Top: -> v935(x0) % 0.29/0.77 2660:2:2:[182.1,180.1]:TopTop: v922(x0,x1) -> v42(x0,x1) % 0.29/0.77 2661:4:2:[198.0,192.1]:TopTop: v42(x0,x1) -> v838(x0),v879(x0),v37(x0,x1) % 0.29/0.77 2662:4:2:[199.0,193.1]:TopTop: v37(x0,x1) -> v838(x0),v879(x0),v42(x0,x1) % 0.29/0.77 2663:2:1:[339.0,340.2]:Top: v849(x0,bitIndex0) -> v855(x0) % 0.29/0.77 2664:2:1:[373.1,371.1]:Top: v833(x0) -> v834(x0) % 0.29/0.77 2665:2:1:[378.0,377.0]:Top: v831(x0) -> v830(x0) % 0.29/0.77 2666:1:1:[380.1,379.1]:Top: v831(x0) -> % 0.29/0.77 2667:2:1:[392.1,390.1]:Top: v821(x0) -> v31(x0,bitIndex1) % 0.29/0.77 2668:1:1:[410.0,409.0]:Top: -> v809(x0) % 0.29/0.77 2669:2:2:[429.1,427.1]:TopTop: v792(x0,x1) -> v77(x0,x1) % 0.29/0.77 2670:4:2:[445.0,439.1]:TopTop: v77(x0,x1) -> v703(x0),v745(x0),v75(x0,x1) % 0.29/0.77 2671:4:2:[446.0,440.1]:TopTop: v75(x0,x1) -> v703(x0),v745(x0),v77(x0,x1) % 0.29/0.77 2672:2:1:[598.0,599.2]:Top: v714(x0,bitIndex0) -> v721(x0) % 0.29/0.77 2673:2:1:[637.1,635.1]:Top: v691(x0) -> v95(x0) % 0.29/0.77 2674:2:1:[667.1,656.2]:Top: v97(x0,bitIndex0),v677(x0) -> % 0.29/0.77 2675:3:1:[667.1,664.3]:Top: v97(x0,bitIndex1) -> v679(x0),v97(x0,bitIndex0) % 0.29/0.77 2676:2:2:[667.1,665.2]:TopTop: v97(x0,x1) -> v607(x0,x1) % 0.29/0.77 2677:4:1:[679.1,686.4]:Top: v495(x0,bitIndex4),sP570(x0) -> sP294_aig_name(x0),v495(x0,bitIndex3) % 0.29/0.77 2678:4:1:[679.1,688.4]:Top: v495(x0,bitIndex4),sP570(x0) -> sP294_aig_name(x0),v495(x0,bitIndex6) % 0.29/0.77 2679:4:1:[11.1,689.2]:Top: v495(x0,bitIndex3),sP570(x0) -> v495(x0,bitIndex6),sP569(x0) % 0.29/0.77 2680:7:2:[706.1,702.1]:TopTop: v607(x0,x1),v495(x0,bitIndex0) -> v495(x0,bitIndex5),v495(x0,bitIndex4),v495(x0,bitIndex2),v495(x0,bitIndex1),v495(x0,bitIndex6) % 0.29/0.77 2681:8:2:[703.3,704.4]:TopTop: v607(x0,x1),v495(x0,bitIndex3),v495(x0,bitIndex1) -> v652(x0,x1),v495(x0,bitIndex4),v495(x0,bitIndex5),v495(x0,bitIndex0),v495(x0,bitIndex2) % 0.29/0.77 2682:2:2:[710.1,711.1]:TopTop: v652(x0,x1) -> b10(x1) % 0.29/0.77 2683:2:2:[1421.1,1419.1]:TopTop: v579(x0,x1) -> v582(x0,x1) % 0.29/0.77 2684:3:2:[1801.0,1807.0]:TopTop: nextState(x0,x1) -> v562(x1),v20(x0) % 0.29/0.77 2685:4:2:[2018.0,2012.1]:TopTop: v513(x0,x1) -> v516(x0),v520(x0),v464(x0,x1) % 0.29/0.77 2686:4:2:[2019.0,2013.1]:TopTop: v464(x0,x1) -> v516(x0),v520(x0),v513(x0,x1) % 0.29/0.77 2687:2:1:[2093.1,2092.1]:Top: v491(x0) -> v488(x0) % 0.29/0.77 2688:3:1:[2125.0,2127.2]:Top: v97(x0,bitIndex0),v458(x0) -> v456(x0) % 0.29/0.77 2689:3:1:[2125.0,2129.2]:Top: v457(x0) -> v97(x0,bitIndex0),v456(x0) % 0.29/0.77 2690:3:1:[667.1,2138.3]:Top: v97(x0,bitIndex0),v97(x0,bitIndex1),v446(x0) -> % 0.29/0.77 2691:2:2:[2157.1,2155.1]:TopTop: v431(x0,x1) -> v139(x0,x1) % 0.29/0.77 2692:4:2:[2173.0,2167.1]:TopTop: v139(x0,x1) -> v371(x0),v400(x0),v134(x0,x1) % 0.29/0.77 2693:4:2:[2174.0,2168.1]:TopTop: v134(x0,x1) -> v371(x0),v400(x0),v139(x0,x1) % 0.29/0.77 2694:2:1:[2316.0,2317.2]:Top: v382(x0,bitIndex0) -> v385(x0) % 0.29/0.78 2695:2:1:[2447.0,2448.2]:Top: v169(x0,bitIndex0) -> v329(x0) % 0.29/0.78 2696:4:1:[667.1,2464.3]:Top: v97(x0,bitIndex0),v285(x0) -> v97(x0,bitIndex1),v286(x0) % 0.29/0.78 2697:4:1:[667.1,2465.3]:Top: v97(x0,bitIndex0),v286(x0) -> v97(x0,bitIndex1),v285(x0) % 0.29/0.78 2698:2:1:[667.1,2472.2]:Top: v97(x0,bitIndex1),v276(x0) -> % 0.29/0.78 2699:2:1:[2485.1,2487.1]:Top: v332(x0,bitIndex1) -> v270(x0) % 0.29/0.78 % 0.29/0.78 SZS status Unsatisfiable % 0.29/0.78 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.29/0.78 % 0.29/0.78 SPASS-SCL-FOL Statistics: % 0.29/0.78 Number of learned clauses: 0 % 0.29/0.78 Number of propagations: 0 % 0.29/0.78 Number of decisions: 0 % 0.29/0.78 Number of resolutions: 0 % 0.29/0.78 Number of condensations: 0 % 0.29/0.78 Number of sub resolutions: 47 % 0.29/0.78 % 0.29/0.78 Needed: 0:00:00.04 % 0.29/0.78 %------------------------------------------------------------------------------