Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-2.opb |
MD5SUM | 270e069f649d19b0da4e4d23c0e1ebfc |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -30 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 760 |
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 | 760 |
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 | 760 |
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.06 |
Number of variables | 760 |
Total number of constraints | 41263 |
Number of constraints which are clauses | 41263 |
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 wulflinc7 THE 2005-05-27 05:33:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23079 boxname=wulflinc7 idbench=325 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 270e069f649d19b0da4e4d23c0e1ebfc /oldhome/oroussel/tmp/wulflinc7/normalized-frb40-19-2.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-frb40-19-2.opb IDLAUNCH: 23079 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 451.050 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: 870912 kB Buffers: 33552 kB Cached: 109916 kB SwapCached: 692 kB Active: 50548 kB Inactive: 94980 kB HighTotal: 131008 kB HighFree: 59192 kB LowTotal: 903652 kB LowFree: 811720 kB SwapTotal: 2097136 kB SwapFree: 2095524 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5084 kB Slab: 12636 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 05:53:31 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 23079 7 1229.85 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 41263 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 | 41263 82526 | 13754 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost:35010 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 77411 167438 | 25803 0 0 nan | 0.000 % | c | 100 | 77197 167004 | 28383 85 1743 20.5 | 0.449 % | c | 250 | 76777 166128 | 31221 216 3076 14.2 | 1.370 % | c | 475 | 75681 163748 | 34343 367 7270 19.8 | 3.965 % | c | 812 | 74772 161767 | 37778 638 10625 16.7 | 6.213 % | c | 1318 | 72216 156098 | 41555 971 15210 15.7 | 12.362 % | 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 | 1358 | 71957 155524 | 23985 1000 15644 15.6 | 12.362 % | c | 1458 | 71484 154445 | 26383 1077 16216 15.1 | 14.235 % | c | 1609 | 70637 152550 | 29021 1185 17694 14.9 | 16.491 % | c | 1834 | 69903 150904 | 31924 1355 19103 14.1 | 18.302 % | c | 2171 | 68629 148052 | 35116 1633 21862 13.4 | 21.386 % | c | 2677 | 66555 143323 | 38628 2003 25849 12.9 | 26.681 % | c | 3436 | 63907 137250 | 42490 2573 35121 13.6 | 33.519 % | c | 4575 | 60641 129717 | 46739 3414 45806 13.4 | 42.032 % | c | 6284 | 58132 123765 | 51413 4758 70644 14.8 | 48.684 % | 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 | 6893 | 57499 122346 | 19166 5251 79403 15.1 | 48.684 % | c | 6993 | 57374 122059 | 21082 5340 80419 15.1 | 50.986 % | c | 7143 | 57174 121601 | 23190 5476 83135 15.2 | 51.497 % | c | 7368 | 57124 121493 | 25509 5691 90616 15.9 | 51.614 % | c | 7705 | 56450 119888 | 28060 5895 93895 15.9 | 53.460 % | c | 8211 | 55724 118204 | 30867 6317 101819 16.1 | 55.371 % | c | 8970 | 54430 115147 | 33953 6865 120056 17.5 | 58.891 % | c | 10109 | 53229 112295 | 37349 7784 156050 20.0 | 62.178 % | c | 11817 | 51998 109354 | 41084 9200 202992 22.1 | 65.558 % | c | 14379 | 50235 105114 | 45192 10981 295829 26.9 | 70.406 % | 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 | 15965 | 49478 103359 | 16492 12311 371372 30.2 | 70.406 % | c | 16066 | 49478 103359 | 18141 12412 374678 30.2 | 72.440 % | c | 16216 | 49424 103225 | 19955 12525 376566 30.1 | 72.597 % | c | 16441 | 49285 102876 | 21950 12651 381138 30.1 | 72.991 % | c | 16778 | 49212 102697 | 24145 12924 395334 30.6 | 73.204 % | c | 17285 | 49156 102561 | 26560 13400 438885 32.8 | 73.360 % | c | 18044 | 48324 100548 | 29216 13832 461348 33.4 | 75.707 % | c | 19183 | 48201 100261 | 32138 14905 550058 36.9 | 76.033 % | c | 20891 | 47874 99472 | 35352 16285 636889 39.1 | 76.957 % | c | 23453 | 47628 98870 | 38887 18649 839926 45.0 | 77.656 % | 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 | 25038 | 47524 98566 | 15841 20184 980752 48.6 | 77.656 % | c | 25139 | 47524 98566 | 17425 20285 983661 48.5 | 77.940 % | c | 25289 | 47524 98566 | 19167 20435 990976 48.5 | 77.939 % | c | 25514 | 47524 98566 | 21084 20660 1005617 48.7 | 77.939 % | c | 25851 | 47524 98566 | 23192 20997 1026282 48.9 | 77.939 % | c | 26358 | 47524 98566 | 25512 21504 1055909 49.1 | 77.940 % | c | 27118 | 47524 98566 | 28063 22264 1120991 50.3 | 77.939 % | c | 28258 | 47202 97772 | 30869 23237 1219781 52.5 | 78.852 % | c | 29966 | 47191 97747 | 33956 24941 1366171 54.8 | 78.880 % | c | 32528 | 47072 97453 | 37352 27423 1611937 58.8 | 79.221 % | c | 36372 | 47072 97453 | 41087 31267 2099445 67.1 | 79.221 % | c | 42138 | 46746 96661 | 45196 36763 2600401 70.7 | 80.142 % | c ============================================================================== c [1mFound solution: -35[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46022 | 46748 96684 | 15582 40621 3011087 74.1 | 80.142 % | c | 46122 | 46748 96684 | 17140 18203 1211729 66.6 | 80.221 % | c | 46272 | 46748 96684 | 18854 18353 1218705 66.4 | 80.221 % | c | 46497 | 46714 96607 | 20739 18539 1230555 66.4 | 80.297 % | c | 46834 | 46703 96582 | 22813 18867 1250274 66.3 | 80.325 % | c | 47340 | 46651 96453 | 25094 19368 1284175 66.3 | 80.473 % | c | 48100 | 46472 96017 | 27604 20063 1320976 65.8 | 80.974 % | c | 49239 | 46437 95936 | 30364 21181 1424831 67.3 | 81.066 % | c | 50947 | 46434 95929 | 33401 22886 1532403 67.0 | 81.074 % | c | 53509 | 46389 95814 | 36741 25444 1762687 69.3 | 81.214 % | c | 57353 | 46351 95720 | 40415 29177 2121672 72.7 | 81.326 % | c | 63119 | 46102 95119 | 44457 34489 2610152 75.7 | 82.030 % | c | 71769 | 46087 95084 | 48902 43071 3470985 80.6 | 82.070 % | c | 84743 | 46022 94925 | 53793 55928 4763761 85.2 | 82.259 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 91656 | 46006 94872 | 15335 62707 5469040 87.2 | 82.259 % | c | 91756 | 46006 94872 | 16868 20099 1258236 62.6 | 82.312 % | c | 91906 | 46004 94868 | 18555 20247 1269896 62.7 | 82.316 % | c | 92131 | 45981 94815 | 20410 20467 1286191 62.8 | 82.376 % | c | 92469 | 45978 94808 | 22451 20801 1325256 63.7 | 82.384 % | c | 92975 | 45956 94754 | 24697 21154 1350045 63.8 | 82.448 % | c | 93735 | 45891 94586 | 27166 21886 1408143 64.3 | 82.640 % | c | 94874 | 45891 94586 | 29883 23025 1506974 65.4 | 82.640 % | c | 96582 | 45850 94484 | 32871 24718 1656829 67.0 | 82.756 % | c | 99144 | 45850 94484 | 36159 27280 1890855 69.3 | 82.756 % | c | 102988 | 45767 94285 | 39775 31063 2199681 70.8 | 82.989 % | c | 108754 | 45767 94285 | 43752 36829 2758646 74.9 | 82.988 % | c | 117404 | 45755 94257 | 48127 45475 3584527 78.8 | 83.021 % | c | 130378 | 45713 94155 | 52940 58391 4806838 82.3 | 83.141 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 136420 | 45733 94207 | 15244 64433 5331404 82.7 | 83.141 % | c | 136520 | 45733 94207 | 16768 20826 1132496 54.4 | 83.107 % | c | 136670 | 45733 94207 | 18445 20976 1139985 54.3 | 83.107 % | c | 136895 | 45733 94207 | 20289 21201 1153537 54.4 | 83.107 % | c | 137232 | 45733 94207 | 22318 21538 1169510 54.3 | 83.107 % | c | 137738 | 45733 94207 | 24550 22044 1213136 55.0 | 83.107 % | c | 138497 | 45733 94207 | 27005 22803 1266674 55.5 | 83.108 % | c | 139636 | 45733 94207 | 29706 23942 1351252 56.4 | 83.107 % | c | 141344 | 45733 94207 | 32676 25650 1504180 58.6 | 83.107 % | c | 143906 | 45733 94207 | 35944 28212 1667932 59.1 | 83.107 % | c | 147751 | 45733 94207 | 39539 32057 2014186 62.8 | 83.107 % | c | 153517 | 45733 94207 | 43492 37823 2552526 67.5 | 83.107 % | c | 162166 | 45681 94069 | 47842 46460 3249653 69.9 | 83.271 % | c | 175140 | 45681 94069 | 52626 59434 4360949 73.4 | 83.271 % | c | 194601 | 45651 93995 | 57889 24662 1331831 54.0 | 83.359 % | c | 223793 | 45636 93958 | 63677 53847 4465405 82.9 | 83.403 % | c | 267582 | 45636 93958 | 70045 31596 1238437 39.2 | 83.403 % | c | 333266 | 45616 93912 | 77050 24572 866247 35.3 | 83.455 % | c | 431792 | 45563 93787 | 84755 42419 1615243 38.1 | 83.599 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 22890 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.95 0.90 2/54 22886 Raw data (stat): 22886 (runsolver) R 22885 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795456914 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0002 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0008 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0004 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0012 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0008 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0005 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0011 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0008 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.001 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+219.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+229.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+239.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+249.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+259.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+269.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+279.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+289.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+299.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+309.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+319.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+329.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+339.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+349.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+359.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+369.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+379.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+389.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+399.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+409.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+419.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+429.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+439.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+449.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+459.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+469.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+479.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+489.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+499.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+509.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+519.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+529.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+539.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+549.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+559.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+569.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+579.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+589.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+599.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+609.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+619.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+629.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+639.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+649.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+659.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+669.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+679.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+689.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+699.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+709.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+719.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+729.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+739.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+749.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+759.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+769.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+779.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+789.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+799.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+809.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+819.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+829.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+839.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+849.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+859.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+869.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+879.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+889.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+899.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+909.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+919.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+929.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+939.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+949.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+959.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+969.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+979.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+989.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+999.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1009.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1019.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1029.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1039.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1049.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1059.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1069.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1079.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1089.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1099.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1109.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1119.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1129.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1139.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1149.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1159.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1169.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1179.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1189.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1199.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1209.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1219.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 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.91 1/53 22890 Raw data (stat): 22886 (minisat+_script) S 22885 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795456914 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 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.39 CPU system time (s): 0.460929 CPU usage (%): 100.014 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####