PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-bal8x12.opb
MD5SUM	ff4c2c4c9f15b8f5e44f85b64f7c2f83
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	89133158
Optimality of the best value was proved	NO
Number of terms in the objective function	2976
Biggest coefficient in the objective function	412316860416
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	35253236940736
Number of bits of the sum of numbers in the objective function	46
Biggest number in a constraint	412316860416
Number of bits of the biggest number in a constraint	39
Biggest sum of numbers in a constraint	35253236940736
Number of bits of the biggest sum of numbers	46
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1230.8
Number of variables	2976
Total number of constraints	116
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	116
Minimum length of a constraint	31
Maximum length of a constraint	360
Trace number 30856

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-05-25 20:15:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22259 boxname=wulflinc11 idbench=1075 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  ff4c2c4c9f15b8f5e44f85b64f7c2f83  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-bal8x12.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-bal8x12.opb
IDLAUNCH: 22259
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        910900 kB
Buffers:          2300 kB
Cached:         101856 kB
SwapCached:        768 kB
Active:          38992 kB
Inactive:        67236 kB
HighTotal:      131008 kB
HighFree:        26684 kB
LowTotal:       903652 kB
LowFree:        884216 kB
SwapTotal:     2097136 kB
SwapFree:      2095468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5036 kB
Slab:            11756 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:36:06 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22259 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 136 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 134]---> Adder-cost: 306   maxlim: 164852   bits: 18/18
c ---[ 132]---> Adder-cost: 320   maxlim: 258036   bits: 19/18
c ---[ 130]---> Adder-cost: 320   maxlim: 265204   bits: 19/19
c ---[ 128]---> Adder-cost: 320   maxlim: 275444   bits: 19/19
c ---[ 126]---> Adder-cost: 320   maxlim: 252916   bits: 19/18
c ---[ 124]---> Adder-cost: 320   maxlim: 275444   bits: 19/19
c ---[ 122]---> Adder-cost: 306   maxlim: 169972   bits: 18/18
c ---[ 120]---> Adder-cost: 320   maxlim: 252916   bits: 19/18
c ---[ 118]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost: 1899     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> BDD-cost:   18
c ---[  94]---> BDD-cost:   18
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   16
c ---[  91]---> BDD-cost:   18
c ---[  90]---> BDD-cost:   18
c ---[  89]---> BDD-cost:   18
c ---[  88]---> BDD-cost:   18
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:   18
c ---[  85]---> BDD-cost:   18
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   18
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   16
c ---[  78]---> BDD-cost:   18
c ---[  77]---> BDD-cost:   18
c ---[  76]---> BDD-cost:   18
c ---[  75]---> BDD-cost:   18
c ---[  74]---> BDD-cost:   16
c ---[  73]---> BDD-cost:   18
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   19
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   22
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   16
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   18
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   19
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   22
c ---[  55]---> BDD-cost:   20
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   18
c ---[  51]---> BDD-cost:   18
c ---[  50]---> BDD-cost:   18
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   18
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   20
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   16
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   18
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   19
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   22
c ---[  29]---> BDD-cost:   20
c ---[  28]---> BDD-cost:   17
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   17
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   16
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  17]---> BDD-cost:   18
c ---[  16]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   17
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   16
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   18
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   18
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   18
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   20
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   72701   191717 |   24233       0        0     nan |  0.000 % |
c |       100 |   72648   191596 |   26656      95      443     4.7 | 11.505 % |
c |       250 |   72648   191596 |   29321     245      998     4.1 | 11.505 % |
c |       476 |   72589   191397 |   32254     465     1850     4.0 | 11.549 % |
c |       813 |   72524   191245 |   35479     799     3198     4.0 | 11.635 % |
c |      1320 |   72230   190574 |   39027    1279     5082     4.0 | 11.984 % |
c |      2079 |   72230   190574 |   42930    2038     8168     4.0 | 11.984 % |
c |      3218 |   71949   189853 |   47223    3146    12783     4.1 | 12.285 % |
c |      4926 |   71817   189546 |   51945    4844    21648     4.5 | 12.455 % |
c |      7489 |   71443   188692 |   57140    7380    35357     4.8 | 12.910 % |
c |     11333 |   71113   187909 |   62854   11194    56572     5.1 | 13.325 % |
c |     17099 |   70569   186511 |   69139   16900    93890     5.6 | 13.979 % |
c ==============================================================================
c [1mFound solution: 214009354[0m
c ---[   0]---> Adder-cost: 11188   maxlim: 669735350   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19604 |  148647   465692 |   49549   19396   113494     5.9 | 13.979 % |
c |     19704 |  148604   465594 |   54503   19494   114193     5.9 |  9.815 % |
c |     19854 |  148604   465594 |   59954   19644   115105     5.9 |  9.815 % |
c |     20079 |  148521   465374 |   65949   19860   116412     5.9 |  9.876 % |
c |     20416 |  148521   465374 |   72544   20197   122323     6.1 |  9.876 % |
c |     20922 |  148504   465323 |   79799   20702   128472     6.2 |  9.888 % |
c |     21682 |  148409   465034 |   87779   21438   134492     6.3 |  9.946 % |
c |     22821 |  148339   464840 |   96556   22569   149335     6.6 |  9.996 % |
c ==============================================================================
c [1mFound solution: 204589577[0m
c ---[   0]---> Adder-cost: 0   maxlim: 679155127   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24525 |  148366   465107 |   49455   24273   195564     8.1 |  9.996 % |
c |     24625 |  148366   465107 |   54400   24373   196124     8.0 | 10.030 % |
c |     24775 |  148366   465107 |   59840   24523   197229     8.0 | 10.030 % |
c |     25000 |  148366   465107 |   65824   24748   200407     8.1 | 10.030 % |
c |     25337 |  148352   465073 |   72407   25084   203859     8.1 | 10.041 % |
c ==============================================================================
c [1mFound solution: 201549050[0m
c ---[   0]---> Adder-cost: 0   maxlim: 682195654   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25700 |  148380   465385 |   49460   25447   209540     8.2 | 10.041 % |
c |     25800 |  148380   465385 |   54406   25547   209992     8.2 | 10.075 % |
c |     25952 |  148380   465385 |   59846   25699   210770     8.2 | 10.075 % |
c |     26177 |  148380   465385 |   65831   25924   211898     8.2 | 10.075 % |
c |     26514 |  148380   465385 |   72414   26261   214433     8.2 | 10.075 % |
c |     27020 |  148380   465385 |   79655   26767   218597     8.2 | 10.075 % |
c |     27779 |  148355   465327 |   87621   27524   227184     8.3 | 10.098 % |
c |     28918 |  148217   465004 |   96383   28650   236703     8.3 | 10.226 % |
c |     30627 |  148190   464926 |  106021   30355   257097     8.5 | 10.245 % |
c |     33189 |  148116   464742 |  116624   32912   301628     9.2 | 10.304 % |
c |     37034 |  148036   464487 |  128286   36736   402769    11.0 | 10.351 % |
c ==============================================================================
c [1mFound solution: 182813927[0m
c ---[   0]---> Adder-cost: 0   maxlim: 700930777   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40067 |  148058   464771 |   49352   39767   676544    17.0 | 10.351 % |
c |     40167 |  148058   464771 |   54287   39867   678895    17.0 | 10.392 % |
c |     40318 |  148058   464771 |   59715   40018   681716    17.0 | 10.392 % |
c |     40543 |  148058   464771 |   65687   40243   723475    18.0 | 10.392 % |
c |     40881 |  148058   464771 |   72256   40581   728356    17.9 | 10.392 % |
c |     41389 |  148058   464771 |   79481   41089   747126    18.2 | 10.392 % |
c |     42150 |  148058   464771 |   87430   41850   814270    19.5 | 10.392 % |
c |     43289 |  148058   464771 |   96173   42989   837052    19.5 | 10.392 % |
c |     44997 |  147926   464448 |  105790   44661   861269    19.3 | 10.493 % |
c |     47560 |  147749   464038 |  116369   47213  1070866    22.7 | 10.657 % |
c |     51404 |  147653   463818 |  128006   51038  1434153    28.1 | 10.741 % |
c |     57175 |  147619   463740 |  140807   56805  1873614    33.0 | 10.771 % |
c |     65824 |  147355   463125 |  154887   65420  2372271    36.3 | 11.011 % |
c ==============================================================================
c [1mFound solution: 149088699[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734656005   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73362 |  147380   463368 |   49126   72958  3211474    44.0 | 11.011 % |
c |     73462 |  147380   463368 |   54038   23056  1250058    54.2 | 11.044 % |
c |     73612 |  147358   463319 |   59442   23205  1250862    53.9 | 11.063 % |
c |     73837 |  147358   463319 |   65386   23430  1252080    53.4 | 11.063 % |
c |     74174 |  147358   463319 |   71925   23767  1253933    52.8 | 11.063 % |
c |     74681 |  147340   463276 |   79117   24273  1259866    51.9 | 11.083 % |
c |     75440 |  147340   463276 |   87029   25032  1265366    50.5 | 11.083 % |
c |     76579 |  147238   463042 |   95732   26162  1276581    48.8 | 11.175 % |
c |     78287 |  147238   463042 |  105305   27870  1297527    46.6 | 11.175 % |
c |     80849 |  147227   463016 |  115836   30431  1336211    43.9 | 11.186 % |
c |     84694 |  147210   462977 |  127420   34275  1561515    45.6 | 11.202 % |
c |     90463 |  147196   462946 |  140162   40043  1907558    47.6 | 11.214 % |
c |     99112 |  147190   462933 |  154178   48691  2322125    47.7 | 11.219 % |
c |    112087 |  147180   462908 |  169596   61665  5549172    90.0 | 11.227 % |
c |    131548 |  147154   462830 |  186555   81117  6761386    83.4 | 11.244 % |
c |    160740 |  147054   462595 |  205211  110302 10457947    94.8 | 11.342 % |
c ==============================================================================
c [1mFound solution: 147827184[0m
c ---[   0]---> Adder-cost: 0   maxlim: 735917520   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200049 |  147062   462811 |   49020  149609 14371103    96.1 | 11.342 % |
c |    200149 |  147062   462811 |   53922   23537  1092931    46.4 | 11.378 % |
c |    200299 |  147062   462811 |   59314   23687  1093531    46.2 | 11.378 % |
c |    200524 |  147056   462797 |   65245   23911  1094996    45.8 | 11.387 % |
c |    200861 |  147056   462797 |   71770   24248  1097032    45.2 | 11.387 % |
c |    201367 |  147051   462786 |   78947   24753  1102070    44.5 | 11.392 % |
c |    202126 |  147051   462786 |   86841   25512  1106908    43.4 | 11.392 % |
c |    203265 |  147051   462786 |   95526   26651  1130187    42.4 | 11.392 % |
c |    204973 |  147051   462786 |  105078   28359  1142252    40.3 | 11.392 % |
c |    207535 |  146935   462520 |  115586   30904  1165217    37.7 | 11.484 % |
c |    211379 |  146874   462379 |  127145   34741  1440132    41.5 | 11.545 % |
c |    217146 |  146874   462379 |  139859   40508  1869259    46.1 | 11.545 % |
c |    225795 |  146874   462379 |  153845   49157  2859362    58.2 | 11.545 % |
c |    238770 |  146874   462379 |  169230   62132  3541991    57.0 | 11.545 % |
c |    258231 |  146874   462379 |  186153   81593  6023294    73.8 | 11.545 % |
c |    287423 |  146839   462298 |  204768  110781 11247075   101.5 | 11.579 % |
c ==============================================================================
c [1mFound solution: 146553777[0m
c ---[   0]---> Adder-cost: 0   maxlim: 737190927   bits: 30/30
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    299535 |  146847   462399 |   48949  122893 13869998   112.9 | 11.579 % |
c |    299635 |  146847   462399 |   53843   23533  2683343   114.0 | 11.593 % |
c |    299785 |  146847   462399 |   59228   23683  2684495   113.4 | 11.593 % |
c |    300010 |  146847   462399 |   65151   23908  2685843   112.3 | 11.593 % |
c |    300350 |  146837   462376 |   71666   24245  2688095   110.9 | 11.601 % |
c |    300856 |  146837   462376 |   78832   24751  2690863   108.7 | 11.601 % |
c |    301615 |  146837   462376 |   86716   25510  2695601   105.7 | 11.601 % |
c |    302756 |  146837   462376 |   95387   26651  2753237   103.3 | 11.601 % |
c |    304466 |  146800   462287 |  104926   28356  2765516    97.5 | 11.635 % |
c |    307028 |  146800   462287 |  115419   30918  2807384    90.8 | 11.635 % |
c |    310872 |  146800   462287 |  126961   34762  2870461    82.6 | 11.635 % |
c |    316640 |  146800   462287 |  139657   40530  3806737    93.9 | 11.635 % |
c |    325289 |  146796   462278 |  153622   49178  4202356    85.5 | 11.637 % |
c |    338265 |  146796   462278 |  168985   62154 11027986   177.4 | 11.637 % |
c |    357728 |  146791   462262 |  185883   81614 13875573   170.0 | 11.640 % |
c |    386920 |  146791   462262 |  204472  110806 16922700   152.7 | 11.640 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10874 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 10870
Raw data (stat): 10870 (runsolver) R 10869 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783458571 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.0007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.0016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+950.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+990.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1210.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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+1220.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.73 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10874
Raw data (stat): 10870 (minisat+_script) S 10869 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783458571 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.73
CPU time (s): 1229.88
CPU user time (s): 1228.94
CPU system time (s): 0.949855
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####