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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08a.opb
MD5SUM	962e64054cef66ff1ace4918a032c24a
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1983976
Optimality of the best value was proved	NO
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	3584
Total number of constraints	200
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	136
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 18479

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 15:14:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17924 boxname=wulflinc19 idbench=1379 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  962e64054cef66ff1ace4918a032c24a  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 17924
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        747928 kB
Buffers:         23836 kB
Cached:         238768 kB
SwapCached:        556 kB
Active:          39532 kB
Inactive:       225144 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        747676 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16360 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:34:33 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 17924 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 198]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 196]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 195]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 194]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 193]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 192]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 191]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 190]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 189]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 188]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 187]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 186]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 184]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[ 183]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 182]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 181]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 180]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 179]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 178]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 177]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 176]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 175]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 174]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 172]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 171]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 170]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 169]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 168]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 167]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 166]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 165]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 164]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 163]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 162]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 160]---> Adder-cost: 160   maxlim: 2126077   bits: 23/22
c ---[ 159]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 158]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 157]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 156]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 155]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 154]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 153]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 151]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 149]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 147]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 145]---> Adder-cost: 80   maxlim: 1108990   bits: 22/21
c ---[ 143]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 141]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 139]---> Adder-cost: 160   maxlim: 2153725   bits: 23/22
c ---[ 137]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 135]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 133]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 131]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 129]---> Adder-cost: 80   maxlim: 1093630   bits: 22/21
c ---[ 127]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 125]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 123]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 121]---> Adder-cost: 160   maxlim: 2143485   bits: 23/22
c ---[ 119]---> Adder-cost: 160   maxlim: 2142205   bits: 23/22
c ---[ 117]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 115]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 113]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 111]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 109]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 107]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 105]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 103]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 101]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[  99]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[  97]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[  95]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[  93]---> Adder-cost: 80   maxlim: 1080062   bits: 22/21
c ---[  91]---> Adder-cost: 80   maxlim: 1105150   bits: 22/21
c ---[  89]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[  87]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[  85]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[  83]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[  81]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[  79]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[  77]---> Adder-cost: 80   maxlim: 1107710   bits: 22/21
c ---[  75]---> Adder-cost: 80   maxlim: 1081342   bits: 22/21
c ---[  73]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[  71]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[  69]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[  67]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[  65]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[  63]---> Adder-cost: 160   maxlim: 2122237   bits: 23/22
c ---[  61]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[  59]---> Adder-cost: 80   maxlim: 1076222   bits: 22/21
c ---[  57]---> Adder-cost: 80   maxlim: 1063678   bits: 22/21
c ---[  55]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[  53]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[  51]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[  49]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[  47]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[  45]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[  43]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[  41]---> Adder-cost: 80   maxlim: 1061118   bits: 22/21
c ---[  40]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[  39]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[  38]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[  37]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[  36]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[  34]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[  33]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[  32]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[  31]---> Adder-cost: 218   maxlim: 312823   bits: 19/19
c ---[  30]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  29]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  28]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  27]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  26]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  25]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  24]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  22]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[  21]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  20]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  19]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  18]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  17]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  16]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  15]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  14]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  13]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  12]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  10]---> Adder-cost: 80   maxlim: 1078782   bits: 22/21
c ---[   9]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[   8]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[   7]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[   6]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[   5]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[   4]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[   3]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[   2]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[   1]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[   0]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70648   254822 |   23549       0        0     nan |  0.000 % |
c |       100 |   70648   254822 |   25903     100      314     3.1 | 24.404 % |
c |       252 |   70640   254796 |   28494     251      781     3.1 | 24.410 % |
c |       477 |   70604   254680 |   31343     468     1527     3.3 | 24.439 % |
c |       814 |   70575   254585 |   34478     801     2763     3.4 | 24.462 % |
c |      1320 |   70528   254430 |   37925    1300     4619     3.6 | 24.502 % |
c |      2079 |   70484   254288 |   41718    2051     7556     3.7 | 24.537 % |
c |      3218 |   70442   254152 |   45890    3180    12518     3.9 | 24.571 % |
c |      4926 |   70286   253634 |   50479    4852    21008     4.3 | 24.704 % |
c |      7488 |   70180   253290 |   55527    7388    35704     4.8 | 24.796 % |
c |     11333 |   70110   253058 |   61080   11221    59602     5.3 | 24.853 % |
c |     17099 |   69925   252455 |   67188   16936    98900     5.8 | 25.009 % |
c |     25748 |   69728   251806 |   73906   25532   163984     6.4 | 25.176 % |
c |     38722 |   69680   251652 |   81297   38496   304156     7.9 | 25.216 % |
c |     58183 |   69470   250968 |   89427   57909   481490     8.3 | 25.383 % |
c |     87375 |   69385   250693 |   98370   87078   827534     9.5 | 25.452 % |
c |    131165 |   69317   250467 |  108207   55706   475850     8.5 | 25.509 % |
c |    196849 |   69228   250174 |  119027   36635   334298     9.1 | 25.584 % |
c |    295375 |   69130   249852 |  130930   41918   358029     8.5 | 25.665 % |
c |    443165 |   69095   249737 |  144023   73079   815567    11.2 | 25.693 % |
c |    664849 |   69095   249737 |  158425   56397   586353    10.4 | 25.693 % |
c |    997375 |   69074   249668 |  174268  122026  1369002    11.2 | 25.711 % |
c |   1496163 |   69029   249525 |  191695  169955  2208443    13.0 | 25.768 % |
#### 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.93 0.98 0.94 2/55 2167
Raw data (stat): 2167 (runsolver) R 2166 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546072552 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0001 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 2167
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 2406 0 0 0 993 5 0 0 25 0 1 0 546072552 12619776 2327 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3081 2327 603 41 0 3040 0
vsize: 12324
[startup+20.0006 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 2167
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 2645 0 0 0 1991 7 0 0 25 0 1 0 546072552 13623296 2566 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3326 2566 603 41 0 3285 0
vsize: 13304
[startup+30.0002 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 2936 0 0 0 2990 8 0 0 25 0 1 0 546072552 14827520 2857 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3620 2857 603 41 0 3579 0
vsize: 14480
[startup+40.0002 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 3189 0 0 0 3988 9 0 0 25 0 1 0 546072552 15908864 3110 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3884 3110 603 41 0 3843 0
vsize: 15536
[startup+50.001 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 3509 0 0 0 4988 10 0 0 25 0 1 0 546072552 17387520 3430 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3430 603 41 0 4204 0
vsize: 16980
[startup+60.0005 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 3779 0 0 0 5987 11 0 0 25 0 1 0 546072552 18464768 3700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4508 3700 603 41 0 4467 0
vsize: 18032
[startup+70.0006 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4042 0 0 0 6986 12 0 0 25 0 1 0 546072552 19529728 3963 4294967295 134512640 134672761 3221224544 3221223724 134553617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4768 3963 603 41 0 4727 0
vsize: 19072
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4269 0 0 0 7985 13 0 0 25 0 1 0 546072552 20336640 4190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4965 4190 603 41 0 4924 0
vsize: 19860
[startup+90.0009 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4339 0 0 0 8985 13 0 0 25 0 1 0 546072552 20602880 4260 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4260 603 41 0 4989 0
vsize: 20120
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4339 0 0 0 9985 13 0 0 25 0 1 0 546072552 20602880 4260 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4260 603 41 0 4989 0
vsize: 20120
[startup+110.001 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4339 0 0 0 10985 13 0 0 25 0 1 0 546072552 20602880 4260 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4260 603 41 0 4989 0
vsize: 20120
[startup+120.001 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4339 0 0 0 11985 13 0 0 25 0 1 0 546072552 20602880 4260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4260 603 41 0 4989 0
vsize: 20120
[startup+130.001 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4339 0 0 0 12985 13 0 0 25 0 1 0 546072552 20602880 4260 4294967295 134512640 134672761 3221224544 3221223696 134565143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4260 603 41 0 4989 0
vsize: 20120
[startup+140.001 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4491 0 0 0 13985 14 0 0 25 0 1 0 546072552 21278720 4412 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5195 4412 603 41 0 5154 0
vsize: 20780
[startup+150.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4783 0 0 0 14984 15 0 0 25 0 1 0 546072552 22491136 4704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5491 4704 603 41 0 5450 0
vsize: 21964
[startup+160.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4783 0 0 0 15984 15 0 0 25 0 1 0 546072552 22491136 4704 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5491 4704 603 41 0 5450 0
vsize: 21964
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4783 0 0 0 16984 15 0 0 25 0 1 0 546072552 22491136 4704 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5491 4704 603 41 0 5450 0
vsize: 21964
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4783 0 0 0 17984 15 0 0 25 0 1 0 546072552 22491136 4704 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5491 4704 603 41 0 5450 0
vsize: 21964
[startup+190.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4783 0 0 0 18984 15 0 0 25 0 1 0 546072552 22491136 4704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5491 4704 603 41 0 5450 0
vsize: 21964
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4783 0 0 0 19984 15 0 0 25 0 1 0 546072552 22491136 4704 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5491 4704 603 41 0 5450 0
vsize: 21964
[startup+210.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 4862 0 0 0 20984 16 0 0 25 0 1 0 546072552 22761472 4783 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 4783 603 41 0 5516 0
vsize: 22228
[startup+220.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5085 0 0 0 21984 16 0 0 25 0 1 0 546072552 23703552 5006 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5787 5006 603 41 0 5746 0
vsize: 23148
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5249 0 0 0 22983 17 0 0 25 0 1 0 546072552 24244224 5170 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5170 603 41 0 5878 0
vsize: 23676
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5249 0 0 0 23983 17 0 0 25 0 1 0 546072552 24244224 5170 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5170 603 41 0 5878 0
vsize: 23676
[startup+250.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5249 0 0 0 24983 17 0 0 25 0 1 0 546072552 24244224 5170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5170 603 41 0 5878 0
vsize: 23676
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5249 0 0 0 25983 17 0 0 25 0 1 0 546072552 24244224 5170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5170 603 41 0 5878 0
vsize: 23676
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5296 0 0 0 26983 17 0 0 25 0 1 0 546072552 24518656 5217 4294967295 134512640 134672761 3221224544 3221223712 134561124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5986 5217 603 41 0 5945 0
vsize: 23944
[startup+280.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5567 0 0 0 27983 18 0 0 25 0 1 0 546072552 25612288 5488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6253 5488 603 41 0 6212 0
vsize: 25012
[startup+290.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 5903 0 0 0 28982 19 0 0 25 0 1 0 546072552 27099136 5824 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6616 5824 603 41 0 6575 0
vsize: 26464
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6242 0 0 0 29981 20 0 0 25 0 1 0 546072552 28491776 6163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6956 6163 603 41 0 6915 0
vsize: 27824
[startup+310.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 30981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+320.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2169
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 31981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223708 134564508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+330.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 32981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 33981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 34981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 35981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+370.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 36981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+380.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 37981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+390.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 38981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+400.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6528 0 0 0 39981 21 0 0 25 0 1 0 546072552 30240768 6449 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6449 603 41 0 7342 0
vsize: 29532
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6535 0 0 0 40981 21 0 0 25 0 1 0 546072552 30240768 6456 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6456 603 41 0 7342 0
vsize: 29532
[startup+420.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 41982 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+430.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 42982 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 43982 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+450.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 44982 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+460.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 45982 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+470.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 46982 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+480.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 47983 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 48983 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6540 0 0 0 49983 21 0 0 25 0 1 0 546072552 30240768 6461 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6461 603 41 0 7342 0
vsize: 29532
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 50983 21 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+520.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 51983 21 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+530.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 52983 21 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 53982 21 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+550.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 54982 22 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+560.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 55982 22 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+570.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 56982 22 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+580.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 57982 22 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+590.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6541 0 0 0 58982 22 0 0 25 0 1 0 546072552 30240768 6462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6462 603 41 0 7342 0
vsize: 29532
[startup+600.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6691 0 0 0 59983 22 0 0 25 0 1 0 546072552 30777344 6612 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7514 6612 603 41 0 7473 0
vsize: 30056
[startup+610.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 6919 0 0 0 60982 23 0 0 25 0 1 0 546072552 31723520 6840 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7745 6840 603 41 0 7704 0
vsize: 30980
[startup+620.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2171
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 61981 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+630.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 62982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+640.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 63982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+650.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 64982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+660.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 65982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223668 134565986 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+670.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 66982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+680.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 67982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+690.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 68982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+700.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 69982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+710.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 70982 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+720.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 71983 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+730.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 72983 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134564695 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+740.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 73983 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+750.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 74983 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+760.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 75983 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+770.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 76984 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+780.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 77984 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+790.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 78984 24 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+800.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 79984 25 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+810.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7072 0 0 0 80984 25 0 0 25 0 1 0 546072552 32395264 6993 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7909 6993 603 41 0 7868 0
vsize: 31636
[startup+820.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7188 0 0 0 81984 25 0 0 25 0 1 0 546072552 32796672 7109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8007 7109 603 41 0 7966 0
vsize: 32028
[startup+830.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7491 0 0 0 82983 26 0 0 25 0 1 0 546072552 34009088 7412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8303 7412 603 41 0 8262 0
vsize: 33212
[startup+840.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 83982 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+850.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 84982 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+860.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 85982 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+870.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 86983 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223692 134565968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+880.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 87983 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+890.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 88983 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+900.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 89983 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+910.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 90983 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+920.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2173
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 91984 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+930.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 92984 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+940.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 93984 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+950.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 94984 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+960.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 95984 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+970.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 96984 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+980.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 97985 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+990.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 98985 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 99985 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 100985 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 101985 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223648 134555333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 102985 27 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 103985 28 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 104985 28 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 105985 28 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7743 0 0 0 106985 28 0 0 25 0 1 0 546072552 35086336 7664 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8566 7664 603 41 0 8525 0
vsize: 34264
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 107985 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 108985 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 109986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 110986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 111986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 112986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 113986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 114986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 115986 28 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223612 1075346562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7822 0 0 0 116986 29 0 0 25 0 1 0 546072552 35356672 7743 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8632 7743 603 41 0 8591 0
vsize: 34528
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 7853 0 0 0 117986 29 0 0 25 0 1 0 546072552 35491840 7774 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8665 7774 603 41 0 8624 0
vsize: 34660
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 8027 0 0 0 118984 30 0 0 25 0 1 0 546072552 36167680 7948 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8830 7948 603 41 0 8789 0
vsize: 35320
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 2175
Raw data (stat): 2167 (minisat+) R 2166 22929 22928 0 -1 0 8332 0 0 0 119983 31 0 0 25 0 1 0 546072552 37384192 8253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9127 8253 603 41 0 9086 0
vsize: 36508
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.94 1/55 2175
Raw data (stat): 2167 (minisat+) Z 2166 22929 22928 0 -1 12 8334 0 0 0 119983 32 0 0 25 0 1 0 546072552 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.05
CPU time (s): 1200.16
CPU user time (s): 1199.84
CPU system time (s): 0.328949
CPU usage (%): 100.01
Max. virtual memory (Kb): 36508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####