%------------------------------------------------------------------------------
% 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 : n021.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 : Theorem 22.25s 5.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : HWV095+1 : TPTP v9.2.1. Released v6.1.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.32 % Computer : n021.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu May 7 12:10:01 EDT 2026
% 0.11/0.32 % CPUTime :
% 0.11/0.32 SPASS-SCL-FOL version:
% 0.15/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 22.25/4.97 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.25/4.97 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.25/4.97 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.25/4.97 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.25/4.97 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.25/4.97 Execution normal ended with status: unsatisfiable
% 22.25/4.97 Used heuristic: normal
% 22.25/4.97
% 22.25/4.97 Input Clauses:
% 22.25/4.99
% 22.25/4.99 Predicates: nextState reachableState = v1 v4 v995 v996 v998 v1010 v1000 v999 v1001 v1003 v1007 v1004 v1005 v1006 v1008 v1009 range_3_0 v8 v981 v989 v987 v990 v23 v10 v982 v983 v777 v788 v25 v958 v959 v960 v976 v974 v969 v962 v975 v978 v977 v970 v973 v966 v971 v972 v963 v968 v965 v964 v967 b1110 v27 v950 v951 v803 v954 v952 v806 v955 v810 v802 v953 v832 v807 v938 v29 v946 v944 v824 v31 v939 v941 v779 v817 v930 v934 v931 v935 v933 v932 v33 v35 v37 v914 range_4_0 v924 v922 v925 v42 v39 v915 v916 v911 v918 v836 v838 v879 v881 v840 v908 v909 v67 v44 v882 v883 b01111 v905 v903 v898 v893 v885 v904 v907 v906 v899 v902 v890 v900 v901 v894 v897 v889 v895 v896 v886 v892 v888 v887 v891 v880 v841 range_31_0 v842 v843 range_5_0 v877 v875 v871 v867 v863 v845 v876 v878 v849 v857 v872 v874 v855 v858 v873 v868 v870 v853 v859 v869 v864 v866 v851 v860 v865 v846 v861 v848 v862 v847 v850 v852 v854 v856 v839 v837 v69 v828 v829 v833 v830 v834 v831 v71 v813 v823 v821 v12 v814 v815 v800 v808 v801 v809 v804 v805 v73 v75 v784 v794 v792 v795 v77 v785 v786 v781 v340 v701 v703 v745 v747 v705 v774 v775 v79 v748 v749 v771 v769 v764 v759 v751 v770 v773 v772 v765 v768 v756 v766 v767 v760 v763 v755 v761 v762 v752 v758 v754 v753 v757 v746 v706 v707 v708 v743 v741 v737 v733 v729 v710 v742 v744 v714 v723 v738 v740 v721 v724 v739 v734 v736 v719 v725 v735 v730 v732 v717 v726 v731 v711 v727 v713 v728 v712 v716 v718 v720 v722 v704 b00000 v702 v81 v83 v85 v87 v89 v685 v693 v691 v694 v95 v91 v686 v687 v336 v347 v677 v682 v679 v678 v681 v283 v680 v280 v452 v99 range_1_0 v97 v607 v608 v645 v653 v661 b01 v652 v663 v672 v674 v627 v675 v495 v624 v664 v669 v671 v667 v666 v626 v668 v619 v654 v656 v658 v659 v660 v625 v636 v647 v592 b10 v648 v649 v650 v651 v623 v621 v610 v643 v630 v611 v641 v616 v612 v638 v640 v634 v613 v631 v633 v635 v637 v622 v614 v628 v617 v618 v620 v497 v499 v501 v594 v596 range_122_0 v581 v597 v562 v599 v467 v474 v546 v551 v550 v504 v544 v543 v527 v529 v531 v533 v535 v537 v539 v541 range_122_116 v553 v554 v579 v564 v582 b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 v568 v570 v555 v560 v563 v575 v576 v577 v578 v123 v105 v565 v566 v574 v567 v572 v573 v571 v569 v103 v556 v548 v508 v506 v510 v511 range_8_0 v513 v512 v514 v516 v520 v464 v522 v518 v524 v525 v521 v517 v515 range_8_1 v462 v463 v101 v470 v490 v488 v487 v491 v471 v480 v478 v481 v482 v483 v486 v484 v485 v460 v472 v125 v446 v455 v448 v456 v451 v279 v458 v457 v167 v439 v447 v454 v453 v449 v450 v444 v441 v130 v132 v134 v423 range_2_0 v433 v431 v434 v139 v136 v424 v425 v420 v427 v369 v371 v400 v402 v373 v417 v418 v161 v141 v403 v404 b100 v414 v412 v406 v413 v416 v415 v407 v411 v409 v408 v410 v401 v374 v375 b00000000000000000000000000000000 v376 v397 v395 v391 v378 v396 v398 v382 v387 v392 v394 v385 v388 v393 v379 v389 v381 v390 v380 v384 v386 b000 v372 v370 v163 v165 v361 v365 v362 v363 v364 v359 v169 v329 v343 v353 v351 v354 v172 b1000 v344 v345 v338 v290 v313 v315 v292 v330 v331 v333 v334 v272 v174 v332 b00 v311 v327 v323 v317 v328 v301 v324 v326 v321 v302 v325 v318 v322 v320 v304 v319 v314 v309 v305 v294 v310 v312 v306 v308 v299 v307 v295 v303 v297 v296 v298 v300 v291 v274 v276 v285 v278 v286 v277 v282 v284 v281 v176 v178 v180 v263 v270 v264 v266 v267 v268 v269 b001 v244 v219 v182 v265 b010 v258 v259 v254 v221 v246 v256 range_7_0 v248 v250 v252 v241 v242 v234 v223 v236 v238 b0000 v225 v227 v232 v184 v186 v188 v190 v192 v194 v196 v198 v200 v202 v210 v212 v214 v216 v204 v206 v208 v143 v145 v147 v149 v151 v153 v155 v157 b11 v107 v109 v111 v113 v115 v117 v119 v121 v93 v16 v46 v64 v65 v56 v48 v58 v60 v62 v50 v52 v54 v14 v18 v20 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
% 22.25/4.99 Fol Constants: constB8 constB9 constB7 constB6 constB5 constB4 constB3 constB2 constB1 constB0 constB10 constB11 constB12 constB13 constB14 constB15 constB16 constB17 constB18 constB19 constB20 bitIndex0 bitIndex1 bitIndex5 bitIndex4 bitIndex3 bitIndex2 bitIndex6 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 bitIndex81 bitIndex696 bitIndex122 bitIndex737 bitIndex121 bitIndex736 bitIndex120 bitIndex735 bitIndex119 bitIndex734 bitIndex118 bitIndex733 bitIndex117 bitIndex732 bitIndex116 bitIndex731 bitIndex115 bitIndex730 bitIndex114 bitIndex729 bitIndex113 bitIndex728 bitIndex112 bitIndex727 bitIndex111 bitIndex726 bitIndex110 bitIndex725 bitIndex109 bitIndex724 bitIndex108 bitIndex723 bitIndex107 bitIndex722 bitIndex106 bitIndex721 bitIndex105 bitIndex720 bitIndex104 bitIndex719 bitIndex103 bitIndex718 bitIndex102 bitIndex717 bitIndex101 bitIndex716 bitIndex100 bitIndex715 bitIndex99 bitIndex714 bitIndex98 bitIndex713 bitIndex97 bitIndex712 bitIndex96 bitIndex711 bitIndex95 bitIndex710 bitIndex94 bitIndex709 bitIndex93 bitIndex708 bitIndex92 bitIndex707 bitIndex91 bitIndex706 bitIndex90 bitIndex705 bitIndex89 bitIndex704 bitIndex88 bitIndex703 bitIndex87 bitIndex702 bitIndex86 bitIndex701 bitIndex85 bitIndex700 bitIndex84 bitIndex699 bitIndex83 bitIndex698 bitIndex82 bitIndex697 bitIndex80 bitIndex695 bitIndex79 bitIndex694 bitIndex78 bitIndex693 bitIndex77 bitIndex692 bitIndex76 bitIndex691 bitIndex75 bitIndex690 bitIndex74 bitIndex689 bitIndex73 bitIndex688 bitIndex72 bitIndex687 bitIndex71 bitIndex686 bitIndex70 bitIndex685 bitIndex69 bitIndex684 bitIndex68 bitIndex683 bitIndex67 bitIndex682 bitIndex66 bitIndex681 bitIndex65 bitIndex680 bitIndex64 bitIndex679 bitIndex63 bitIndex678 bitIndex62 bitIndex677 bitIndex61 bitIndex676 bitIndex60 bitIndex675 bitIndex59 bitIndex674 bitIndex58 bitIndex673 bitIndex57 bitIndex672 bitIndex56 bitIndex671 bitIndex55 bitIndex670 bitIndex54 bitIndex669 bitIndex53 bitIndex668 bitIndex52 bitIndex667 bitIndex51 bitIndex666 bitIndex50 bitIndex665 bitIndex49 bitIndex664 bitIndex48 bitIndex663 bitIndex47 bitIndex662 bitIndex46 bitIndex661 bitIndex45 bitIndex660 bitIndex44 bitIndex659 bitIndex43 bitIndex658 bitIndex42 bitIndex657 bitIndex41 bitIndex656 bitIndex40 bitIndex655 bitIndex39 bitIndex654 bitIndex38 bitIndex653 bitIndex37 bitIndex652 bitIndex36 bitIndex651 bitIndex35 bitIndex650 bitIndex34 bitIndex649 bitIndex33 bitIndex648 bitIndex32 bitIndex647 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 skc1
% 22.25/4.99 Fol Functions:
% 22.25/4.99 Problem Properties:
% 22.25/4.99 This is a Bernays Schoenfinkel Ramsey problem.
% 22.25/4.99
% 22.25/4.99
% 22.25/4.99 Reduced Input Clauses:
% 22.25/4.99 5084:1:1:[60.0,52.0]:Top: -> v1010(x0)
% 22.25/4.99 5085:2:1:[60.0,57.1]:Top: v1000(x0,bitIndex0) -> v999(x0)
% 22.25/4.99 5086:1:1:[82.0,62.1]:Top: v1001(x0) ->
% 22.25/4.99 5087:1:1:[81.0,65.1]:Top: v1003(x0) ->
% 22.25/4.99 5088:1:1:[232.0,231.1]:Top: v955(x0) ->
% 22.25/4.99 5089:1:1:[296.0,295.0]:Top: -> v935(x0)
% 22.25/4.99 5090:1:1:[649.0,610.1]:Top: -> v862(x0)
% 22.25/4.99 5091:2:1:[649.0,612.2]:Top: v846(x0) -> v847(x0)
% 22.25/4.99 5092:1:1:[709.0,708.1]:Top: v831(x0) ->
% 22.25/4.99 5093:1:1:[774.0,773.0]:Top: -> v809(x0)
% 22.25/5.00 5094:1:1:[1155.0,1116.1]:Top: -> v728(x0)
% 22.25/5.00 5095:2:1:[1155.0,1118.2]:Top: v711(x0) -> v712(x0)
% 22.25/5.01 5096:1:1:[4046.0,4045.0]:Top: -> v462(x0,bitIndex0)
% 22.25/5.01 5097:1:1:[4452.0,4429.1]:Top: -> v390(x0)
% 22.25/5.01 5098:2:1:[4452.0,4431.2]:Top: v379(x0) -> v380(x0)
% 22.25/5.01
% 22.25/5.01 Most General Atoms: ren1(x0,x1) reachableState(x1) nextState(x0,x1) =(constB0,x0) =(constB1,x0) =(constB2,x0) =(constB3,x0) =(constB4,x0) =(constB5,x0) =(constB6,x0) =(constB7,x0) =(constB8,x0) =(constB9,x0) =(constB10,x0) =(constB11,x0) =(constB12,x0) =(constB13,x0) =(constB14,x0) =(constB15,x0) =(constB16,x0) =(constB17,x0) =(constB18,x0) =(constB19,x0) =(constB20,x0) v1(x1) ren2(x1,x0) v4(x0) v995(x0) v996(x0) v998(x0) v1010(x0) v20(x0) v18(x0) v1000(x0,bitIndex0) v999(x0) v1001(x0) v1000(x0,bitIndex1) v1003(x0) v16(x0) v1004(x0) v1005(x0) v1006(x0) v1008(x0) v1009(x0) v1007(x0,x1) ren3(x1,x0) v8(x2,x1) ren4(x1,x2,x0) ren5(x0,x1) v989(x0,x1) v981(x0) range_3_0(x1) ren6(x1,x2,x0) v987(x0,x1) v23(x0,x1) ren7(x1,x0) v990(x0) v10(x0) v982(x0) ren8(x1) ren9(x0) v983(x0) ren10(x1) v788(x0) ren11(x1) ren12(x1,x0) ren13(x0,x1) v958(x0,x1) v25(x0) v960(x0,x1) ren14(x1,x0) v959(x0) v976(x0) v974(x0) v969(x0) v962(x0) v975(x0) v978(x0) v977(x0) v970(x0) v973(x0) v966(x0) v971(x0) v972(x0) v963(x0) v968(x0) v965(x0) v964(x0) v967(x0) b1110(bitIndex3) b1110(bitIndex2) b1110(bitIndex1) b1110(bitIndex0) v27(x0) v950(x0) ren15(x0) v951(x0) ren16(x0) v954(x0) v803(x0) ren17(x0) v952(x0) ren18(x0) v955(x0) v806(x0) v810(x0) ren19(x0) v953(x0) v802(x0) v832(x0) v807(x0) v29(x1,bitIndex0) ren20(x1,x0) ren21(x0) v946(x0) v938(x0) ren22(x1,x0) ren23(x0) v944(x0) v31(x0,bitIndex0) v824(x0) v939(x0) ren24(x1) ren25(x0) v941(x0) ren26(x1) v817(x0) ren27(x1) v930(x0) ren28(x0) v934(x0) v931(x0) ren29(x0) v935(x0) v933(x0) v932(x0) v33(x0) v35(x0) v37(x2,x1) ren30(x1,x2,x0) ren31(x0,x1) v924(x0,x1) v914(x0) ren32(x1,x2,x0) v922(x0,x1) v42(x0,x1) range_4_0(x0) ren33(x1,x0) v925(x0) v39(x0) v915(x0) ren34(x1) ren35(x0) v916(x0) ren36(x1) v918(x0) ren37(x1) v911(x1) ren38(x1,x0) ren39(x1,x0) ren40(x0,x1) v881(x0,x1) v879(x0) ren41(x0,x1) v840(x0,x1) v838(x0) ren42(x0,x1) v836(x0) v908(x0) v909(x0,bitIndex1) v909(x0,bitIndex0) v67(x0) v44(x0) v883(x0,x1) ren43(x1,x0) ren44(x0,x1) b01111(x1) v882(x0) v905(x0) v903(x0) v898(x0) v893(x0) v885(x0) v904(x0) v907(x0) v906(x0) v899(x0) v902(x0) v890(x0) v900(x0) v901(x0) v894(x0) v897(x0) v889(x0) v895(x0) v896(x0) v886(x0) v892(x0) v888(x0) v887(x0) v891(x0) v880(x0,bitIndex1) v880(x0,bitIndex0) v842(x0,x1) ren45(x1,x0) v841(x0) range_31_0(x1) v843(x0,x1) range_5_0(x0) ren46(x1,x0) v877(x0) v875(x0) v871(x0) v867(x0) v863(x0) v845(x0) v876(x0) v878(x0) v857(x0) v872(x0) v874(x0) v855(x0) v858(x0) v873(x0) v868(x0) v870(x0) v853(x0) v859(x0) v869(x0) v864(x0) v866(x0) v851(x0) v860(x0) v865(x0) v846(x0) v861(x0) v848(x0) v862(x0) v14(x0) v847(x0) v850(x0) v852(x0) v854(x0) v856(x0) v849(x0,x1) ren47(x1,x0) v839(x0,bitIndex1) v839(x0,bitIndex0) v837(x0,bitIndex1) v837(x0,bitIndex0) v69(x0) v828(x0) ren48(x0) v829(x0) ren49(x0) v833(x0) ren50(x0) v830(x0) ren51(x0) v834(x0) ren52(x0) v831(x0) v71(x0) v29(x1,bitIndex1) ren53(x1,x0) ren54(x0) v823(x0) v813(x0) ren55(x1,x0) ren56(x0) v821(x0) v31(x0,bitIndex1) v12(x0) v814(x0) ren57(x1) ren58(x0) v815(x0) ren59(x1) ren60(x1) v779(x1) ren61(x1,x0) v800(x0) ren62(x0) v808(x0) ren63(x0) v809(x0) v801(x0) v804(x0) v805(x0) v73(x0) v75(x2,x1) ren64(x1,x2,x0) ren65(x0,x1) v794(x0,x1) v784(x0) ren66(x1,x2,x0) v792(x0,x1) v77(x0,x1) ren67(x1,x0) v795(x0) v785(x0) ren68(x1) ren69(x0) v786(x0) ren70(x1) ren71(x1) v777(x1) ren72(x1,x0) v781(x0) v340(x0) ren73(x1,x0) ren74(x0,x1) v747(x0,x1) v745(x0) ren75(x0,x1) v705(x0,x1) v703(x0) ren76(x0,x1) v701(x0) v774(x0) v775(x0,bitIndex1) v775(x0,bitIndex0) v79(x0) v749(x0,x1) ren77(x1,x0) ren78(x0,x1) v748(x0) v771(x0) v769(x0) v764(x0) v759(x0) v751(x0) v770(x0) v773(x0) v772(x0) v765(x0) v768(x0) v756(x0) v766(x0) v767(x0) v760(x0) v763(x0) v755(x0) v761(x0) v762(x0) v752(x0) v758(x0) v754(x0) v753(x0) v757(x0) v746(x0,bitIndex1) v746(x0,bitIndex0) v707(x0,x1) ren79(x1,x0) v706(x0) v708(x0,x1) ren80(x1,x0) =(bitIndex0,x0) =(bitIndex1,x0) =(bitIndex2,x0) =(bitIndex3,x0) =(bitIndex4,x0) =(bitIndex5,x0) v743(x0) v741(x0) v737(x0) v733(x0) v729(x0) v710(x0) v742(x0) v744(x0) v723(x0) v738(x0) v740(x0) v721(x0) v724(x0) v739(x0) v734(x0) v736(x0) v719(x0) v725(x0) v735(x0) v730(x0) v732(x0) v717(x0) v726(x0) v731(x0) v711(x0) v727(x0) v713(x0) v728(x0) v712(x0) v716(x0) v718(x0) v720(x0) v722(x0) v714(x0,x1) ren81(x1,x0) v704(x0,bitIndex1) v704(x0,bitIndex0) b00000(bitIndex4) b00000(bitIndex3) b00000(bitIndex2) b00000(bitIndex1) b00000(bitIndex0) v702(x0,bitIndex1) v702(x0,bitIndex0) v81(x0) v83(x0) v85(x0) v87(x0) v89(x1) ren82(x1,x0) ren83(x0) v693(x0) v685(x0) ren84(x1,x0) ren85(x0) v691(x0) v95(x0) v694(x0) v91(x0) v686(x0) ren86(x1) ren87(x0) v687(x0) ren88(x1) v347(x0) ren89(x1) v677(x0) ren90(x0) v682(x0) v679(x0) v678(x0) v681(x0) v283(x0) v680(x0) v280(x0) v452(x0) v97(x0,x1) ren91(x1,x0) v99(x0) range_1_0(x1) v607(x1,x0) ren92(x0,x1) b01(x1) v661(x0) v653(x0) ren93(x0,x1) v645(x0) v608(x0) v663(x0) v672(x0) v674(x0) v627(x0) v675(x0) v495(x0,bitIndex5) v624(x0) v495(x0,bitIndex4) v664(x0) v669(x0) v671(x0) v495(x0,bitIndex6) v667(x0) v666(x0) v626(x0) v668(x0) v619(x0) v495(x0,bitIndex3) v654(x0) v656(x0) v658(x0) v659(x0) v660(x0) v625(x0) v636(x0) v647(x0) v652(x1,x0) ren94(x0,x1) b10(x1) v592(x0) v648(x0) v649(x0) v650(x0) v651(x0) v623(x0) v621(x0) v495(x0,bitIndex1) v610(x0) v643(x0) v630(x0) v611(x0) v641(x0) v616(x0) v612(x0) v638(x0) v640(x0) v634(x0) v613(x0) v631(x0) v633(x0) v635(x0) v637(x0) v495(x0,bitIndex0) v622(x0) v614(x0) v628(x0) v617(x0) v618(x0) v620(x0) v495(x0,bitIndex2) ren95(x0,x1) ren96(x0,x1) ren97(x0,x1) ren98(x0,x1) ren99(x0,x1) ren100(x0,x1) ren101(x0,x1) ren102(x0,x1) v501(x1,bitIndex730) ren103(x0,x1) v501(x1,bitIndex729) ren104(x0,x1) v501(x1,bitIndex728) ren105(x0,x1) v501(x1,bitIndex727) ren106(x0,x1) v501(x1,bitIndex726) ren107(x0,x1) v501(x1,bitIndex725) ren108(x0,x1) v501(x1,bitIndex724) ren109(x0,x1) v501(x1,bitIndex723) ren110(x0,x1) v501(x1,bitIndex722) ren111(x0,x1) v501(x1,bitIndex721) ren112(x0,x1) v501(x1,bitIndex720) ren113(x0,x1) v501(x1,bitIndex719) ren114(x0,x1) v501(x1,bitIndex718) ren115(x0,x1) v501(x1,bitIndex717) ren116(x0,x1) v501(x1,bitIndex716) ren117(x0,x1) v501(x1,bitIndex715) ren118(x0,x1) v501(x1,bitIndex714) ren119(x0,x1) v501(x1,bitIndex713) ren120(x0,x1) v501(x1,bitIndex712) ren121(x0,x1) v501(x1,bitIndex711) ren122(x0,x1) v501(x1,bitIndex710) ren123(x0,x1) v501(x1,bitIndex709) ren124(x0,x1) v501(x1,bitIndex708) ren125(x0,x1) v501(x1,bitIndex707) ren126(x0,x1) v501(x1,bitIndex706) ren127(x0,x1) v501(x1,bitIndex705) ren128(x0,x1) v501(x1,bitIndex704) ren129(x0,x1) v501(x1,bitIndex703) ren130(x0,x1) v501(x1,bitIndex702) ren131(x0,x1) v501(x1,bitIndex701) ren132(x0,x1) v501(x1,bitIndex700) ren133(x0,x1) v501(x1,bitIndex699) ren134(x0,x1) v501(x1,bitIndex698) ren135(x0,x1) v501(x1,bitIndex697) ren136(x0,x1) v501(x1,bitIndex696) ren137(x0,x1) v501(x1,bitIndex695) ren138(x0,x1) v501(x1,bitIndex694) ren139(x0,x1) v501(x1,bitIndex693) ren140(x0,x1) v501(x1,bitIndex692) ren141(x0,x1) v501(x1,bitIndex691) ren142(x0,x1) v501(x1,bitIndex690) ren143(x0,x1) v501(x1,bitIndex689) ren144(x0,x1) v501(x1,bitIndex688) ren145(x0,x1) v501(x1,bitIndex687) ren146(x0,x1) v501(x1,bitIndex686) ren147(x0,x1) v501(x1,bitIndex685) ren148(x0,x1) v501(x1,bitIndex684) ren149(x0,x1) v501(x1,bitIndex683) ren150(x0,x1) v501(x1,bitIndex682) ren151(x0,x1) v501(x1,bitIndex681) ren152(x0,x1) v501(x1,bitIndex680) ren153(x0,x1) v501(x1,bitIndex679) ren154(x0,x1) v501(x1,bitIndex678) ren155(x0,x1) v501(x1,bitIndex677) ren156(x0,x1) v501(x1,bitIndex676) ren157(x0,x1) v501(x1,bitIndex675) ren158(x0,x1) v501(x1,bitIndex674) ren159(x0,x1) v501(x1,bitIndex673) ren160(x0,x1) v501(x1,bitIndex672) ren161(x0,x1) v501(x1,bitIndex671) ren162(x0,x1) v501(x1,bitIndex670) ren163(x0,x1) v501(x1,bitIndex669) ren164(x0,x1) v501(x1,bitIndex668) ren165(x0,x1) v501(x1,bitIndex667) ren166(x0,x1) v501(x1,bitIndex666) ren167(x0,x1) v501(x1,bitIndex665) ren168(x0,x1) v501(x1,bitIndex664) ren169(x0,x1) v501(x1,bitIndex663) ren170(x0,x1) v501(x1,bitIndex662) ren171(x0,x1) v501(x1,bitIndex661) ren172(x0,x1) v501(x1,bitIndex660) ren173(x0,x1) v501(x1,bitIndex659) ren174(x0,x1) v501(x1,bitIndex658) ren175(x0,x1) v501(x1,bitIndex657) ren176(x0,x1) v501(x1,bitIndex656) ren177(x0,x1) v501(x1,bitIndex655) ren178(x0,x1) v501(x1,bitIndex654) ren179(x0,x1) v501(x1,bitIndex653) ren180(x0,x1) v501(x1,bitIndex652) ren181(x0,x1) v501(x1,bitIndex651) ren182(x0,x1) v501(x1,bitIndex650) ren183(x0,x1) v501(x1,bitIndex649) ren184(x0,x1) v501(x1,bitIndex648) ren185(x0,x1) v501(x1,bitIndex647) ren186(x0,x1) v501(x1,bitIndex646) ren187(x0,x1) v501(x1,bitIndex645) ren188(x0,x1) v501(x1,bitIndex644) ren189(x0,x1) v501(x1,bitIndex643) ren190(x0,x1) v501(x1,bitIndex642) ren191(x0,x1) v501(x1,bitIndex641) ren192(x0,x1) v501(x1,bitIndex640) ren193(x0,x1) v501(x1,bitIndex639) ren194(x0,x1) v501(x1,bitIndex638) ren195(x0,x1) v501(x1,bitIndex637) ren196(x0,x1) v501(x1,bitIndex636) ren197(x0,x1) v501(x1,bitIndex635) ren198(x0,x1) v501(x1,bitIndex634) ren199(x0,x1) v501(x1,bitIndex633) ren200(x0,x1) v501(x1,bitIndex632) ren201(x0,x1) v501(x1,bitIndex631) ren202(x0,x1) v501(x1,bitIndex630) ren203(x0,x1) v501(x1,bitIndex629) ren204(x0,x1) v501(x1,bitIndex628) ren205(x0,x1) v501(x1,bitIndex627) ren206(x0,x1) v501(x1,bitIndex626) ren207(x0,x1) v501(x1,bitIndex625) ren208(x0,x1) v501(x1,bitIndex624) ren209(x0,x1) v501(x1,bitIndex623) ren210(x0,x1) v501(x1,bitIndex622) ren211(x0,x1) v501(x1,bitIndex621) ren212(x0,x1) v501(x1,bitIndex620) ren213(x0,x1) v501(x1,bitIndex619) ren214(x0,x1) v501(x1,bitIndex618) ren215(x0,x1) v501(x1,bitIndex617) ren216(x0,x1) v501(x1,bitIndex616) ren217(x0,x1) v501(x1,bitIndex615) ren218(x1,x0) ren219(x0,x1) v594(x0,x1) v581(x0,x1) v596(x0) ren220(x0) v597(x0) v562(x0) ren221(x1) ren222(x0) v599(x0) ren223(x1) v474(x0) ren224(x1) v501(x0,bitIndex573) v497(x0,x1) v499(x0,x1) range_122_116(x0) ren225(x1,x0) v501(x0,bitIndex737) v501(x0,bitIndex736) v501(x0,bitIndex735) v501(x0,bitIndex734) v501(x0,bitIndex733) v501(x0,bitIndex732) v501(x0,bitIndex731) ren226(x0,x1) ren227(x0,x1) ren228(x0,x1) ren229(x0,x1) ren230(x0,x1) ren231(x0,x1) ren232(x0,x1) ren233(x0,x1) ren234(x0,x1) ren235(x0,x1) ren236(x0,x1) ren237(x0,x1) ren238(x0,x1) ren239(x0,x1) ren240(x0,x1) ren241(x0,x1) ren242(x0,x1) ren243(x0,x1) ren244(x0,x1) ren245(x0,x1) ren246(x0,x1) ren247(x0,x1) ren248(x0,x1) ren249(x0,x1) ren250(x0,x1) ren251(x0,x1) ren252(x0,x1) ren253(x0,x1) ren254(x0,x1) ren255(x0,x1) ren256(x0,x1) ren257(x0,x1) ren258(x0,x1) ren259(x0,x1) ren260(x0,x1) ren261(x0,x1) ren262(x0,x1) ren263(x0,x1) ren264(x0,x1) ren265(x0,x1) ren266(x0,x1) ren267(x0,x1) ren268(x0,x1) ren269(x0,x1) ren270(x0,x1) ren271(x0,x1) ren272(x0,x1) ren273(x0,x1) ren274(x0,x1) ren275(x0,x1) ren276(x0,x1) ren277(x0,x1) ren278(x0,x1) ren279(x0,x1) ren280(x0,x1) ren281(x0,x1) ren282(x0,x1) ren283(x0,x1) ren284(x0,x1) ren285(x0,x1) ren286(x0,x1) ren287(x0,x1) ren288(x0,x1) ren289(x0,x1) ren290(x0,x1) ren291(x0,x1) ren292(x0,x1) ren293(x0,x1) ren294(x0,x1) ren295(x0,x1) ren296(x0,x1) ren297(x0,x1) ren298(x0,x1) ren299(x0,x1) ren300(x0,x1) ren301(x0,x1) ren302(x0,x1) ren303(x0,x1) ren304(x0,x1) ren305(x0,x1) ren306(x0,x1) ren307(x0,x1) ren308(x0,x1) ren309(x0,x1) ren310(x0,x1) ren311(x0,x1) ren312(x0,x1) ren313(x0,x1) ren314(x0,x1) ren315(x0,x1) ren316(x0,x1) ren317(x0,x1) ren318(x0,x1) ren319(x0,x1) ren320(x0,x1) ren321(x0,x1) ren322(x0,x1) ren323(x0,x1) ren324(x0,x1) ren325(x0,x1) ren326(x0,x1) ren327(x0,x1) ren328(x0,x1) ren329(x0,x1) ren330(x0,x1) ren331(x0,x1) ren332(x0,x1) ren333(x0,x1) ren334(x0,x1) ren335(x0,x1) ren336(x0,x1) ren337(x0,x1) ren338(x0,x1) ren339(x0,x1) ren340(x0,x1) ren341(x0,x1) ren342(x0,x1) ren343(x0,x1) ren344(x0,x1) ren345(x0,x1) ren346(x0,x1) ren347(x0,x1) ren348(x0,x1) ren349(x1,x0) ren350(x0,x1) v553(x0,x1) v554(x0) ren351(x1,x2,x0) v579(x0,x1) v582(x0,x1) range_122_0(x0) ren352(x1,x0) v564(x0) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex122) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex121) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex120) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex119) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex118) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex117) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex116) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex115) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex114) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex113) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex112) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex111) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex110) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex109) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex108) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex107) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex106) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex105) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex104) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex103) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex102) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex101) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex100) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex99) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex98) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex97) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex96) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex95) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex94) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex93) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex92) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex91) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex90) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex89) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex88) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex87) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex86) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex85) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex84) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex83) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex82) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex81) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex80) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex79) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex78) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex77) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex76) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex75) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex74) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex73) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex72) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex71) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex70) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex69) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex68) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex67) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex66) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex65) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex64) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex63) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex62) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex61) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex60) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex59) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex58) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex57) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex56) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex55) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex54) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex53) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex52) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex51) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex50) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex49) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex48) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex47) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex46) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex45) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex44) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex43) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex42) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex41) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex40) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex39) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex38) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex37) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex36) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex35) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex34) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex33) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex32) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex31) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex30) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex29) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex28) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex27) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex26) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex25) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex24) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex23) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex22) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex21) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex20) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex19) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex18) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex17) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex16) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex15) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex14) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex13) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex12) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex11) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex10) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex9) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex8) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex7) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex6) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex5) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex4) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex3) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex2) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex1) b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000(bitIndex0) v546(x0,x1) ren353(x1,x0) ren354(x0,x1) v504(x0,x1) v570(x0) ren355(x0) v501(x0,bitIndex614) ren356(x0) v501(x0,bitIndex613) ren357(x0) v501(x0,bitIndex612) ren358(x0) v501(x0,bitIndex611) ren359(x0) v501(x0,bitIndex610) ren360(x0) v501(x0,bitIndex609) ren361(x0) v501(x0,bitIndex608) ren362(x0) v501(x0,bitIndex607) ren363(x0) v501(x0,bitIndex606) ren364(x0) v501(x0,bitIndex605) ren365(x0) v501(x0,bitIndex604) ren366(x0) v501(x0,bitIndex603) ren367(x0) v501(x0,bitIndex602) ren368(x0) v501(x0,bitIndex601) ren369(x0) v501(x0,bitIndex600) ren370(x0) v501(x0,bitIndex599) ren371(x0) v501(x0,bitIndex598) ren372(x0) v501(x0,bitIndex597) ren373(x0) v501(x0,bitIndex596) ren374(x0) v501(x0,bitIndex595) ren375(x0) v501(x0,bitIndex594) ren376(x0) v501(x0,bitIndex593) ren377(x0) v501(x0,bitIndex592) ren378(x0) v501(x0,bitIndex591) ren379(x0) v501(x0,bitIndex590) ren380(x0) v501(x0,bitIndex589) ren381(x0) v501(x0,bitIndex588) ren382(x0) v501(x0,bitIndex587) ren383(x0) v501(x0,bitIndex586) ren384(x0) v501(x0,bitIndex585) ren385(x0) v501(x0,bitIndex584) ren386(x0) v501(x0,bitIndex583) ren387(x0) v501(x0,bitIndex582) ren388(x0) v501(x0,bitIndex581) ren389(x0) v501(x0,bitIndex580) ren390(x0) v501(x0,bitIndex579) ren391(x0) v501(x0,bitIndex578) ren392(x0) v501(x0,bitIndex577) ren393(x0) v501(x0,bitIndex576) ren394(x0) v501(x0,bitIndex575) ren395(x0) v501(x0,bitIndex574) ren396(x0) ren397(x0) v501(x0,bitIndex572) ren398(x0) v501(x0,bitIndex571) ren399(x0) v501(x0,bitIndex570) ren400(x0) v501(x0,bitIndex569) ren401(x0) v501(x0,bitIndex568) ren402(x0) v501(x0,bitIndex567) ren403(x0) v501(x0,bitIndex566) ren404(x0) v501(x0,bitIndex565) ren405(x0) v501(x0,bitIndex564) ren406(x0) v501(x0,bitIndex563) ren407(x0) v501(x0,bitIndex562) ren408(x0) v501(x0,bitIndex561) ren409(x0) v501(x0,bitIndex560) ren410(x0) v501(x0,bitIndex559) ren411(x0) v501(x0,bitIndex558) ren412(x0) v501(x0,bitIndex557) ren413(x0) v501(x0,bitIndex556) ren414(x0) v501(x0,bitIndex555) ren415(x0) v501(x0,bitIndex554) ren416(x0) v501(x0,bitIndex553) ren417(x0) v501(x0,bitIndex552) ren418(x0) v501(x0,bitIndex551) ren419(x0) v501(x0,bitIndex550) ren420(x0) v501(x0,bitIndex549) ren421(x0) v501(x0,bitIndex548) ren422(x0) v501(x0,bitIndex547) ren423(x0) v501(x0,bitIndex546) ren424(x0) v501(x0,bitIndex545) ren425(x0) v501(x0,bitIndex544) ren426(x0) v501(x0,bitIndex543) ren427(x0) v501(x0,bitIndex542) ren428(x0) v501(x0,bitIndex541) ren429(x0) v501(x0,bitIndex540) ren430(x0) v501(x0,bitIndex539) ren431(x0) v501(x0,bitIndex538) ren432(x0) v501(x0,bitIndex537) ren433(x0) v501(x0,bitIndex536) ren434(x0) v501(x0,bitIndex535) ren435(x0) v501(x0,bitIndex534) ren436(x0) v501(x0,bitIndex533) ren437(x0) v501(x0,bitIndex532) ren438(x0) v501(x0,bitIndex531) ren439(x0) v501(x0,bitIndex530) ren440(x0) v501(x0,bitIndex529) ren441(x0) v501(x0,bitIndex528) ren442(x0) v501(x0,bitIndex527) ren443(x0) v501(x0,bitIndex526) ren444(x0) v501(x0,bitIndex525) ren445(x0) v501(x0,bitIndex524) ren446(x0) v501(x0,bitIndex523) ren447(x0) v501(x0,bitIndex522) ren448(x0) v501(x0,bitIndex521) ren449(x0) v501(x0,bitIndex520) ren450(x0) v501(x0,bitIndex519) ren451(x0) v501(x0,bitIndex518) ren452(x0) v501(x0,bitIndex517) ren453(x0) v501(x0,bitIndex516) ren454(x0) v501(x0,bitIndex515) ren455(x0) v501(x0,bitIndex514) ren456(x0) v501(x0,bitIndex513) ren457(x0) v501(x0,bitIndex512) ren458(x0) v501(x0,bitIndex511) ren459(x0) v501(x0,bitIndex510) ren460(x0) v501(x0,bitIndex509) ren461(x0) v501(x0,bitIndex508) ren462(x0) v501(x0,bitIndex507) ren463(x0) v501(x0,bitIndex506) ren464(x0) v501(x0,bitIndex505) ren465(x0) v501(x0,bitIndex504) ren466(x0) v501(x0,bitIndex503) ren467(x0) v501(x0,bitIndex502) ren468(x0) v501(x0,bitIndex501) ren469(x0) v501(x0,bitIndex500) ren470(x0) v501(x0,bitIndex499) ren471(x0) v501(x0,bitIndex498) ren472(x0) v501(x0,bitIndex497) ren473(x0) v501(x0,bitIndex496) ren474(x0) v501(x0,bitIndex495) ren475(x0) v501(x0,bitIndex494) ren476(x0) v501(x0,bitIndex493) ren477(x0) v501(x0,bitIndex492) ren478(x0) v568(x0) ren479(x0) v555(x0) ren480(x1) ren481(x1,x0) v560(x0) v563(x0) v575(x0) v576(x0) v577(x0) v578(x0,bitIndex1) v578(x0,bitIndex0) v123(x0) v105(x0) v565(x0) v566(x0) v574(x0) v567(x0) v572(x0) v573(x0,bitIndex1) v573(x0,bitIndex0) v571(x0,bitIndex1) v571(x0,bitIndex0) v569(x0,bitIndex1) v569(x0,bitIndex0) v103(x0) ren482(x0) v556(x0) ren483(x1) ren484(x1) v551(x0,x1) ren485(x1,x0) v550(x0,x1) ren486(x1,x0) ren487(x0,x1) v527(x0,x1) v548(x0) v508(x0,bitIndex1) v544(x0,x1) ren488(x1,x0) v543(x0,x1) ren489(x1,x0) ren490(x0,x1) v506(x0) =(bitIndex6,x0) =(bitIndex7,x0) =(bitIndex8,x0) =(bitIndex9,x0) =(bitIndex10,x0) =(bitIndex11,x0) =(bitIndex12,x0) =(bitIndex13,x0) =(bitIndex14,x0) =(bitIndex15,x0) =(bitIndex16,x0) =(bitIndex17,x0) =(bitIndex18,x0) =(bitIndex19,x0) =(bitIndex20,x0) =(bitIndex21,x0) =(bitIndex22,x0) =(bitIndex23,x0) =(bitIndex24,x0) =(bitIndex25,x0) =(bitIndex26,x0) =(bitIndex27,x0) =(bitIndex28,x0) =(bitIndex29,x0) =(bitIndex30,x0) =(bitIndex31,x0) =(bitIndex32,x0) =(bitIndex33,x0) =(bitIndex34,x0) =(bitIndex35,x0) =(bitIndex36,x0) =(bitIndex37,x0) =(bitIndex38,x0) =(bitIndex39,x0) =(bitIndex40,x0) =(bitIndex41,x0) =(bitIndex42,x0) =(bitIndex43,x0) =(bitIndex44,x0) =(bitIndex45,x0) =(bitIndex46,x0) =(bitIndex47,x0) =(bitIndex48,x0) =(bitIndex49,x0) =(bitIndex50,x0) =(bitIndex51,x0) =(bitIndex52,x0) =(bitIndex53,x0) =(bitIndex54,x0) =(bitIndex55,x0) =(bitIndex56,x0) =(bitIndex57,x0) =(bitIndex58,x0) =(bitIndex59,x0) =(bitIndex60,x0) =(bitIndex61,x0) =(bitIndex62,x0) =(bitIndex63,x0) =(bitIndex64,x0) =(bitIndex65,x0) =(bitIndex66,x0) =(bitIndex67,x0) =(bitIndex68,x0) =(bitIndex69,x0) =(bitIndex70,x0) =(bitIndex71,x0) =(bitIndex72,x0) =(bitIndex73,x0) =(bitIndex74,x0) =(bitIndex75,x0) =(bitIndex76,x0) =(bitIndex77,x0) =(bitIndex78,x0) =(bitIndex79,x0) =(bitIndex80,x0) =(bitIndex81,x0) =(bitIndex82,x0) =(bitIndex83,x0) =(bitIndex84,x0) =(bitIndex85,x0) =(bitIndex86,x0) =(bitIndex87,x0) =(bitIndex88,x0) =(bitIndex89,x0) =(bitIndex90,x0) =(bitIndex91,x0) =(bitIndex92,x0) =(bitIndex93,x0) =(bitIndex94,x0) =(bitIndex95,x0) =(bitIndex96,x0) =(bitIndex97,x0) =(bitIndex98,x0) =(bitIndex99,x0) =(bitIndex100,x0) =(bitIndex101,x0) =(bitIndex102,x0) =(bitIndex103,x0) =(bitIndex104,x0) =(bitIndex105,x0) =(bitIndex106,x0) =(bitIndex107,x0) =(bitIndex108,x0) =(bitIndex109,x0) =(bitIndex110,x0) =(bitIndex111,x0) =(bitIndex112,x0) =(bitIndex113,x0) =(bitIndex114,x0) =(bitIndex115,x0) =(bitIndex116,x0) =(bitIndex117,x0) =(bitIndex118,x0) =(bitIndex119,x0) =(bitIndex120,x0) =(bitIndex121,x0) =(bitIndex122,x0) v529(x0,x1) ren491(x1,x0) v531(x0,x1) ren492(x1,x0) v533(x0,x1) ren493(x1,x0) v535(x0,x1) ren494(x1,x0) v537(x0,x1) ren495(x1,x0) v539(x0,x1) ren496(x1,x0) v541(x0,x1) ren497(x1,x0) v510(x0,x1) v513(x0,x1) ren498(x1,x0) ren499(x0,x1) v512(x0,x1) v511(x0) range_8_0(x1) v464(x0,x1) ren500(x1,x0) ren501(x0,x1) v522(x0,x1) v520(x0) ren502(x0,x1) v518(x0,x1) v516(x0) ren503(x0,x1) v514(x0) v524(x0) v525(x0,bitIndex1) v525(x0,bitIndex0) v521(x0,bitIndex1) v521(x0,bitIndex0) v517(x0,bitIndex1) v517(x0,bitIndex0) v515(x0,bitIndex1) v515(x0,bitIndex0) v462(x0,x1) range_8_1(x0) ren504(x1,x0) v101(x1) ren505(x1,x0) ren506(x0) v490(x0) v470(x0) ren507(x1,x0) ren508(x0) v488(x0) v491(x0) v487(x0) ren509(x0) v471(x0) v480(x0) ren510(x1) ren511(x1,x0) v478(x0) v481(x0) v482(x0) v483(x0) v486(x0) v484(x0) v485(x0) v460(x0,bitIndex1) ren512(x0) v472(x0) ren513(x1) ren514(x1) v467(x1) ren515(x1,x0) v463(x0,x1) ren516(x1,x0) v125(x0) v446(x0) ren517(x0) v455(x0) v448(x0) ren518(x0) v456(x0) v451(x0) v279(x0) ren519(x0) v458(x0) ren520(x0) v457(x0) v167(x0) v439(x0) v447(x0) v454(x0) v453(x0) v449(x0) v450(x0) v444(x0) v441(x0,bitIndex2) v441(x0,bitIndex0) v441(x0,bitIndex1) v130(x0) v132(x0) v134(x2,x1) ren521(x1,x2,x0) ren522(x0,x1) v433(x0,x1) v423(x0) ren523(x1,x2,x0) v431(x0,x1) v139(x0,x1) range_2_0(x0) ren524(x1,x0) v434(x0) v136(x0) v424(x0) ren525(x1) ren526(x0) v425(x0) ren527(x1) v427(x0) ren528(x1) v420(x1) ren529(x1,x0) ren530(x1,x0) ren531(x0,x1) v402(x0,x1) v400(x0) ren532(x0,x1) v373(x0,x1) v371(x0) ren533(x0,x1) v369(x0) v417(x0) v418(x0,bitIndex1) v418(x0,bitIndex0) v161(x0) v141(x0) v404(x0,x1) ren534(x1,x0) ren535(x0,x1) b100(x1) v403(x0) v414(x0) v412(x0) v406(x0) v413(x0) v416(x0) v415(x0) v407(x0) v411(x0) v409(x0) v408(x0) v410(x0) v401(x0,bitIndex1) v401(x0,bitIndex0) v375(x0,x1) ren536(x1,x0) v374(x0) b00000000000000000000000000000000(bitIndex31) b00000000000000000000000000000000(bitIndex30) b00000000000000000000000000000000(bitIndex29) b00000000000000000000000000000000(bitIndex28) b00000000000000000000000000000000(bitIndex27) b00000000000000000000000000000000(bitIndex26) b00000000000000000000000000000000(bitIndex25) b00000000000000000000000000000000(bitIndex24) b00000000000000000000000000000000(bitIndex23) b00000000000000000000000000000000(bitIndex22) b00000000000000000000000000000000(bitIndex21) b00000000000000000000000000000000(bitIndex20) b00000000000000000000000000000000(bitIndex19) b00000000000000000000000000000000(bitIndex18) b00000000000000000000000000000000(bitIndex17) b00000000000000000000000000000000(bitIndex16) b00000000000000000000000000000000(bitIndex15) b00000000000000000000000000000000(bitIndex14) b00000000000000000000000000000000(bitIndex13) b00000000000000000000000000000000(bitIndex12) b00000000000000000000000000000000(bitIndex11) b00000000000000000000000000000000(bitIndex10) b00000000000000000000000000000000(bitIndex9) b00000000000000000000000000000000(bitIndex8) b00000000000000000000000000000000(bitIndex7) b00000000000000000000000000000000(bitIndex6) b00000000000000000000000000000000(bitIndex5) b00000000000000000000000000000000(bitIndex4) b00000000000000000000000000000000(bitIndex3) b00000000000000000000000000000000(bitIndex2) b00000000000000000000000000000000(bitIndex1) b00000000000000000000000000000000(bitIndex0) v376(x0,x1) ren537(x1,x0) v397(x0) v395(x0) v391(x0) v378(x0) v396(x0) v398(x0) v387(x0) v392(x0) v394(x0) v385(x0) v388(x0) v393(x0) v379(x0) v389(x0) v381(x0) v390(x0) v380(x0) v384(x0) v386(x0) v382(x0,x1) ren538(x1,x0) b000(bitIndex2) b000(bitIndex1) b000(bitIndex0) v372(x0,bitIndex1) v372(x0,bitIndex0) v370(x0,bitIndex1) v370(x0,bitIndex0) v163(x0) v165(x0) v361(x0) ren539(x0) v365(x0) v362(x0) v363(x0) v364(x0) v359(x0) v329(x0) v169(x2,x1) ren540(x1,x2,x0) ren541(x0,x1) v353(x0,x1) v343(x0) ren542(x1,x2,x0) v351(x0,x1) v172(x0,x1) ren543(x1,x0) ren544(x0,x1) b1000(x1) v354(x0) v344(x0) ren545(x1) ren546(x0) v345(x0) ren547(x1) ren548(x1) v336(x1) ren549(x1,x0) v338(x0) ren550(x1,x0) ren551(x0,x1) v315(x0,x1) v313(x0) ren552(x0,x1) v292(x0,x1) v290(x0) v330(x0) v331(x0) v333(x0) v334(x0,bitIndex1) v334(x0,bitIndex0) v272(x0) v174(x0) v332(x0,bitIndex1) v332(x0,bitIndex0) b00(bitIndex1) b00(bitIndex0) v311(x0) v327(x0) v323(x0) v317(x0) v328(x0) v301(x0) v324(x0) v326(x0) v321(x0) v302(x0) v325(x0) v318(x0) v322(x0) v320(x0) v304(x0) v319(x0) v314(x0,bitIndex1) v314(x0,bitIndex0) v309(x0) v305(x0) v294(x0) v310(x0) v312(x0) v306(x0) v308(x0) v299(x0) v307(x0) v295(x0) v303(x0) v297(x0) v296(x0) v298(x0) v300(x0) v291(x0,bitIndex1) v291(x0,bitIndex0) v274(x0) v276(x0) ren553(x0) v285(x0) v278(x0) ren554(x0) v286(x0) v277(x0) v282(x0) v284(x0) v281(x0) v176(x0) v178(x0) v180(x0) v263(x0) ren555(x0) v270(x0) v264(x0) v266(x0) v267(x0) v268(x0) v269(x0,bitIndex2) v269(x0,bitIndex1) v269(x0,bitIndex0) b001(bitIndex2) b001(bitIndex1) b001(bitIndex0) v244(x0) v219(x0) v182(x0) v265(x0,bitIndex2) v265(x0,bitIndex1) v265(x0,bitIndex0) b010(bitIndex2) b010(bitIndex1) b010(bitIndex0) v258(x0) v259(x0) v254(x0) ren556(x0) v221(x0,bitIndex7) ren557(x0) v221(x0,bitIndex6) ren558(x0) v221(x0,bitIndex5) ren559(x0) v221(x0,bitIndex4) ren560(x0) v221(x0,bitIndex3) ren561(x0) v221(x0,bitIndex2) ren562(x0) v221(x0,bitIndex1) ren563(x0) v221(x0,bitIndex0) v256(x0) v246(x0,x1) v248(x0,x1) range_7_0(x0) ren564(x1,x0) v250(x0,x1) ren565(x1,x0) v252(x0,bitIndex400) v252(x0,bitIndex399) v252(x0,bitIndex398) v252(x0,bitIndex397) v252(x0,bitIndex396) v252(x0,bitIndex395) v252(x0,bitIndex394) v252(x0,bitIndex393) v241(x0) v242(x0) v234(x0) ren566(x0) ren567(x0) ren568(x0) ren569(x0) ren570(x0) ren571(x0) ren572(x0) ren573(x0) v236(x0) v238(x0,bitIndex3) v238(x0,bitIndex2) v238(x0,bitIndex1) v238(x0,bitIndex0) b0000(bitIndex3) b0000(bitIndex2) b0000(bitIndex1) b0000(bitIndex0) v223(x0,x1) v225(x0,x1) ren574(x1,x0) v227(x0,x1) ren575(x1,x0) v232(x0,x1) ren576(x1,x0) v184(x0) v186(x0) v188(x0) v190(x0) v192(x0) v194(x0) v196(x0) v198(x0) v200(x0) v202(x0) v210(x0) v212(x0,bitIndex6) v214(x0,bitIndex6) v216(x0,bitIndex6) v204(x0,bitIndex2) v206(x0,bitIndex2) v208(x0,bitIndex2) v143(x0) v145(x0) v147(x0) v149(x0) v151(x0) v153(x0) v155(x0) v157(x0,bitIndex1) v157(x0,bitIndex0) b11(bitIndex1) b11(bitIndex0) v107(x0) v109(x0) v111(x0) v113(x0) v115(x0) v117(x0) v119(x0) v121(x0,bitIndex1) v93(x0) v46(x0) v64(x0) v65(x0) v56(x0) v48(x0,bitIndex8) v58(x0) v60(x0) v62(x0) v50(x0,bitIndex8) v52(x0,bitIndex8) v54(x0,bitIndex8)
% 22.25/5.01
% 22.25/5.01 === Starting SPASS-SCL-FOL A Little Less Naive, considering 2580 atoms initially, heuristics mode: normal ===
% 22.25/5.01
% 22.25/5.01 === Backtracking. Learning clause 5099:2:1:[430.2,436.2,434.2,466.2,467.2,463.2]:Top: v899(x0),v888(x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5100:2:1:[430.2,436.2,434.2,467.2,466.2]:Top: v899(x0),v889(x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5101:3:1:[427.1,425.2]:Top: v898(x0) -> v890(x0),v37(x0,bitIndex2)
% 22.25/5.01 === Backtracking. Learning clause 5102:2:1:[622.3,619.1,623.1,618.1,616.1,5091.2,604.2,558.2,523.2]:Top: v851(x0),v842(x0,bitIndex22) ->
% 22.25/5.01 === Backtracking. Learning clause 5104:1:1:[5093.0,5103.0,771.1,772.1,768.1]:Top: -> v808(x0)
% 22.25/5.01 === Backtracking. Learning clause 5105:3:1:[4492.1,4496.2,4489.1,4494.2,4754.3,4755.1,4121.1,4124.1,4227.2]:Top: v167(x0) -> v165(x0),v415(x0)
% 22.25/5.01 === Backtracking. Learning clause 5106:2:1:[4492.2,4489.1,4496.2,4493.2]:Top: v365(x0) -> v165(x0)
% 22.25/5.01 === Backtracking. Learning clause 5107:3:1:[4705.1,4703.1,4707.1,4710.1,4696.1,4715.1,4718.1,4622.1,4699.2,4700.1,4623.1,4510.1,4509.1,4506.1,4507.1,4754.2]:Top: v284(x0) -> v294(x0),v283(x0)
% 22.25/5.01 === Backtracking. Learning clause 5108:2:1:[1222.1,1223.1,1218.1]:Top: v691(x0) -> v95(x0)
% 22.25/5.01 === Backtracking. Learning clause 5109:2:1:[160.1,164.1,155.1,201.2,158.2,200.2]:Top: v959(x0) -> v974(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5110:4:0:TAUT:: =(bitIndex67,constB8),=(bitIndex98,constB8),v553(constB8,bitIndex67) -> v553(constB8,bitIndex98)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5112:2:1:[4492.0,5111.2,4491.1,4487.1]:Top: -> v365(x0),ren539(x0)
% 22.25/5.01 === Backtracking. Learning clause 5113:2:1:[631.2,626.1,630.2,627.1,5102.1]:Top: v853(x0),v842(x0,bitIndex22) ->
% 22.25/5.01 === Backtracking. Learning clause 5114:4:1:[211.2,216.3,214.2,243.2,301.2,230.2,300.2,297.3]:Top: ren16(x0),v930(x0) -> v27(x0),v931(x0)
% 22.25/5.01 === Backtracking. Learning clause 5115:3:2:[2153.1,2171.1]:TopTop: -> v501(x0,bitIndex736),v501(x1,bitIndex736),ren227(x0,x1)
% 22.25/5.01 === Backtracking. Learning clause 5116:1:1:[2152.2,2170.1,5115.1]:Top: -> ren227(x0,x0)
% 22.25/5.01 === Backtracking. Learning clause 5117:1:1:[4493.1,5112.1,4496.1,4492.1]:Top: -> ren539(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5118:4:0:TAUT:: =(bitIndex20,constB8),=(bitIndex73,constB8),v582(constB8,bitIndex73) -> v582(constB8,bitIndex20)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5119:3:0:TAUT:: =(bitIndex46,constB8),v582(constB8,constB8) -> v582(constB8,bitIndex46)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5120:2:1:[4483.1,4198.2,4485.1]:Top: v418(x0,bitIndex0) -> v165(x0)
% 22.25/5.01 === Backtracking. Learning clause 5121:2:1:[646.2,647.1,643.1,642.1,638.1,639.1,634.1,635.1,5113.1,524.2,531.2]:Top: v849(x0,bitIndex0),v842(x0,bitIndex26) ->
% 22.25/5.01 === Backtracking. Learning clause 5122:2:1:[647.1,646.2,642.1,643.1,638.1,639.1,634.1,635.1]:Top: v849(x0,bitIndex0) -> v853(x0)
% 22.25/5.01 === Backtracking. Learning clause 5123:2:1:[631.2,626.1,630.2,627.1,603.1]:Top: v853(x0),v865(x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5124:2:1:[213.1,209.1,215.2,219.2,242.1,214.1]:Top: -> v954(x0),ren15(x0)
% 22.25/5.01 === Backtracking. Learning clause 5126:2:1:[230.0,5125.1,233.3,239.1,237.2,238.1,220.3,224.2,711.2,787.2,219.1,215.1]:Top: v951(x0) -> v954(x0)
% 22.25/5.01 === Backtracking. Learning clause 5127:2:1:[1129.2,1124.1,1128.2,1125.1,1122.1,5095.2,1110.2,1064.2,1036.2]:Top: v717(x0),v707(x0,bitIndex29) ->
% 22.25/5.01 === Backtracking. Learning clause 5128:2:1:[4408.2,4403.1,4410.1,4449.1,4446.1,4406.2,4450.1,4445.1,4441.1,4438.1,4442.1,4437.1,4435.1,5098.2,4423.2,4399.2,4334.2]:Top: v375(x0,bitIndex5) -> v395(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5129:3:0:TAUT:: =(bitIndex13,constB8),v375(constB8,constB8) -> v375(constB8,bitIndex13)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5131:3:0:[3941.0,5130.3]:: =(bitIndex8,constB8),=(bitIndex2,constB8),v518(constB8,bitIndex2) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5132:2:1:[4063.2,4091.1,4061.2,3897.2]:Top: v525(x0,bitIndex0) -> v454(x0)
% 22.25/5.01 === Backtracking. Learning clause 5133:3:1:[4720.2,4721.1,4621.2,4717.1,4716.1,4712.1,4713.1,4508.2,4709.1,4708.1,4706.1,4702.2]:Top: v359(x0),v295(x0) -> v169(x0,bitIndex3)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5134:4:0:TAUT:: =(bitIndex83,constB8),=(bitIndex74,constB8),v553(constB8,bitIndex83) -> v553(constB8,bitIndex74)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5135:2:1:[238.2,236.1,237.1]:Top: -> v953(x0),ren19(x0)
% 22.25/5.01 === Backtracking. Learning clause 5136:2:1:[801.1,798.2]:Top: v75(x0,bitIndex3),v71(x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5137:2:1:[453.3,310.2,451.2,463.1,467.1,312.2,308.2,796.2]:Top: v885(x0) -> v802(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5139:2:0:[2.0,5138.1]:: =(constB7,constB8) -> nextState(constB8,constB8)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5140:3:0:TAUT:: =(bitIndex1,constB8),v404(constB8,constB8) -> v404(constB8,bitIndex1)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5141:3:0:TAUT:: =(bitIndex4,constB8),v714(constB8,bitIndex4) -> v714(constB8,constB8)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5142:3:1:[225.1,229.2,5088.1,218.2]:Top: -> v806(x0),v951(x0),ren16(x0)
% 22.25/5.01 === Backtracking. Learning clause 5143:5:1:[1246.2,1251.2,1249.2,1254.3,1258.2,1264.3,4103.3,4109.1,4112.1,4767.1]:Top: v681(x0),v280(x0),v449(x0),v97(x0,bitIndex1) -> v95(x0)
% 22.25/5.01 === Backtracking. Learning clause 5144:1:2:[318.1,319.1]:TopTop: -> ren30(x0,x1,x0)
% 22.25/5.01 === Backtracking. Learning clause 5145:2:1:[1260.1,1259.1,1264.2,1258.1]:Top: v452(x0) -> v678(x0)
% 22.25/5.01 === Backtracking. Learning clause 5146:2:2:[4458.2,4967.1,4968.1,4969.1,4955.1]:TopTop: range_2_0(x0) -> ren574(x1,x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5147:3:0:TAUT:: =(bitIndex0,constB8),v37(constB8,bitIndex0) -> v37(constB8,constB8)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5149:2:1:[314.1,5148.2,414.3,313.2]:Top: v907(x0),v35(x0) ->
% 22.25/5.01 === CC is in false state. New clause to be learned: 5152:2:0:[4800.0,5150.2,4798.0,5151.3]:: =(bitIndex0,constB8),=(bitIndex2,constB8) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5153:1:0:[343.1,2.1]:: -> ren34(constB8)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5156:2:0:[4251.0,5154.2,4252.0,5155.3]:: =(bitIndex1,constB8),=(bitIndex2,constB8) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5157:1:2:[4513.1,4514.1]:TopTop: -> ren540(x0,x1,x0)
% 22.25/5.01 === Backtracking. Learning clause 5158:2:1:[1389.2,1392.1,1386.2,1383.3,1404.1,1396.1,1413.1,1418.1,1423.1,1429.1,1432.2,1330.2,1326.2,1407.1,1323.2,1411.1,1422.1,1324.2,1320.2]:Top: v612(x0),v656(x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5159:2:1:[595.2,598.2,600.2,623.1,618.1,616.1,5091.2,604.2,558.2,602.1,5102.1,524.2,519.2]:Top: v842(x0,bitIndex20) -> v863(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5160:3:0:TAUT:: =(bitIndex0,constB8),v97(constB8,bitIndex0) -> v97(constB8,constB8)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5161:2:1:[622.3,619.1,623.1,618.1]:Top: v851(x0) -> v848(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5163:2:0:[795.0,5162.1]:: =(constB0,constB8) -> v29(constB8,bitIndex0)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5164:2:1:[589.1,591.1]:Top: -> v868(x0),v853(x0)
% 22.25/5.01 === Backtracking. Learning clause 5165:1:1:[35.2,36.2]:Top: ren2(x0,x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5166:2:1:[609.2,606.2,5090.1,559.1]:Top: v846(x0) -> v843(x0,bitIndex5)
% 22.25/5.01 === Backtracking. Learning clause 5167:2:1:[4441.3,4438.1,4442.1,4437.1,4435.1,5098.2]:Top: v385(x0),v379(x0) ->
% 22.25/5.01 === Backtracking. Learning clause 5168:1:2:[90.1,91.1]:TopTop: -> ren4(x0,x1,x0)
% 22.25/5.01 === Backtracking. Learning clause 5169:2:1:[4712.2,4713.1,4709.1,4708.1]:Top: v299(x0) -> v297(x0)
% 22.25/5.01 === Backtracking. Learning clause 5170:1:2:[4130.1,4129.1]:TopTop: -> ren521(x0,x1,x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5171:4:0:TAUT:: =(bitIndex69,constB8),=(bitIndex62,constB8),v553(constB8,bitIndex69) -> v553(constB8,bitIndex62)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5172:2:1:[4109.3,4767.1,4112.1]:Top: v450(x0),v97(x0,bitIndex1) ->
% 22.25/5.01 === Backtracking. Learning clause 5173:5:1:[3582.1,3593.2,3578.1,3575.1,3596.3,3600.2,3560.1,3562.2,3571.2,3568.1,3565.1]:Top: v574(x0),v576(x0) -> v571(x0,bitIndex0),v560(x0),v578(x0,bitIndex0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5174:3:0:TAUT:: =(bitIndex15,constB8),v594(constB8,bitIndex15) -> v594(constB8,constB8)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5175:3:0:TAUT:: =(bitIndex1,constB8),v97(constB8,constB8) -> v97(constB8,bitIndex1)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5176:1:0:TAUT:: -> =(constB8,constB8)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5177:3:1:[3586.1,3590.2,3588.2,3597.2,3596.2,3600.2,3571.2]:Top: v578(x0,bitIndex1) -> v572(x0),v570(x0)
% 22.25/5.01 === Backtracking. Learning clause 5178:3:1:[3603.1,3605.2,3606.1]:Top: v123(x0) -> v568(x0),v105(x0)
% 22.25/5.01 === Backtracking. Learning clause 5179:3:0:[1270.3,5160.3,1342.2]:: v99(constB8),v97(constB8,bitIndex0),=(bitIndex0,constB8) ->
% 22.25/5.01 === Backtracking. Learning clause 5180:6:2:[4966.5,3888.1,3891.1,3890.1,3889.1,3892.1,3883.2]:TopTop: range_7_0(x0),v514(x1) -> =(bitIndex0,x0),=(bitIndex1,x0),=(bitIndex2,x0),ren503(x1,x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5181:3:0:TAUT:: =(bitIndex3,constB8),v169(constB8,constB8) -> v169(constB8,bitIndex3)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5183:3:0:[649.0,5182.3]:: =(bitIndex3,constB8),=(bitIndex5,constB8),v849(constB8,bitIndex3) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5184:1:1:[1206.1,1205.1]:Top: -> ren82(x0,x0)
% 22.25/5.01 === Backtracking. Learning clause 5185:2:1:[5028.1,5048.2,4149.1]:Top: v93(x0),v434(x0) ->
% 22.25/5.01 === CC is in false state. New clause to be learned: 5188:2:0:[973.0,5186.2,972.0,5187.3]:: =(bitIndex3,constB8),=(bitIndex4,constB8) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5189:3:1:[3544.2,3478.1,5178.2]:Top: v123(x0) -> ren412(x0),v105(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5190:3:0:TAUT:: =(bitIndex2,constB8),v134(constB8,constB8) -> v134(constB8,bitIndex2)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5191:3:1:[1416.2,1373.2,1415.2]:Top: v616(x0) -> v641(x0),v614(x0)
% 22.25/5.01 === CC is in false state. New clause to be learned: 5192:3:0:TAUT:: =(bitIndex0,constB8),v37(constB8,constB8) -> v37(constB8,bitIndex0)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5195:2:0:[4536.0,5193.2,4538.0,5194.3]:: =(bitIndex3,constB8),=(bitIndex1,constB8) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === CC is in false state. New clause to be learned: 5198:2:0:[4536.0,5196.2,4539.0,5197.3]:: =(bitIndex3,constB8),=(bitIndex0,constB8) ->
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5199:2:1:[4783.1,4778.2,4779.1,4776.2,4774.2,4784.1,4807.1,4772.2,4819.2,4976.2,4978.2,4728.2,4980.2]:Top: v291(x0,bitIndex1),v188(x0) ->
% 22.25/5.01 === CC is in false state. New clause to be learned: 5200:4:0:TAUT:: =(bitIndex6,constB8),=(bitIndex5,constB8),v495(constB8,bitIndex6) -> v495(constB8,bitIndex5)
% 22.25/5.01 === Restarting.
% 22.25/5.01 === Backtracking. Learning clause 5201:1:1:[53.2,55.1,49.1,46.1,5084.1,58.1,43.2,5086.1]:Top: -> v4(x0)
% 22.25/5.01 === Conflict found: 5201:1:1:[53.2,55.1,49.1,46.1,5084.1,58.1,43.2,5086.1]:Top: -> v4(x0) {x0 -> skc1}
% 22.25/5.01
% 22.25/5.01 SZS status Unsatisfiable
% 22.25/5.01
% 22.25/5.01 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.25/5.01
% 22.25/5.01 SPASS-SCL-FOL Statistics:
% 22.25/5.01 Number of learned clauses: 59
% 22.25/5.01 Number of propagations: 36067
% 22.25/5.01 Number of decisions: 3544
% 22.25/5.01 Number of resolutions: 282
% 22.25/5.01 Number of condensations: 0
% 22.25/5.01 Number of sub resolutions: 33
% 22.25/5.01 Number of input literals (deduplicated): 2580
% 22.25/5.01 Number of grows: 0
% 22.25/5.01 Number of considered ground atoms: 2580
% 22.25/5.01
% 22.25/5.01 Needed: 0:00:04.43
% 22.25/5.01
%------------------------------------------------------------------------------