Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-2.opb |
MD5SUM | 409f1cf0658f035df65cb61f3e4f598e |
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 | 27847 |
Number of constraints which are clauses | 27847 |
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 wulflinc1 THE 2005-05-25 17:10:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21902 boxname=wulflinc1 idbench=320 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 409f1cf0658f035df65cb61f3e4f598e /oldhome/oroussel/tmp/wulflinc1/normalized-frb35-17-2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-frb35-17-2.opb IDLAUNCH: 21902 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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: 612008 kB Buffers: 35472 kB Cached: 357468 kB SwapCached: 3976 kB Active: 79788 kB Inactive: 320116 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 611756 kB SwapTotal: 2097136 kB SwapFree: 2092844 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6968 kB Slab: 16952 kB Committed_AS: 92712 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:31:18 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 21902 7 1229.85 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 27847 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 | 27847 55694 | 9282 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -24[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56112 122082 | 18704 0 0 nan | 0.000 % | c | 100 | 55441 120669 | 20574 62 485 7.8 | 1.950 % | c | 252 | 54383 118381 | 22631 186 1801 9.7 | 5.130 % | c | 477 | 53349 116119 | 24895 313 3077 9.8 | 8.306 % | c | 814 | 51759 112535 | 27384 516 5065 9.8 | 13.461 % | c | 1321 | 49950 108452 | 30122 920 9543 10.4 | 19.341 % | 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 | 1658 | 48453 105089 | 16151 1166 13758 11.8 | 19.341 % | c | 1758 | 48207 104544 | 17766 1257 15573 12.4 | 25.098 % | c | 1908 | 47653 103297 | 19542 1386 16993 12.3 | 26.885 % | c | 2133 | 47022 101840 | 21496 1582 20176 12.8 | 29.018 % | c | 2471 | 45334 97977 | 23646 1783 22714 12.7 | 34.745 % | c | 2977 | 43116 92786 | 26011 2128 28051 13.2 | 41.789 % | 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 | 3108 | 42804 92166 | 14268 2242 29536 13.2 | 41.789 % | c | 3208 | 42633 91773 | 15694 2311 32120 13.9 | 43.581 % | c | 3358 | 42086 90483 | 17264 2410 34663 14.4 | 45.442 % | c | 3583 | 41186 88373 | 18990 2527 36936 14.6 | 48.512 % | c | 3920 | 39875 85257 | 20889 2675 39865 14.9 | 53.073 % | c | 4427 | 38250 81393 | 22978 2937 45919 15.6 | 58.815 % | c | 5186 | 37415 79400 | 25276 3573 58638 16.4 | 61.715 % | 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 | 5777 | 36536 77244 | 12178 3923 69803 17.8 | 61.715 % | c | 5877 | 36375 76873 | 13395 4009 70834 17.7 | 65.308 % | c | 6027 | 36111 76265 | 14735 4119 72852 17.7 | 66.182 % | c | 6252 | 35833 75598 | 16208 4304 78604 18.3 | 67.328 % | c | 6590 | 35525 74869 | 17829 4581 87877 19.2 | 68.259 % | c | 7096 | 35132 73939 | 19612 5015 102250 20.4 | 69.626 % | c | 7855 | 35004 73641 | 21574 5721 119858 21.0 | 70.063 % | c | 8994 | 34621 72729 | 23731 6710 156327 23.3 | 71.405 % | c | 10702 | 34449 72319 | 26104 8303 266846 32.1 | 72.007 % | 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 | 10930 | 34398 72230 | 11466 8491 276955 32.6 | 72.007 % | c | 11030 | 34307 72002 | 12612 8543 279040 32.7 | 72.564 % | c | 11180 | 34307 72002 | 13873 8693 286044 32.9 | 72.564 % | c | 11405 | 34227 71812 | 15261 8862 292699 33.0 | 72.846 % | c | 11743 | 33985 71231 | 16787 9032 296460 32.8 | 73.704 % | c | 12250 | 33985 71231 | 18466 9539 330834 34.7 | 73.704 % | c | 13010 | 33963 71183 | 20312 10270 353365 34.4 | 73.770 % | c | 14149 | 33552 70232 | 22343 11249 423515 37.6 | 75.141 % | c | 15857 | 33222 69433 | 24578 12762 568784 44.6 | 76.291 % | c | 18419 | 33120 69188 | 27036 15273 761555 49.9 | 76.651 % | c | 22263 | 32930 68727 | 29739 18985 1120606 59.0 | 77.344 % | 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 | 26467 | 32657 68028 | 10885 22867 1465252 64.1 | 77.344 % | c | 26567 | 32647 68006 | 11973 22966 1468382 63.9 | 78.332 % | c | 26717 | 32647 68006 | 13170 23116 1476425 63.9 | 78.332 % | c | 26942 | 32647 68006 | 14487 23341 1495373 64.1 | 78.332 % | c | 27279 | 32477 67592 | 15936 23347 1512616 64.8 | 78.938 % | c | 27785 | 32364 67313 | 17530 23764 1543363 64.9 | 79.364 % | c | 28544 | 32254 67045 | 19283 24353 1597203 65.6 | 79.764 % | c | 29683 | 32254 67045 | 21211 25492 1710400 67.1 | 79.764 % | c | 31391 | 32254 67045 | 23332 27200 1919412 70.6 | 79.764 % | c | 33955 | 32254 67045 | 25666 29764 2101826 70.6 | 79.764 % | 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 | 35137 | 31980 66414 | 10660 30812 2169138 70.4 | 79.764 % | c | 35238 | 31946 66328 | 11726 15491 930133 60.0 | 80.939 % | c | 35389 | 31915 66258 | 12898 15639 935925 59.8 | 81.041 % | c | 35614 | 31915 66258 | 14188 15864 948886 59.8 | 81.041 % | c | 35951 | 31915 66258 | 15607 16201 965361 59.6 | 81.041 % | c | 36458 | 31915 66258 | 17168 16708 996138 59.6 | 81.041 % | c | 37217 | 31915 66258 | 18884 17467 1044393 59.8 | 81.041 % | c | 38357 | 31910 66247 | 20773 18600 1113004 59.8 | 81.056 % | c | 40065 | 31845 66095 | 22850 20288 1216954 60.0 | 81.276 % | c | 42627 | 31804 65994 | 25135 22834 1375865 60.3 | 81.429 % | c | 46471 | 31804 65994 | 27649 26678 1735048 65.0 | 81.429 % | c | 52237 | 31510 65286 | 30414 32374 2209723 68.3 | 82.477 % | c | 60886 | 31481 65217 | 33455 40961 2771939 67.7 | 82.579 % | c | 73860 | 31477 65205 | 36801 19710 946500 48.0 | 82.600 % | c | 93322 | 31477 65205 | 40481 39172 2462580 62.9 | 82.600 % | 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 | 98887 | 31443 65100 | 10481 44676 2833202 63.4 | 82.600 % | c | 98987 | 31443 65100 | 11529 17731 914127 51.6 | 82.724 % | c | 99137 | 31443 65100 | 12682 17881 921601 51.5 | 82.724 % | c | 99362 | 31405 65004 | 13950 18104 938348 51.8 | 82.867 % | c | 99699 | 31381 64946 | 15345 18412 962309 52.3 | 82.954 % | c | 100205 | 31381 64946 | 16879 18918 1006461 53.2 | 82.954 % | c | 100964 | 31370 64919 | 18567 19674 1054745 53.6 | 82.995 % | c | 102103 | 31370 64919 | 20424 20813 1143158 54.9 | 82.995 % | c | 103813 | 31365 64908 | 22466 22519 1262523 56.1 | 83.011 % | c | 106376 | 31365 64908 | 24713 25082 1418165 56.5 | 83.011 % | c | 110222 | 31365 64908 | 27185 28928 1703939 58.9 | 83.011 % | c | 115988 | 31330 64825 | 29903 34689 2037716 58.7 | 83.133 % | c | 124637 | 31284 64708 | 32893 43252 2666638 61.7 | 83.307 % | c | 137612 | 31239 64605 | 36183 22486 988221 43.9 | 83.450 % | c | 157073 | 31239 64605 | 39801 41947 2056155 49.0 | 83.450 % | c | 186265 | 31236 64598 | 43781 31773 1941768 61.1 | 83.460 % | c | 230054 | 31231 64587 | 48159 32261 2906002 90.1 | 83.476 % | 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 | 278557 | 31244 64621 | 10414 32296 2237077 69.3 | 83.476 % | c | 278658 | 31244 64621 | 11455 16249 954352 58.7 | 83.452 % | c | 278809 | 31244 64621 | 12600 16400 966097 58.9 | 83.452 % | c | 279034 | 31244 64621 | 13861 16625 981948 59.1 | 83.452 % | c | 279372 | 31244 64621 | 15247 16963 1000566 59.0 | 83.452 % | c | 279878 | 31244 64621 | 16771 17469 1034794 59.2 | 83.452 % | c | 280638 | 31244 64621 | 18449 18229 1067205 58.5 | 83.452 % | c | 281777 | 31244 64621 | 20293 19368 1125638 58.1 | 83.452 % | c | 283486 | 31244 64621 | 22323 21077 1208886 57.4 | 83.452 % | c | 286048 | 31244 64621 | 24555 23639 1365631 57.8 | 83.452 % | c | 289893 | 31244 64621 | 27011 27484 1608741 58.5 | 83.452 % | c | 295659 | 31207 64527 | 29712 33206 1964370 59.2 | 83.595 % | c | 304308 | 31207 64527 | 32683 41855 2460979 58.8 | 83.595 % | c | 317282 | 31197 64503 | 35951 22333 712494 31.9 | 83.630 % | c | 336743 | 31197 64503 | 39547 41794 1397205 33.4 | 83.630 % | c | 365935 | 31193 64493 | 43501 34344 952519 27.7 | 83.646 % | c | 409725 | 31143 64373 | 47852 34709 1222470 35.2 | 83.824 % | c | 475409 | 31136 64358 | 52637 54302 1647686 30.3 | 83.845 % | c | 573935 | 31106 64290 | 57900 50437 1608080 31.9 | 83.942 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 24416 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.94 0.95 2/55 24412 Raw data (stat): 24412 (runsolver) R 24411 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 725497120 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.93 0.94 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0004 s] Raw data (loadavg): 0.94 0.94 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0011 s] Raw data (loadavg): 0.95 0.94 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0009 s] Raw data (loadavg): 0.95 0.94 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0017 s] Raw data (loadavg): 0.96 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0016 s] Raw data (loadavg): 0.97 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0013 s] Raw data (loadavg): 0.97 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0021 s] Raw data (loadavg): 0.97 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0019 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.96 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.95 2/56 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.68 s] Raw data (loadavg): 0.99 0.97 0.95 1/54 24416 Raw data (stat): 24412 (minisat+_script) S 24411 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725497120 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.68 CPU time (s): 1229.85 CPU user time (s): 1229.48 CPU system time (s): 0.370943 CPU usage (%): 100.014 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####