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/MIPLIB/miplib3/normalized-mps-v2-20-10-p0548.opb
MD5SUM	10547c6c0f11ab5df74fcaff6ba6d160
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14938
Optimality of the best value was proved	NO
Number of terms in the objective function	416
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	96797
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	96797
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1230.87
Number of variables	548
Total number of constraints	724
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	550
Number of constraints which are nor clauses,nor cardinality constraints	134
Minimum length of a constraint	1
Maximum length of a constraint	143
Trace number 21108

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 22:47:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13741 boxname=wulflinc25 idbench=1057 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 13741
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        715512 kB
Buffers:         10084 kB
Cached:         289148 kB
SwapCached:        716 kB
Active:          51008 kB
Inactive:       250176 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        715260 kB
SwapTotal:     2097892 kB
SwapFree:      2096236 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12316 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:07:07 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 13741 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   46
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:   48
c ---[ 159]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:   75
c ---[ 156]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   54
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:  105
c ---[ 151]---> BDD-cost:  104
c ---[ 150]---> BDD-cost:  120
c ---[ 149]---> BDD-cost:   79
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:  115
c ---[ 146]---> BDD-cost:  107
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   55
c ---[ 143]---> BDD-cost:   87
c ---[ 142]---> BDD-cost:   54
c ---[ 141]---> BDD-cost:  164
c ---[ 140]---> BDD-cost:  151
c ---[ 139]---> BDD-cost:   31
c ---[ 138]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   28
c ---[ 135]---> BDD-cost:   77
c ---[ 134]---> BDD-cost:  153
c ---[ 133]---> BDD-cost:  109
c ---[ 131]---> BDD-cost:  137
c ---[ 130]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:   56
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:    7
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   24
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:   29
c ---[ 112]---> BDD-cost:    6
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   29
c ---[ 109]---> BDD-cost:   51
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:   35
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   29
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   49
c ---[  99]---> BDD-cost:   60
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   68
c ---[  92]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   47
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   68
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   12
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> BDD-cost:   37
c ---[  75]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   49
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    2
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24239    72664 |    8079       0        0     nan |  0.000 % |
c |       100 |   24204    72543 |    8886      94      630     6.7 |  2.627 % |
c |       250 |   24204    72543 |    9775     244     1500     6.1 |  2.627 % |
c |       475 |   24168    72424 |   10753     463     3762     8.1 |  2.700 % |
c |       812 |   24147    72351 |   11828     793     6573     8.3 |  2.736 % |
c |      1318 |   24094    72172 |   13011    1287    11505     8.9 |  2.845 % |
c |      2077 |   24070    72093 |   14312    2044    36065    17.6 |  2.881 % |
c |      3216 |   24070    72093 |   15743    3183    66248    20.8 |  2.881 % |
c |      4924 |   24070    72093 |   17318    4891   129432    26.5 |  2.881 % |
c |      7486 |   24046    72024 |   19049    7452   225412    30.2 |  2.917 % |
c |     11330 |   24030    71968 |   20954   11293   381242    33.8 |  2.953 % |
c |     17096 |   24024    71948 |   23050   17058   532868    31.2 |  2.972 % |
c |     25746 |   24024    71948 |   25355   13467   596053    44.3 |  2.972 % |
c |     38720 |   24024    71948 |   27890   13378   350688    26.2 |  2.972 % |
c |     58184 |   24024    71948 |   30679   17530   691331    39.4 |  2.972 % |
c |     87376 |   24024    71948 |   33747   27765   906272    32.6 |  2.972 % |
c |    131165 |   24016    71928 |   37122   30146  1168742    38.8 |  3.008 % |
c |    196849 |   24016    71928 |   40835   26633   994072    37.3 |  3.008 % |
c |    295375 |   24016    71928 |   44918   22515   781186    34.7 |  3.008 % |
c |    443166 |   23998    71874 |   49410   21696   804926    37.1 |  3.080 % |
c |    664849 |   23994    71864 |   54351   37767  1328360    35.2 |  3.099 % |
#### 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/54 16322
Raw data (stat): 16322 (runsolver) R 16321 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548804007 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 1823 0 0 0 994 4 0 0 25 0 1 0 548804007 9183232 1790 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2242 1790 603 41 0 2201 0
vsize: 8968
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2098 0 0 0 1993 5 0 0 25 0 1 0 548804007 10248192 2065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2502 2065 603 41 0 2461 0
vsize: 10008
[startup+29.9999 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2183 0 0 0 2992 5 0 0 25 0 1 0 548804007 10514432 2150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2567 2150 603 41 0 2526 0
vsize: 10268
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2301 0 0 0 3992 5 0 0 25 0 1 0 548804007 11051008 2268 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2698 2268 603 41 0 2657 0
vsize: 10792
[startup+50.0014 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2492 0 0 0 4992 6 0 0 25 0 1 0 548804007 11849728 2459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2893 2459 603 41 0 2852 0
vsize: 11572
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2498 0 0 0 5992 6 0 0 25 0 1 0 548804007 11849728 2465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2893 2465 603 41 0 2852 0
vsize: 11572
[startup+70.0016 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2521 0 0 0 6992 6 0 0 25 0 1 0 548804007 11997184 2488 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2929 2488 603 41 0 2888 0
vsize: 11716
[startup+80.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2613 0 0 0 7992 6 0 0 25 0 1 0 548804007 12529664 2580 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3059 2580 603 41 0 3018 0
vsize: 12236
[startup+90.0025 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2622 0 0 0 8992 7 0 0 25 0 1 0 548804007 12529664 2589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3059 2589 603 41 0 3018 0
vsize: 12236
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2701 0 0 0 9992 7 0 0 25 0 1 0 548804007 12943360 2668 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3160 2668 603 41 0 3119 0
vsize: 12640
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 2822 0 0 0 10992 7 0 0 25 0 1 0 548804007 13348864 2789 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2789 603 41 0 3218 0
vsize: 13036
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3064 0 0 0 11992 8 0 0 25 0 1 0 548804007 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3031 603 41 0 3484 0
vsize: 14100
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3064 0 0 0 12992 8 0 0 25 0 1 0 548804007 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3031 603 41 0 3484 0
vsize: 14100
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3076 0 0 0 13991 8 0 0 25 0 1 0 548804007 14438400 3043 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3043 603 41 0 3484 0
vsize: 14100
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3076 0 0 0 14991 8 0 0 25 0 1 0 548804007 14438400 3043 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3043 603 41 0 3484 0
vsize: 14100
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3077 0 0 0 15991 8 0 0 25 0 1 0 548804007 14438400 3044 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3044 603 41 0 3484 0
vsize: 14100
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3082 0 0 0 16991 8 0 0 25 0 1 0 548804007 14438400 3049 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3049 603 41 0 3484 0
vsize: 14100
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3114 0 0 0 17990 9 0 0 25 0 1 0 548804007 14573568 3081 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3081 603 41 0 3517 0
vsize: 14232
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3146 0 0 0 18990 9 0 0 25 0 1 0 548804007 14716928 3113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3113 603 41 0 3552 0
vsize: 14372
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3167 0 0 0 19990 9 0 0 25 0 1 0 548804007 14876672 3134 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3632 3134 603 41 0 3591 0
vsize: 14528
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3248 0 0 0 20989 10 0 0 25 0 1 0 548804007 15142912 3215 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3697 3215 603 41 0 3656 0
vsize: 14788
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3283 0 0 0 21990 10 0 0 25 0 1 0 548804007 15421440 3250 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3250 603 41 0 3724 0
vsize: 15060
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3287 0 0 0 22990 10 0 0 25 0 1 0 548804007 15421440 3254 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3254 603 41 0 3724 0
vsize: 15060
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3304 0 0 0 23990 10 0 0 25 0 1 0 548804007 15421440 3271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3271 603 41 0 3724 0
vsize: 15060
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3307 0 0 0 24990 10 0 0 25 0 1 0 548804007 15585280 3274 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3805 3274 603 41 0 3764 0
vsize: 15220
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3317 0 0 0 25990 10 0 0 25 0 1 0 548804007 15585280 3284 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3805 3284 603 41 0 3764 0
vsize: 15220
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3338 0 0 0 26990 10 0 0 25 0 1 0 548804007 15749120 3305 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3845 3305 603 41 0 3804 0
vsize: 15380
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3352 0 0 0 27990 10 0 0 25 0 1 0 548804007 15749120 3319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3845 3319 603 41 0 3804 0
vsize: 15380
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3366 0 0 0 28991 10 0 0 25 0 1 0 548804007 15912960 3333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3333 603 41 0 3844 0
vsize: 15540
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3367 0 0 0 29991 10 0 0 25 0 1 0 548804007 15912960 3334 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3367 0 0 0 30991 10 0 0 25 0 1 0 548804007 15912960 3334 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3368 0 0 0 31991 10 0 0 25 0 1 0 548804007 15912960 3335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3335 603 41 0 3844 0
vsize: 15540
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3368 0 0 0 32991 10 0 0 25 0 1 0 548804007 15912960 3335 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3335 603 41 0 3844 0
vsize: 15540
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3382 0 0 0 33991 10 0 0 25 0 1 0 548804007 15912960 3349 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3349 603 41 0 3844 0
vsize: 15540
[startup+350.005 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3442 0 0 0 34990 10 0 0 25 0 1 0 548804007 16211968 3409 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3958 3409 603 41 0 3917 0
vsize: 15832
[startup+360.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3617 0 0 0 35990 11 0 0 25 0 1 0 548804007 16883712 3584 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4122 3584 603 41 0 4081 0
vsize: 16488
[startup+370.005 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3631 0 0 0 36990 11 0 0 25 0 1 0 548804007 17018880 3598 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3598 603 41 0 4114 0
vsize: 16620
[startup+380.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3639 0 0 0 37990 11 0 0 25 0 1 0 548804007 17018880 3606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3606 603 41 0 4114 0
vsize: 16620
[startup+390.006 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3676 0 0 0 38991 11 0 0 25 0 1 0 548804007 17182720 3643 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3643 603 41 0 4154 0
vsize: 16780
[startup+400.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3695 0 0 0 39991 11 0 0 25 0 1 0 548804007 17346560 3662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4235 3662 603 41 0 4194 0
vsize: 16940
[startup+410.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3741 0 0 0 40991 11 0 0 25 0 1 0 548804007 17477632 3708 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4267 3708 603 41 0 4226 0
vsize: 17068
[startup+420.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3742 0 0 0 41991 11 0 0 25 0 1 0 548804007 17477632 3709 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4267 3709 603 41 0 4226 0
vsize: 17068
[startup+430.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3763 0 0 0 42991 11 0 0 25 0 1 0 548804007 17620992 3730 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3730 603 41 0 4261 0
vsize: 17208
[startup+440.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3806 0 0 0 43991 11 0 0 25 0 1 0 548804007 17752064 3773 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3773 603 41 0 4293 0
vsize: 17336
[startup+450.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3806 0 0 0 44991 11 0 0 25 0 1 0 548804007 17752064 3773 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3773 603 41 0 4293 0
vsize: 17336
[startup+460.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3820 0 0 0 45992 11 0 0 25 0 1 0 548804007 17899520 3787 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4370 3787 603 41 0 4329 0
vsize: 17480
[startup+470.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 3844 0 0 0 46992 11 0 0 25 0 1 0 548804007 17899520 3811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4370 3811 603 41 0 4329 0
vsize: 17480
[startup+480.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4105 0 0 0 47992 12 0 0 25 0 1 0 548804007 19095552 4072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4662 4072 603 41 0 4621 0
vsize: 18648
[startup+490.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4212 0 0 0 48991 12 0 0 25 0 1 0 548804007 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+500.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4212 0 0 0 49992 12 0 0 25 0 1 0 548804007 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+510.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4212 0 0 0 50992 12 0 0 25 0 1 0 548804007 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+520.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4255 0 0 0 51992 12 0 0 25 0 1 0 548804007 19648512 4222 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4797 4222 603 41 0 4756 0
vsize: 19188
[startup+530.005 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4259 0 0 0 52992 12 0 0 25 0 1 0 548804007 19648512 4226 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4797 4226 603 41 0 4756 0
vsize: 19188
[startup+540.006 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4350 0 0 0 53992 13 0 0 25 0 1 0 548804007 20062208 4317 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+550.006 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4350 0 0 0 54992 13 0 0 25 0 1 0 548804007 20062208 4317 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+560.006 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4362 0 0 0 55991 13 0 0 25 0 1 0 548804007 20213760 4329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4935 4329 603 41 0 4894 0
vsize: 19740
[startup+570.007 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4392 0 0 0 56991 13 0 0 25 0 1 0 548804007 20377600 4359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4359 603 41 0 4934 0
vsize: 19900
[startup+580.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4409 0 0 0 57991 13 0 0 25 0 1 0 548804007 20377600 4376 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4376 603 41 0 4934 0
vsize: 19900
[startup+590.007 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4409 0 0 0 58992 13 0 0 25 0 1 0 548804007 20377600 4376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4376 603 41 0 4934 0
vsize: 19900
[startup+600.008 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4433 0 0 0 59992 13 0 0 25 0 1 0 548804007 20541440 4400 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5015 4400 603 41 0 4974 0
vsize: 20060
[startup+610.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4448 0 0 0 60992 13 0 0 25 0 1 0 548804007 20541440 4415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5015 4415 603 41 0 4974 0
vsize: 20060
[startup+620.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4487 0 0 0 61992 13 0 0 25 0 1 0 548804007 20738048 4454 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5063 4454 603 41 0 5022 0
vsize: 20252
[startup+630.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4521 0 0 0 62992 14 0 0 25 0 1 0 548804007 20934656 4488 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+640.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4521 0 0 0 63992 14 0 0 25 0 1 0 548804007 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+650.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4521 0 0 0 64992 14 0 0 25 0 1 0 548804007 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+660.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4521 0 0 0 65992 14 0 0 25 0 1 0 548804007 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+670.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4534 0 0 0 66992 14 0 0 25 0 1 0 548804007 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+680.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4534 0 0 0 67992 14 0 0 25 0 1 0 548804007 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+690.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4534 0 0 0 68992 14 0 0 25 0 1 0 548804007 20934656 4501 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+700.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4534 0 0 0 69992 14 0 0 25 0 1 0 548804007 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+710.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4628 0 0 0 70992 15 0 0 25 0 1 0 548804007 21352448 4595 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5213 4595 603 41 0 5172 0
vsize: 20852
[startup+720.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4639 0 0 0 71992 15 0 0 25 0 1 0 548804007 21516288 4606 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5253 4606 603 41 0 5212 0
vsize: 21012
[startup+730.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4660 0 0 0 72992 15 0 0 25 0 1 0 548804007 21516288 4627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5253 4627 603 41 0 5212 0
vsize: 21012
[startup+740.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4681 0 0 0 73993 15 0 0 25 0 1 0 548804007 21680128 4648 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5293 4648 603 41 0 5252 0
vsize: 21172
[startup+750.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4702 0 0 0 74993 15 0 0 25 0 1 0 548804007 21872640 4669 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4669 603 41 0 5299 0
vsize: 21360
[startup+760.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4704 0 0 0 75993 15 0 0 25 0 1 0 548804007 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+770.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16322
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4704 0 0 0 76993 15 0 0 25 0 1 0 548804007 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+780.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 16354
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4704 0 0 0 77993 15 0 0 25 0 1 0 548804007 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+790.012 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 16375
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4710 0 0 0 78986 23 0 0 25 0 1 0 548804007 21872640 4677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4677 603 41 0 5299 0
vsize: 21360
[startup+800.013 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 16375
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4712 0 0 0 79986 23 0 0 25 0 1 0 548804007 21872640 4679 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4679 603 41 0 5299 0
vsize: 21360
[startup+810.012 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 16375
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4712 0 0 0 80986 23 0 0 25 0 1 0 548804007 21872640 4679 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4679 603 41 0 5299 0
vsize: 21360
[startup+820.013 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 16375
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4723 0 0 0 81985 24 0 0 25 0 1 0 548804007 21872640 4690 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4690 603 41 0 5299 0
vsize: 21360
[startup+830.013 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 16375
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4723 0 0 0 82985 24 0 0 25 0 1 0 548804007 21872640 4690 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4690 603 41 0 5299 0
vsize: 21360
[startup+840.014 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 16375
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4725 0 0 0 83985 24 0 0 25 0 1 0 548804007 21872640 4692 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+850.015 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4725 0 0 0 84985 25 0 0 25 0 1 0 548804007 21872640 4692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+860.014 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4735 0 0 0 85985 25 0 0 25 0 1 0 548804007 22036480 4702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4702 603 41 0 5339 0
vsize: 21520
[startup+870.015 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4737 0 0 0 86984 26 0 0 25 0 1 0 548804007 22036480 4704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4704 603 41 0 5339 0
vsize: 21520
[startup+880.015 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4909 0 0 0 87984 26 0 0 25 0 1 0 548804007 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+890.024 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4909 0 0 0 88985 27 0 0 25 0 1 0 548804007 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+900.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4909 0 0 0 89985 27 0 0 25 0 1 0 548804007 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+910.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4909 0 0 0 90984 28 0 0 25 0 1 0 548804007 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+920.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 4909 0 0 0 91984 28 0 0 25 0 1 0 548804007 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5237 0 0 0 92983 30 0 0 25 0 1 0 548804007 24039424 5204 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5204 603 41 0 5828 0
vsize: 23476
[startup+940.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5290 0 0 0 93982 31 0 0 25 0 1 0 548804007 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+950.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5290 0 0 0 94982 32 0 0 25 0 1 0 548804007 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+960.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5290 0 0 0 95982 32 0 0 25 0 1 0 548804007 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+970.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5290 0 0 0 96982 32 0 0 25 0 1 0 548804007 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+980.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5543 0 0 0 97982 33 0 0 25 0 1 0 548804007 25247744 5510 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6164 5510 603 41 0 6123 0
vsize: 24656
[startup+990.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5845 0 0 0 98980 35 0 0 25 0 1 0 548804007 26460160 5812 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6460 5812 603 41 0 6419 0
vsize: 25840
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5964 0 0 0 99979 36 0 0 25 0 1 0 548804007 27004928 5931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5931 603 41 0 6552 0
vsize: 26372
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5970 0 0 0 100979 36 0 0 25 0 1 0 548804007 27004928 5937 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5970 0 0 0 101979 37 0 0 25 0 1 0 548804007 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5975 0 0 0 102979 37 0 0 25 0 1 0 548804007 27148288 5942 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5942 603 41 0 6587 0
vsize: 26512
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5983 0 0 0 103978 38 0 0 25 0 1 0 548804007 27148288 5950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5950 603 41 0 6587 0
vsize: 26512
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5991 0 0 0 104978 38 0 0 25 0 1 0 548804007 27148288 5958 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5958 603 41 0 6587 0
vsize: 26512
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 5991 0 0 0 105978 38 0 0 25 0 1 0 548804007 27148288 5958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5958 603 41 0 6587 0
vsize: 26512
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6000 0 0 0 106977 39 0 0 25 0 1 0 548804007 27148288 5967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5967 603 41 0 6587 0
vsize: 26512
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6000 0 0 0 107977 39 0 0 25 0 1 0 548804007 27148288 5967 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5967 603 41 0 6587 0
vsize: 26512
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6001 0 0 0 108977 40 0 0 25 0 1 0 548804007 27148288 5968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6628 5968 603 41 0 6587 0
vsize: 26512
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16377
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6011 0 0 0 109977 40 0 0 25 0 1 0 548804007 27344896 5978 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5978 603 41 0 6635 0
vsize: 26704
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6012 0 0 0 110976 41 0 0 25 0 1 0 548804007 27344896 5979 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6012 0 0 0 111976 41 0 0 25 0 1 0 548804007 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6012 0 0 0 112976 42 0 0 25 0 1 0 548804007 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6012 0 0 0 113976 42 0 0 25 0 1 0 548804007 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6012 0 0 0 114975 43 0 0 25 0 1 0 548804007 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6021 0 0 0 115975 43 0 0 25 0 1 0 548804007 27344896 5988 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5988 603 41 0 6635 0
vsize: 26704
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6022 0 0 0 116975 44 0 0 25 0 1 0 548804007 27344896 5989 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6022 0 0 0 117975 44 0 0 25 0 1 0 548804007 27344896 5989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6023 0 0 0 118975 44 0 0 25 0 1 0 548804007 27344896 5990 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5990 603 41 0 6635 0
vsize: 26704
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16379
Raw data (stat): 16322 (minisat+) R 16321 28099 28098 0 -1 0 6024 0 0 0 119975 45 0 0 25 0 1 0 548804007 27344896 5991 4294967295 134512640 134672761 3221224544 3221223732 1075347078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 5991 603 41 0 6635 0
vsize: 26704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 16379
Raw data (stat): 16322 (minisat+) Z 16321 28099 28098 0 -1 12 6026 0 0 0 119975 46 0 0 25 0 1 0 548804007 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.06
CPU time (s): 1200.22
CPU user time (s): 1199.75
CPU system time (s): 0.463929
CPU usage (%): 100.013
Max. virtual memory (Kb): 26704
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####