Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-1.opb |
MD5SUM | 16a8eb66aae2bcfd534a482dd0a3948e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 27856 |
Number of constraints which are clauses | 27856 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc15 THE 2005-05-25 17:08:00 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21901 boxname=wulflinc15 idbench=319 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 16a8eb66aae2bcfd534a482dd0a3948e /oldhome/oroussel/tmp/wulflinc15/normalized-frb35-17-1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-frb35-17-1.opb IDLAUNCH: 21901 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 622528 kB Buffers: 35104 kB Cached: 355360 kB SwapCached: 672 kB Active: 74016 kB Inactive: 318592 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 622276 kB SwapTotal: 2097136 kB SwapFree: 2095624 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5080 kB Slab: 13912 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:28:30 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 21901 7 1229.84 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 27856 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 27856 55712 | 9285 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -25[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56151 122167 | 18717 0 0 nan | 0.000 % | c | 100 | 55641 121103 | 20588 80 1297 16.2 | 1.436 % | c | 250 | 54951 119605 | 22647 189 2268 12.0 | 3.524 % | c | 476 | 54022 117586 | 24912 364 4235 11.6 | 6.330 % | c | 813 | 52202 113569 | 27403 615 7046 11.5 | 11.983 % | c | 1319 | 50454 109647 | 30143 1040 11817 11.4 | 17.600 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1402 | 50068 108787 | 16689 1107 12820 11.6 | 17.600 % | c | 1502 | 49454 107371 | 18357 1174 13840 11.8 | 21.069 % | c | 1652 | 48818 105945 | 20193 1300 15532 11.9 | 22.940 % | c | 1877 | 48058 104211 | 22213 1452 17303 11.9 | 25.446 % | c | 2214 | 47050 101919 | 24434 1732 20313 11.7 | 28.742 % | c | 2720 | 45617 98616 | 26877 2151 25789 12.0 | 33.547 % | c | 3479 | 43899 94657 | 29565 2788 35155 12.6 | 39.272 % | c | 4618 | 40020 85547 | 32522 3583 49056 13.7 | 52.286 % | c ============================================================================== c [1mFound solution: -27[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4643 | 40055 85703 | 13351 3591 49288 13.7 | 52.286 % | c | 4745 | 39723 84935 | 14686 3575 49232 13.8 | 53.493 % | c | 4895 | 39621 84699 | 16154 3698 51856 14.0 | 53.838 % | c | 5120 | 39179 83659 | 17770 3874 56863 14.7 | 55.355 % | c | 5457 | 37944 80743 | 19547 4038 60606 15.0 | 59.650 % | c | 5963 | 37234 79072 | 21501 4463 73988 16.6 | 62.099 % | c ============================================================================== c [1mFound solution: -28[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6315 | 37042 78587 | 12347 4760 82824 17.4 | 62.099 % | c | 6415 | 36898 78246 | 13581 4847 84510 17.4 | 63.317 % | c | 6566 | 36429 77135 | 14939 4926 88695 18.0 | 64.927 % | c | 6791 | 36313 76855 | 16433 5126 95703 18.7 | 65.343 % | c | 7128 | 35730 75480 | 18077 5353 100982 18.9 | 67.308 % | c | 7634 | 35222 74253 | 19884 5765 125403 21.8 | 69.093 % | c | 8393 | 34627 72820 | 21873 6399 144024 22.5 | 71.186 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9306 | 34209 71811 | 11403 7189 178763 24.9 | 71.186 % | c | 9407 | 34209 71811 | 12543 7290 180868 24.8 | 72.783 % | c | 9557 | 34129 71619 | 13797 7379 182136 24.7 | 73.065 % | c | 9783 | 34089 71525 | 15177 7572 191361 25.3 | 73.204 % | c | 10120 | 34089 71525 | 16695 7909 209404 26.5 | 73.204 % | c | 10626 | 34043 71415 | 18364 8361 232830 27.8 | 73.363 % | c | 11385 | 33962 71214 | 20201 9085 269116 29.6 | 73.666 % | c | 12525 | 33255 69528 | 22221 9902 298057 30.1 | 76.137 % | c | 14233 | 32889 68642 | 24443 11283 385731 34.2 | 77.457 % | c | 16795 | 32768 68345 | 26887 13632 659300 48.4 | 77.888 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17157 | 32647 68009 | 10882 13954 681985 48.9 | 77.888 % | c | 17258 | 32641 67993 | 11970 14049 684582 48.7 | 78.347 % | c | 17408 | 32641 67993 | 13167 14199 690091 48.6 | 78.347 % | c | 17634 | 32588 67867 | 14483 14349 701963 48.9 | 78.532 % | c | 17971 | 32555 67786 | 15932 14650 714775 48.8 | 78.655 % | c | 18477 | 32411 67425 | 17525 15034 729230 48.5 | 79.195 % | c | 19237 | 32367 67321 | 19278 15759 758129 48.1 | 79.349 % | c | 20376 | 32301 67168 | 21205 16840 848616 50.4 | 79.544 % | c | 22085 | 32218 66973 | 23326 18501 944250 51.0 | 79.832 % | c | 24647 | 32151 66816 | 25659 21011 1154613 55.0 | 80.063 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27056 | 32115 66734 | 10705 23335 1321535 56.6 | 80.063 % | c | 27157 | 32113 66730 | 11775 23435 1326791 56.6 | 80.316 % | c | 27308 | 32113 66730 | 12953 23586 1331776 56.5 | 80.316 % | c | 27533 | 32071 66627 | 14248 23711 1346197 56.8 | 80.470 % | c | 27871 | 32034 66544 | 15673 23983 1360153 56.7 | 80.587 % | c | 28377 | 31959 66360 | 17240 24473 1380446 56.4 | 80.868 % | c | 29136 | 31866 66137 | 18964 25210 1423417 56.5 | 81.191 % | c | 30275 | 31832 66053 | 20861 26274 1496718 57.0 | 81.313 % | c | 31983 | 31832 66053 | 22947 27982 1622123 58.0 | 81.313 % | c | 34545 | 31805 65984 | 25241 30493 1805024 59.2 | 81.416 % | c | 38389 | 31766 65891 | 27766 34166 2010912 58.9 | 81.554 % | c | 44157 | 31719 65774 | 30542 39804 2430835 61.1 | 81.733 % | c | 52806 | 31615 65520 | 33596 18059 877920 48.6 | 82.106 % | c ============================================================================== c [1mFound solution: -32[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 62973 | 31532 65307 | 10510 28208 1448576 51.4 | 82.106 % | c | 63076 | 31532 65307 | 11561 14207 578195 40.7 | 82.410 % | c | 63226 | 31532 65307 | 12717 14357 585145 40.8 | 82.410 % | c | 63451 | 31532 65307 | 13988 14582 598581 41.0 | 82.410 % | c | 63788 | 31532 65307 | 15387 14919 620951 41.6 | 82.410 % | c | 64294 | 31532 65307 | 16926 15425 653206 42.3 | 82.410 % | c | 65053 | 31464 65147 | 18619 16165 701648 43.4 | 82.634 % | c | 66192 | 31419 65036 | 20481 17286 776803 44.9 | 82.803 % | c | 67901 | 31419 65036 | 22529 18995 879887 46.3 | 82.803 % | c | 70463 | 31402 64997 | 24782 21553 994708 46.2 | 82.860 % | c | 74308 | 31402 64997 | 27260 25398 1201104 47.3 | 82.859 % | c | 80074 | 31402 64997 | 29986 31164 1386011 44.5 | 82.860 % | c | 88723 | 31378 64935 | 32984 39808 1664419 41.8 | 82.957 % | c | 101698 | 31329 64818 | 36283 20738 615428 29.7 | 83.131 % | c | 121159 | 31329 64818 | 39911 40199 1368273 34.0 | 83.131 % | c | 150352 | 31266 64657 | 43902 30887 952875 30.9 | 83.376 % | c | 194141 | 31229 64565 | 48293 31138 1004370 32.3 | 83.514 % | c ============================================================================== c [1mFound solution: -33[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 217392 | 31241 64598 | 10413 54386 1860959 34.2 | 83.514 % | c | 217494 | 31241 64598 | 11454 17566 456371 26.0 | 83.495 % | c | 217644 | 31241 64598 | 12599 17716 463136 26.1 | 83.495 % | c | 217869 | 31241 64598 | 13859 17941 471453 26.3 | 83.495 % | c | 218206 | 31241 64598 | 15245 18278 487008 26.6 | 83.495 % | c | 218712 | 31241 64598 | 16770 18784 502493 26.8 | 83.495 % | c | 219471 | 31241 64598 | 18447 19543 525927 26.9 | 83.495 % | c | 220610 | 31241 64598 | 20291 20682 558029 27.0 | 83.495 % | c | 222318 | 31241 64598 | 22321 22390 603953 27.0 | 83.495 % | c | 224880 | 31241 64598 | 24553 24952 673524 27.0 | 83.495 % | c | 228724 | 31227 64566 | 27008 28790 773486 26.9 | 83.541 % | c | 234490 | 31207 64514 | 29709 34403 940104 27.3 | 83.623 % | c | 243140 | 31207 64514 | 32680 43053 1183495 27.5 | 83.623 % | c | 256114 | 31207 64514 | 35948 24367 575570 23.6 | 83.623 % | c | 275576 | 31168 64425 | 39543 43805 1874953 42.8 | 83.750 % | c | 304768 | 31161 64408 | 43497 33136 1335594 40.3 | 83.776 % | c | 348558 | 31153 64388 | 47847 36328 955951 26.3 | 83.807 % | c | 414243 | 31122 64317 | 52632 58263 1623043 27.9 | 83.904 % | c | 512769 | 31083 64216 | 57895 59889 2165270 36.2 | 84.047 % | c ============================================================================== c [1mFound solution: -34[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 614887 | 31011 64017 | 10337 52804 1656316 31.4 | 84.047 % | c | 614988 | 31011 64017 | 11370 21171 575638 27.2 | 84.304 % | c | 615139 | 31011 64017 | 12507 21322 578882 27.1 | 84.304 % | c | 615365 | 31011 64017 | 13758 21548 583379 27.1 | 84.304 % | c | 615703 | 31011 64017 | 15134 21886 590624 27.0 | 84.304 % | c | 616209 | 31011 64017 | 16647 22392 603214 26.9 | 84.304 % | c | 616969 | 31011 64017 | 18312 23152 624588 27.0 | 84.304 % | c | 618110 | 31011 64017 | 20143 24293 653811 26.9 | 84.304 % | c | 619819 | 31011 64017 | 22158 26002 714382 27.5 | 84.304 % | c | 622381 | 30983 63957 | 24374 28562 777468 27.2 | 84.385 % | c | 626226 | 30983 63957 | 26811 32407 890463 27.5 | 84.385 % | c | 631992 | 30983 63957 | 29492 38173 1062628 27.8 | 84.385 % | c | 640641 | 30838 63649 | 32441 21452 580040 27.0 | 84.513 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 10835 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.93 0.93 2/54 10831 Raw data (stat): 10831 (runsolver) R 10830 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782330611 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.93 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0016 s] Raw data (loadavg): 0.94 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0024 s] Raw data (loadavg): 0.95 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0027 s] Raw data (loadavg): 0.95 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0041 s] Raw data (loadavg): 0.96 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0048 s] Raw data (loadavg): 0.97 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0052 s] Raw data (loadavg): 0.97 0.94 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.005 s] Raw data (loadavg): 0.97 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0049 s] Raw data (loadavg): 0.98 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.005 s] Raw data (loadavg): 0.98 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 0.98 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.006 s] Raw data (loadavg): 0.99 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.006 s] Raw data (loadavg): 0.99 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.006 s] Raw data (loadavg): 0.99 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.006 s] Raw data (loadavg): 0.99 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.007 s] Raw data (loadavg): 0.99 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.007 s] Raw data (loadavg): 0.99 0.95 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.007 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.007 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.007 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.008 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.009 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.009 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.01 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.009 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.01 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.01 s] Raw data (loadavg): 0.99 0.96 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.028 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.028 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.028 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.72 s] Raw data (loadavg): 0.99 0.97 0.93 1/53 10835 Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.72 CPU time (s): 1229.84 CPU user time (s): 1229.48 CPU system time (s): 0.368943 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####