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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-l152lav.opb
MD5SUM00855a9538cee8df79108d56ee6867b4
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 5046
Optimality of the best value was proved NO
Number of terms in the objective function 1989
Biggest coefficient in the objective function 268
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 382524
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 268
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 382524
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.28
Number of variables1989
Total number of constraints2086
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2085
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint1989

Trace number 22296 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-22 02:39:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11900 boxname=wulflinc1 idbench=916 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 11900
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        505924 kB
Buffers:          5196 kB
Cached:         498820 kB
SwapCached:          0 kB
Active:          89048 kB
Inactive:       418136 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        505644 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            15800 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:59:05 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 11900 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   97077   314005 |   32359       0        0     nan |  0.000 % |
c |       100 |   96947   313559 |   35594      82     1270    15.5 |  0.582 % |
c |       251 |   96883   313337 |   39154     212    15944    75.2 |  0.639 % |
c |       476 |   96883   313337 |   43069     437    24593    56.3 |  0.639 % |
c |       813 |   96398   311624 |   47376     699    28796    41.2 |  0.981 % |
c |      1320 |   96280   311210 |   52114    1189    64686    54.4 |  1.062 % |
c |      2079 |   96249   311105 |   57325    1943    92323    47.5 |  1.079 % |
c |      3223 |   96179   310853 |   63058    3077   320979   104.3 |  1.123 % |
c |      4931 |   96005   310207 |   69364    4745   498190   105.0 |  1.229 % |
c |      7493 |   95381   308039 |   76300    7204   629523    87.4 |  1.673 % |
c |     11337 |   94537   305108 |   83930   10849   722117    66.6 |  2.263 % |
c |     17103 |   94126   303709 |   92324   16521   986489    59.7 |  2.520 % |
c |     25752 |   93634   301995 |  101556   25094  1804121    71.9 |  2.821 % |
c |     38728 |   93305   300886 |  111712   38012  3779797    99.4 |  3.028 % |
c |     58192 |   93290   300833 |  122883   57465  9794628   170.4 |  3.032 % |
c |     87386 |   93201   300510 |  135171   86640 15885253   183.3 |  3.085 % |
c |    131175 |   93099   300164 |  148688  130408 28212586   216.3 |  3.150 % |
c |    196860 |   92835   299270 |  163557   74455 14452111   194.1 |  3.289 % |
#### 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.84 0.94 0.91 2/56 8549
Raw data (stat): 8549 (runsolver) R 8548 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 435109007 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0009 s]
Raw data (loadavg): 0.87 0.94 0.91 2/56 8549
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 4364 0 0 0 989 10 0 0 25 0 1 0 435109007 20140032 4000 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4917 4000 603 41 0 4876 0
vsize: 19668
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.91 2/56 8549
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 4695 0 0 0 1988 11 0 0 25 0 1 0 435109007 21487616 4331 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5246 4331 603 41 0 5205 0
vsize: 20984
[startup+30.0025 s]
Raw data (loadavg): 0.90 0.94 0.91 2/56 8549
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 4838 0 0 0 2988 11 0 0 25 0 1 0 435109007 22163456 4474 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5411 4474 603 41 0 5370 0
vsize: 21644
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.91 2/56 8549
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 4965 0 0 0 3987 12 0 0 25 0 1 0 435109007 22564864 4601 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5509 4601 603 41 0 5468 0
vsize: 22036
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.94 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 5220 0 0 0 4986 13 0 0 25 0 1 0 435109007 23638016 4856 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 4856 603 41 0 5730 0
vsize: 23084
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 5666 0 0 0 5985 14 0 0 25 0 1 0 435109007 25530368 5302 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6233 5302 603 41 0 6192 0
vsize: 24932
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 5987 0 0 0 6984 15 0 0 25 0 1 0 435109007 26873856 5623 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6561 5623 603 41 0 6520 0
vsize: 26244
[startup+80.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 6289 0 0 0 7983 17 0 0 25 0 1 0 435109007 28086272 5925 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6857 5925 603 41 0 6816 0
vsize: 27428
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 6837 0 0 0 8982 18 0 0 25 0 1 0 435109007 30240768 6473 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7383 6473 603 41 0 7342 0
vsize: 29532
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 7455 0 0 0 9980 20 0 0 25 0 1 0 435109007 32808960 7091 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8010 7091 603 41 0 7969 0
vsize: 32040
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 7744 0 0 0 10980 20 0 0 25 0 1 0 435109007 34144256 7380 4294967295 134512640 134672761 3221224624 3221223728 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8336 7380 603 41 0 8295 0
vsize: 33344
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 8227 0 0 0 11979 21 0 0 25 0 1 0 435109007 36012032 7863 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8792 7863 603 41 0 8751 0
vsize: 35168
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 8701 0 0 0 12978 23 0 0 25 0 1 0 435109007 38019072 8337 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9282 8337 603 41 0 9241 0
vsize: 37128
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 9267 0 0 0 13976 24 0 0 25 0 1 0 435109007 40304640 8903 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9840 8903 603 41 0 9799 0
vsize: 39360
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 9857 0 0 0 14975 26 0 0 25 0 1 0 435109007 42721280 9493 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10430 9493 603 41 0 10389 0
vsize: 41720
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 10400 0 0 0 15973 27 0 0 25 0 1 0 435109007 44871680 10036 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10955 10036 603 41 0 10914 0
vsize: 43820
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 10907 0 0 0 16972 29 0 0 25 0 1 0 435109007 47017984 10543 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11479 10543 603 41 0 11438 0
vsize: 45916
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 11403 0 0 0 17971 30 0 0 25 0 1 0 435109007 49045504 11039 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11974 11039 603 41 0 11933 0
vsize: 47896
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 11824 0 0 0 18969 32 0 0 25 0 1 0 435109007 50782208 11460 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12398 11460 603 41 0 12357 0
vsize: 49592
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 12254 0 0 0 19968 33 0 0 25 0 1 0 435109007 52510720 11890 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11890 603 41 0 12779 0
vsize: 51280
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 12585 0 0 0 20968 34 0 0 25 0 1 0 435109007 53858304 12221 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13149 12221 603 41 0 13108 0
vsize: 52596
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 12908 0 0 0 21967 35 0 0 25 0 1 0 435109007 55177216 12544 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13471 12544 603 41 0 13430 0
vsize: 53884
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 13225 0 0 0 22966 36 0 0 25 0 1 0 435109007 56504320 12861 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13795 12861 603 41 0 13754 0
vsize: 55180
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 13600 0 0 0 23965 37 0 0 25 0 1 0 435109007 57987072 13236 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14157 13236 603 41 0 14116 0
vsize: 56628
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 14036 0 0 0 24964 38 0 0 25 0 1 0 435109007 59858944 13672 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14614 13672 603 41 0 14573 0
vsize: 58456
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 14503 0 0 0 25963 39 0 0 25 0 1 0 435109007 61747200 14139 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15075 14139 603 41 0 15034 0
vsize: 60300
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 14969 0 0 0 26962 41 0 0 25 0 1 0 435109007 63639552 14605 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15537 14605 603 41 0 15496 0
vsize: 62148
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 15373 0 0 0 27961 41 0 0 25 0 1 0 435109007 65261568 15009 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15933 15009 603 41 0 15892 0
vsize: 63732
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 15852 0 0 0 28959 43 0 0 25 0 1 0 435109007 67268608 15488 4294967295 134512640 134672761 3221224624 3221223728 134555216 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16423 15488 603 41 0 16382 0
vsize: 65692
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 16316 0 0 0 29959 44 0 0 25 0 1 0 435109007 69423104 15952 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16949 15952 603 41 0 16908 0
vsize: 67796
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 16661 0 0 0 30958 45 0 0 25 0 1 0 435109007 70762496 16297 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17276 16297 603 41 0 17235 0
vsize: 69104
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 17022 0 0 0 31957 47 0 0 25 0 1 0 435109007 72232960 16658 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17635 16658 603 41 0 17594 0
vsize: 70540
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 17544 0 0 0 32956 48 0 0 25 0 1 0 435109007 74371072 17180 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18157 17180 603 41 0 18116 0
vsize: 72628
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8551
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 18012 0 0 0 33955 49 0 0 25 0 1 0 435109007 76251136 17648 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18616 17648 603 41 0 18575 0
vsize: 74464
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 18529 0 0 0 34953 51 0 0 25 0 1 0 435109007 78397440 18165 4294967295 134512640 134672761 3221224624 3221223728 134560013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19140 18165 603 41 0 19099 0
vsize: 76560
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 18965 0 0 0 35952 52 0 0 25 0 1 0 435109007 80138240 18601 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19565 18601 603 41 0 19524 0
vsize: 78260
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 19427 0 0 0 36952 53 0 0 25 0 1 0 435109007 82018304 19063 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20024 19063 603 41 0 19983 0
vsize: 80096
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 19896 0 0 0 37950 55 0 0 25 0 1 0 435109007 84021248 19532 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20513 19532 603 41 0 20472 0
vsize: 82052
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 20350 0 0 0 38949 56 0 0 25 0 1 0 435109007 85770240 19986 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20940 19986 603 41 0 20899 0
vsize: 83760
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 20779 0 0 0 39947 58 0 0 25 0 1 0 435109007 87638016 20415 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21396 20415 603 41 0 21355 0
vsize: 85584
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 21149 0 0 0 40946 59 0 0 25 0 1 0 435109007 89124864 20785 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21759 20785 603 41 0 21718 0
vsize: 87036
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 21553 0 0 0 41945 60 0 0 25 0 1 0 435109007 90734592 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22152 21189 603 41 0 22111 0
vsize: 88608
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 22031 0 0 0 42944 62 0 0 25 0 1 0 435109007 92737536 21667 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22641 21667 603 41 0 22600 0
vsize: 90564
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 22557 0 0 0 43943 63 0 0 25 0 1 0 435109007 94879744 22193 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23164 22193 603 41 0 23123 0
vsize: 92656
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 23105 0 0 0 44942 64 0 0 25 0 1 0 435109007 97009664 22741 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23684 22741 603 41 0 23643 0
vsize: 94736
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 23623 0 0 0 45940 66 0 0 25 0 1 0 435109007 99262464 23259 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24234 23259 603 41 0 24193 0
vsize: 96936
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 3/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 24001 0 0 0 46940 66 0 0 25 0 1 0 435109007 100724736 23637 4294967295 134512640 134672761 3221224624 3221223624 1075352757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24591 23637 603 41 0 24550 0
vsize: 98364
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 24418 0 0 0 47939 67 0 0 25 0 1 0 435109007 102424576 24054 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25006 24054 603 41 0 24965 0
vsize: 100024
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 24666 0 0 0 48939 68 0 0 25 0 1 0 435109007 103497728 24302 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25268 24302 603 41 0 25227 0
vsize: 101072
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 25108 0 0 0 49938 69 0 0 25 0 1 0 435109007 105222144 24744 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25689 24744 603 41 0 25648 0
vsize: 102756
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 25595 0 0 0 50936 70 0 0 25 0 1 0 435109007 107233280 25231 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26180 25231 603 41 0 26139 0
vsize: 104720
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 26080 0 0 0 51935 71 0 0 25 0 1 0 435109007 109232128 25716 4294967295 134512640 134672761 3221224624 3221223728 134554907 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26668 25716 603 41 0 26627 0
vsize: 106672
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 26517 0 0 0 52935 72 0 0 25 0 1 0 435109007 110956544 26153 4294967295 134512640 134672761 3221224624 3221223760 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27089 26153 603 41 0 27048 0
vsize: 108356
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 26958 0 0 0 53934 73 0 0 25 0 1 0 435109007 112836608 26594 4294967295 134512640 134672761 3221224624 3221223728 134560171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27548 26594 603 41 0 27507 0
vsize: 110192
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 27418 0 0 0 54933 74 0 0 25 0 1 0 435109007 114696192 27054 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28002 27054 603 41 0 27961 0
vsize: 112008
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 27836 0 0 0 55932 76 0 0 25 0 1 0 435109007 116428800 27472 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28425 27472 603 41 0 28384 0
vsize: 113700
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 28233 0 0 0 56931 76 0 0 25 0 1 0 435109007 118018048 27869 4294967295 134512640 134672761 3221224624 3221223728 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28813 27869 603 41 0 28772 0
vsize: 115252
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 28635 0 0 0 57930 78 0 0 25 0 1 0 435109007 119611392 28271 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29202 28271 603 41 0 29161 0
vsize: 116808
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 28973 0 0 0 58929 79 0 0 25 0 1 0 435109007 121077760 28609 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29560 28609 603 41 0 29519 0
vsize: 118240
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 29489 0 0 0 59928 80 0 0 25 0 1 0 435109007 123113472 29125 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30057 29125 603 41 0 30016 0
vsize: 120228
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 30013 0 0 0 60927 81 0 0 25 0 1 0 435109007 125259776 29649 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30581 29649 603 41 0 30540 0
vsize: 122324
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 30716 0 0 0 61925 83 0 0 25 0 1 0 435109007 128102400 30352 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31275 30352 603 41 0 31234 0
vsize: 125100
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 31342 0 0 0 62923 85 0 0 25 0 1 0 435109007 130654208 30979 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31898 30979 603 41 0 31857 0
vsize: 127592
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8553
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 31734 0 0 0 63922 86 0 0 25 0 1 0 435109007 132263936 31370 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32291 31370 603 41 0 32250 0
vsize: 129164
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 32300 0 0 0 64920 89 0 0 25 0 1 0 435109007 134664192 31936 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32877 31936 603 41 0 32836 0
vsize: 131508
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 32821 0 0 0 65919 90 0 0 25 0 1 0 435109007 136798208 32457 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33398 32457 603 41 0 33357 0
vsize: 133592
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 33133 0 0 0 66918 91 0 0 25 0 1 0 435109007 137994240 32769 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33690 32769 603 41 0 33649 0
vsize: 134760
[startup+680.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 33448 0 0 0 67918 93 0 0 25 0 1 0 435109007 139317248 33084 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34013 33084 603 41 0 33972 0
vsize: 136052
[startup+690.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 33644 0 0 0 68918 93 0 0 25 0 1 0 435109007 140644352 33280 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34337 33280 603 41 0 34296 0
vsize: 137348
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 33957 0 0 0 69917 94 0 0 25 0 1 0 435109007 141983744 33593 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34664 33593 603 41 0 34623 0
vsize: 138656
[startup+710.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 34543 0 0 0 70916 95 0 0 25 0 1 0 435109007 144265216 34179 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35221 34179 603 41 0 35180 0
vsize: 140884
[startup+720.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 35138 0 0 0 71914 97 0 0 25 0 1 0 435109007 146796544 34774 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35839 34774 603 41 0 35798 0
vsize: 143356
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 35675 0 0 0 72913 98 0 0 25 0 1 0 435109007 148922368 35311 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36358 35311 603 41 0 36317 0
vsize: 145432
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 36145 0 0 0 73912 99 0 0 25 0 1 0 435109007 150810624 35781 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36819 35781 603 41 0 36778 0
vsize: 147276
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 36635 0 0 0 74912 100 0 0 25 0 1 0 435109007 152829952 36271 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37312 36271 603 41 0 37271 0
vsize: 149248
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 37122 0 0 0 75910 101 0 0 25 0 1 0 435109007 154828800 36758 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37800 36758 603 41 0 37759 0
vsize: 151200
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 37481 0 0 0 76910 102 0 0 25 0 1 0 435109007 156315648 37117 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38163 37117 603 41 0 38122 0
vsize: 152652
[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 37850 0 0 0 77909 103 0 0 25 0 1 0 435109007 157782016 37486 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38521 37486 603 41 0 38480 0
vsize: 154084
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38246 0 0 0 78908 105 0 0 25 0 1 0 435109007 159391744 37882 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38914 37882 603 41 0 38873 0
vsize: 155656
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38684 0 0 0 79906 106 0 0 25 0 1 0 435109007 161255424 38320 4294967295 134512640 134672761 3221224624 3221223728 134560128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39369 38320 603 41 0 39328 0
vsize: 157476
[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38892 0 0 0 80906 107 0 0 25 0 1 0 435109007 162066432 38528 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39567 38528 603 41 0 39526 0
vsize: 158268
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 81905 107 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223624 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+830.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 82905 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 83905 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 84905 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 85905 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+870.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 86905 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 87906 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 88906 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+900.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 89906 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+910.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 90906 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 91906 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 92906 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+940.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8555
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 93907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+950.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 94907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+960.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 95907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+970.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 96907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+980.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 97907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+990.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 98907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 99907 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 100908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 101908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 102908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 103908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 104908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 105908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 106908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 107908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 108908 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 109909 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 110909 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 111909 108 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 112909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 113909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 114909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 115909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 116909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 117909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 118909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 8557
Raw data (stat): 8549 (minisat+) R 8548 12452 12451 0 -1 0 38954 0 0 0 119909 109 0 0 25 0 1 0 435109007 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 8557
Raw data (stat): 8549 (minisat+) Z 8548 12452 12451 0 -1 12 38956 0 0 0 119909 116 0 0 25 0 1 0 435109007 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.26
CPU user time (s): 1199.09
CPU system time (s): 1.16982
CPU usage (%): 100.012
Max. virtual memory (Kb): 158528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####