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/miplib3/normalized-mps-v2-13-7-pp08a.opb
MD5SUM	d14265fdf4e5a3ef733af1f15b884cbe
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6661373
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.02
Number of variables	3584
Total number of constraints	136
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	136
Minimum length of a constraint	21
Maximum length of a constraint	160
Trace number 14979

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 02:19:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18777 boxname=wulflinc28 idbench=1445 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  d14265fdf4e5a3ef733af1f15b884cbe  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 18777
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        699948 kB
Buffers:          4288 kB
Cached:         302492 kB
SwapCached:        104 kB
Active:          50464 kB
Inactive:       258660 kB
HighTotal:      131008 kB
HighFree:        40880 kB
LowTotal:       903652 kB
LowFree:        659068 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6052 kB
Slab:            19808 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:39:59 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 18777 7 1200.25 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 ---[ 199]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 190]---> BDD-cost:  158
c ---[ 188]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 178]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> BDD-cost:  158
c ---[ 140]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> BDD-cost:  154
c ---[  92]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  80]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  78]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   24
c ---[  62]---> BDD-cost:   24
c ---[  61]---> BDD-cost:   24
c ---[  60]---> BDD-cost:   21
c ---[  59]---> BDD-cost:   21
c ---[  58]---> BDD-cost:   21
c ---[  57]---> BDD-cost:   21
c ---[  56]---> BDD-cost:   23
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   19
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   19
c ---[  50]---> BDD-cost:   19
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   24
c ---[  46]---> BDD-cost:   24
c ---[  45]---> BDD-cost:   24
c ---[  44]---> BDD-cost:   21
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   21
c ---[  41]---> BDD-cost:   21
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   24
c ---[  38]---> BDD-cost:   24
c ---[  37]---> BDD-cost:   24
c ---[  36]---> BDD-cost:   21
c ---[  35]---> BDD-cost:   21
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:   21
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   18
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   18
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:   24
c ---[  22]---> BDD-cost:   24
c ---[  21]---> BDD-cost:   24
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   21
c ---[  16]---> BDD-cost:   21
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   19
c ---[  11]---> BDD-cost:   19
c ---[  10]---> BDD-cost:   19
c ---[   9]---> BDD-cost:   19
c ---[   8]---> BDD-cost:   19
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   19
c ---[   5]---> BDD-cost:   19
c ---[   4]---> BDD-cost:   19
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  192439   454988 |   64146       0        0     nan |  0.000 % |
c |       100 |  192239   454543 |   70560      73      246     3.4 |  5.672 % |
c |       250 |  192206   454471 |   77616     216      748     3.5 |  5.687 % |
c |       475 |  192016   454049 |   85378     412     1679     4.1 |  5.767 % |
c |       812 |  191856   453691 |   93916     721     3004     4.2 |  5.829 % |
c |      1319 |  191699   453343 |  103307    1205     7766     6.4 |  5.895 % |
c |      2079 |  191487   452868 |  113638    1929    14801     7.7 |  5.980 % |
c |      3219 |  191290   452428 |  125002    3045    26101     8.6 |  6.059 % |
c |      4927 |  191115   452036 |  137502    4729    52510    11.1 |  6.130 % |
c |      7490 |  190810   451355 |  151252    7247    81997    11.3 |  6.249 % |
c |     11334 |  189963   449458 |  166378   10976   116451    10.6 |  6.584 % |
c |     17100 |  189884   449279 |  183016   16736   248554    14.9 |  6.614 % |
c |     25749 |  189706   448881 |  201317   25359   431867    17.0 |  6.685 % |
c |     38724 |  189201   447754 |  221449   38259   749831    19.6 |  6.890 % |
c |     58187 |  188976   447252 |  243594   57689  1288213    22.3 |  6.979 % |
c |     87379 |  187270   443439 |  267953   86663  1918714    22.1 |  7.664 % |
c |    131168 |  186149   440936 |  294749  130304  3171694    24.3 |  8.119 % |
c |    196855 |  183362   434691 |  324224  195633  4851184    24.8 |  9.223 % |
c |    295384 |  182771   433365 |  356646  294057  7348160    25.0 |  9.461 % |
#### 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.90 0.94 0.90 2/54 14821
Raw data (stat): 14821 (runsolver) R 14820 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541434431 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 6133 0 0 0 982 17 0 0 25 0 1 0 541434431 30937088 5968 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7553 5968 603 41 0 7512 0
vsize: 30212
[startup+20.0006 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 6344 0 0 0 1981 18 0 0 25 0 1 0 541434431 31748096 6179 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7751 6179 603 41 0 7710 0
vsize: 31004
[startup+30.0013 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 6779 0 0 0 2979 20 0 0 25 0 1 0 541434431 33525760 6614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8185 6614 603 41 0 8144 0
vsize: 32740
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 7114 0 0 0 3977 21 0 0 25 0 1 0 541434431 35000320 6949 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8545 6949 603 41 0 8504 0
vsize: 34180
[startup+50.0017 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 7448 0 0 0 4977 22 0 0 25 0 1 0 541434431 36343808 7283 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8873 7283 603 41 0 8832 0
vsize: 35492
[startup+60.0014 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 7836 0 0 0 5975 24 0 0 25 0 1 0 541434431 37957632 7671 4294967295 134512640 134672761 3221224624 3221223772 134566158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9267 7671 603 41 0 9226 0
vsize: 37068
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8096 0 0 0 6974 25 0 0 25 0 1 0 541434431 38907904 7931 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9499 7931 603 41 0 9458 0
vsize: 37996
[startup+80.0032 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8272 0 0 0 7974 25 0 0 25 0 1 0 541434431 39976960 8107 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 8107 603 41 0 9719 0
vsize: 39040
[startup+90.0024 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8388 0 0 0 8973 26 0 0 25 0 1 0 541434431 40374272 8223 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9857 8223 603 41 0 9816 0
vsize: 39428
[startup+100.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8482 0 0 0 9973 27 0 0 25 0 1 0 541434431 40775680 8317 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9955 8317 603 41 0 9914 0
vsize: 39820
[startup+110.003 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8714 0 0 0 10972 28 0 0 25 0 1 0 541434431 41713664 8549 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10184 8549 603 41 0 10143 0
vsize: 40736
[startup+120.004 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8960 0 0 0 11971 29 0 0 25 0 1 0 541434431 42651648 8795 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10413 8795 603 41 0 10372 0
vsize: 41652
[startup+130.005 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9194 0 0 0 12970 30 0 0 25 0 1 0 541434431 43610112 9029 4294967295 134512640 134672761 3221224624 3221223776 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10647 9029 603 41 0 10606 0
vsize: 42588
[startup+140.004 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9322 0 0 0 13969 31 0 0 25 0 1 0 541434431 44158976 9157 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 9157 603 41 0 10740 0
vsize: 43124
[startup+150.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9492 0 0 0 14969 32 0 0 25 0 1 0 541434431 44830720 9327 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10945 9327 603 41 0 10904 0
vsize: 43780
[startup+160.005 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9591 0 0 0 15968 32 0 0 25 0 1 0 541434431 45236224 9426 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11044 9426 603 41 0 11003 0
vsize: 44176
[startup+170.005 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9839 0 0 0 16967 34 0 0 25 0 1 0 541434431 46170112 9674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11272 9674 603 41 0 11231 0
vsize: 45088
[startup+180.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10157 0 0 0 17966 35 0 0 25 0 1 0 541434431 47513600 9992 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11600 9992 603 41 0 11559 0
vsize: 46400
[startup+190.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10389 0 0 0 18965 36 0 0 25 0 1 0 541434431 48345088 10224 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11803 10224 603 41 0 11762 0
vsize: 47212
[startup+200.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10581 0 0 0 19964 37 0 0 25 0 1 0 541434431 49696768 10416 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12133 10416 603 41 0 12092 0
vsize: 48532
[startup+210.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10618 0 0 0 20965 37 0 0 25 0 1 0 541434431 49827840 10453 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12165 10453 603 41 0 12124 0
vsize: 48660
[startup+220.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10669 0 0 0 21965 37 0 0 25 0 1 0 541434431 49987584 10504 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12204 10504 603 41 0 12163 0
vsize: 48816
[startup+230.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10782 0 0 0 22964 37 0 0 25 0 1 0 541434431 50524160 10617 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12335 10617 603 41 0 12294 0
vsize: 49340
[startup+240.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10870 0 0 0 23964 37 0 0 25 0 1 0 541434431 50814976 10705 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12406 10705 603 41 0 12365 0
vsize: 49624
[startup+250.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11055 0 0 0 24964 38 0 0 25 0 1 0 541434431 51634176 10890 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12606 10890 603 41 0 12565 0
vsize: 50424
[startup+260.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11255 0 0 0 25964 38 0 0 25 0 1 0 541434431 52441088 11090 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11090 603 41 0 12762 0
vsize: 51212
[startup+270.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11365 0 0 0 26964 39 0 0 25 0 1 0 541434431 52862976 11200 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12906 11200 603 41 0 12865 0
vsize: 51624
[startup+280.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11422 0 0 0 27963 39 0 0 25 0 1 0 541434431 53133312 11257 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12972 11257 603 41 0 12931 0
vsize: 51888
[startup+290.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11534 0 0 0 28964 39 0 0 25 0 1 0 541434431 53665792 11369 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13102 11369 603 41 0 13061 0
vsize: 52408
[startup+300.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11704 0 0 0 29963 40 0 0 25 0 1 0 541434431 54226944 11539 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13239 11539 603 41 0 13198 0
vsize: 52956
[startup+310.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11866 0 0 0 30963 40 0 0 25 0 1 0 541434431 55058432 11701 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13442 11701 603 41 0 13401 0
vsize: 53768
[startup+320.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11927 0 0 0 31963 40 0 0 25 0 1 0 541434431 55328768 11762 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13508 11762 603 41 0 13467 0
vsize: 54032
[startup+330.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12090 0 0 0 32963 41 0 0 25 0 1 0 541434431 56008704 11925 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13674 11925 603 41 0 13633 0
vsize: 54696
[startup+340.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12116 0 0 0 33963 41 0 0 25 0 1 0 541434431 56008704 11951 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13674 11951 603 41 0 13633 0
vsize: 54696
[startup+350.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12201 0 0 0 34963 41 0 0 25 0 1 0 541434431 56414208 12036 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13773 12036 603 41 0 13732 0
vsize: 55092
[startup+360.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12340 0 0 0 35963 41 0 0 25 0 1 0 541434431 56971264 12175 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13909 12175 603 41 0 13868 0
vsize: 55636
[startup+370.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12413 0 0 0 36963 42 0 0 25 0 1 0 541434431 57368576 12248 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14006 12248 603 41 0 13965 0
vsize: 56024
[startup+380.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12456 0 0 0 37963 42 0 0 25 0 1 0 541434431 57507840 12291 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14040 12291 603 41 0 13999 0
vsize: 56160
[startup+390.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12544 0 0 0 38963 42 0 0 25 0 1 0 541434431 57815040 12379 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14115 12379 603 41 0 14074 0
vsize: 56460
[startup+400.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12600 0 0 0 39963 42 0 0 25 0 1 0 541434431 58093568 12435 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14183 12435 603 41 0 14142 0
vsize: 56732
[startup+410.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12636 0 0 0 40963 42 0 0 25 0 1 0 541434431 58228736 12471 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14216 12471 603 41 0 14175 0
vsize: 56864
[startup+420.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12703 0 0 0 41963 42 0 0 25 0 1 0 541434431 58499072 12538 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14282 12538 603 41 0 14241 0
vsize: 57128
[startup+430.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12883 0 0 0 42963 43 0 0 25 0 1 0 541434431 59166720 12718 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14445 12718 603 41 0 14404 0
vsize: 57780
[startup+440.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12973 0 0 0 43962 43 0 0 25 0 1 0 541434431 59588608 12808 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14548 12808 603 41 0 14507 0
vsize: 58192
[startup+450.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13024 0 0 0 44962 43 0 0 25 0 1 0 541434431 59719680 12859 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14580 12859 603 41 0 14539 0
vsize: 58320
[startup+460.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13125 0 0 0 45962 43 0 0 25 0 1 0 541434431 60153856 12960 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14686 12960 603 41 0 14645 0
vsize: 58744
[startup+470.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13285 0 0 0 46962 44 0 0 25 0 1 0 541434431 60829696 13120 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14851 13120 603 41 0 14810 0
vsize: 59404
[startup+480.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13418 0 0 0 47962 44 0 0 25 0 1 0 541434431 61227008 13253 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14948 13253 603 41 0 14907 0
vsize: 59792
[startup+490.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13473 0 0 0 48961 45 0 0 25 0 1 0 541434431 61497344 13308 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15014 13308 603 41 0 14973 0
vsize: 60056
[startup+500.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13529 0 0 0 49962 45 0 0 25 0 1 0 541434431 61632512 13364 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15047 13364 603 41 0 15006 0
vsize: 60188
[startup+510.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13612 0 0 0 50962 45 0 0 25 0 1 0 541434431 62033920 13447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15145 13447 603 41 0 15104 0
vsize: 60580
[startup+520.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13713 0 0 0 51962 45 0 0 25 0 1 0 541434431 62435328 13548 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15243 13548 603 41 0 15202 0
vsize: 60972
[startup+530.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13796 0 0 0 52962 45 0 0 25 0 1 0 541434431 62701568 13631 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15308 13631 603 41 0 15267 0
vsize: 61232
[startup+540.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13870 0 0 0 53962 46 0 0 25 0 1 0 541434431 62963712 13705 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15372 13705 603 41 0 15331 0
vsize: 61488
[startup+550.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13910 0 0 0 54962 46 0 0 25 0 1 0 541434431 63234048 13745 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15438 13745 603 41 0 15397 0
vsize: 61752
[startup+560.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13968 0 0 0 55962 46 0 0 25 0 1 0 541434431 63365120 13803 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15470 13803 603 41 0 15429 0
vsize: 61880
[startup+570.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14064 0 0 0 56962 46 0 0 25 0 1 0 541434431 63770624 13899 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15569 13899 603 41 0 15528 0
vsize: 62276
[startup+580.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14136 0 0 0 57962 46 0 0 25 0 1 0 541434431 64102400 13971 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15650 13971 603 41 0 15609 0
vsize: 62600
[startup+590.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14284 0 0 0 58962 47 0 0 25 0 1 0 541434431 64655360 14119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15785 14119 603 41 0 15744 0
vsize: 63140
[startup+600.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14379 0 0 0 59962 47 0 0 25 0 1 0 541434431 65064960 14214 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15885 14214 603 41 0 15844 0
vsize: 63540
[startup+610.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14490 0 0 0 60961 47 0 0 25 0 1 0 541434431 65470464 14325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15984 14325 603 41 0 15943 0
vsize: 63936
[startup+620.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14602 0 0 0 61961 48 0 0 25 0 1 0 541434431 65871872 14437 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16082 14437 603 41 0 16041 0
vsize: 64328
[startup+630.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14772 0 0 0 62961 48 0 0 25 0 1 0 541434431 66547712 14607 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16247 14607 603 41 0 16206 0
vsize: 64988
[startup+640.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14902 0 0 0 63961 49 0 0 25 0 1 0 541434431 67084288 14737 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16378 14737 603 41 0 16337 0
vsize: 65512
[startup+650.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14980 0 0 0 64961 49 0 0 25 0 1 0 541434431 67485696 14815 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16476 14815 603 41 0 16435 0
vsize: 65904
[startup+660.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15023 0 0 0 65961 49 0 0 25 0 1 0 541434431 67620864 14858 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16509 14858 603 41 0 16468 0
vsize: 66036
[startup+670.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15127 0 0 0 66961 49 0 0 25 0 1 0 541434431 69070848 14962 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16863 14962 603 41 0 16822 0
vsize: 67452
[startup+680.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15205 0 0 0 67961 49 0 0 25 0 1 0 541434431 69337088 15040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16928 15040 603 41 0 16887 0
vsize: 67712
[startup+690.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15317 0 0 0 68961 50 0 0 25 0 1 0 541434431 69763072 15152 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17032 15152 603 41 0 16991 0
vsize: 68128
[startup+700.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15407 0 0 0 69961 50 0 0 25 0 1 0 541434431 70184960 15242 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17135 15242 603 41 0 17094 0
vsize: 68540
[startup+710.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15503 0 0 0 70961 50 0 0 25 0 1 0 541434431 70590464 15338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17234 15338 603 41 0 17193 0
vsize: 68936
[startup+720.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15588 0 0 0 71960 51 0 0 25 0 1 0 541434431 70856704 15423 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17299 15423 603 41 0 17258 0
vsize: 69196
[startup+730.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15659 0 0 0 72960 51 0 0 25 0 1 0 541434431 71127040 15494 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17365 15494 603 41 0 17324 0
vsize: 69460
[startup+740.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15739 0 0 0 73960 51 0 0 25 0 1 0 541434431 71532544 15574 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17464 15574 603 41 0 17423 0
vsize: 69856
[startup+750.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15827 0 0 0 74960 51 0 0 25 0 1 0 541434431 71819264 15662 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17534 15662 603 41 0 17493 0
vsize: 70136
[startup+760.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15926 0 0 0 75960 51 0 0 25 0 1 0 541434431 72282112 15761 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17647 15761 603 41 0 17606 0
vsize: 70588
[startup+770.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16030 0 0 0 76960 52 0 0 25 0 1 0 541434431 72814592 15865 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17777 15865 603 41 0 17736 0
vsize: 71108
[startup+780.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16142 0 0 0 77960 52 0 0 25 0 1 0 541434431 73216000 15977 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17875 15977 603 41 0 17834 0
vsize: 71500
[startup+790.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16269 0 0 0 78960 52 0 0 25 0 1 0 541434431 73744384 16104 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18004 16104 603 41 0 17963 0
vsize: 72016
[startup+800.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16332 0 0 0 79959 53 0 0 25 0 1 0 541434431 73879552 16167 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18037 16167 603 41 0 17996 0
vsize: 72148
[startup+810.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16463 0 0 0 80959 53 0 0 25 0 1 0 541434431 74416128 16298 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18168 16298 603 41 0 18127 0
vsize: 72672
[startup+820.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16536 0 0 0 81959 53 0 0 25 0 1 0 541434431 74682368 16371 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18233 16371 603 41 0 18192 0
vsize: 72932
[startup+830.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16603 0 0 0 82959 53 0 0 25 0 1 0 541434431 74948608 16438 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18298 16438 603 41 0 18257 0
vsize: 73192
[startup+840.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16692 0 0 0 83958 54 0 0 25 0 1 0 541434431 75345920 16527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18395 16527 603 41 0 18354 0
vsize: 73580
[startup+850.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16783 0 0 0 84958 54 0 0 25 0 1 0 541434431 75747328 16618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18493 16618 603 41 0 18452 0
vsize: 73972
[startup+860.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16912 0 0 0 85958 54 0 0 25 0 1 0 541434431 76279808 16747 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18623 16747 603 41 0 18582 0
vsize: 74492
[startup+870.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17002 0 0 0 86958 55 0 0 25 0 1 0 541434431 76546048 16837 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18688 16837 603 41 0 18647 0
vsize: 74752
[startup+880.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17079 0 0 0 87959 55 0 0 25 0 1 0 541434431 76951552 16914 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18787 16914 603 41 0 18746 0
vsize: 75148
[startup+890.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17152 0 0 0 88959 55 0 0 25 0 1 0 541434431 77217792 16987 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18852 16987 603 41 0 18811 0
vsize: 75408
[startup+900.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17223 0 0 0 89958 55 0 0 25 0 1 0 541434431 77479936 17058 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18916 17058 603 41 0 18875 0
vsize: 75664
[startup+910.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17394 0 0 0 90957 56 0 0 25 0 1 0 541434431 78151680 17229 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19080 17229 603 41 0 19039 0
vsize: 76320
[startup+920.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17456 0 0 0 91958 56 0 0 25 0 1 0 541434431 78422016 17291 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19146 17291 603 41 0 19105 0
vsize: 76584
[startup+930.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17547 0 0 0 92958 56 0 0 25 0 1 0 541434431 78807040 17382 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19240 17382 603 41 0 19199 0
vsize: 76960
[startup+940.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17631 0 0 0 93958 57 0 0 25 0 1 0 541434431 79077376 17466 4294967295 134512640 134672761 3221224624 3221223776 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19306 17466 603 41 0 19265 0
vsize: 77224
[startup+950.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17730 0 0 0 94958 57 0 0 25 0 1 0 541434431 79478784 17565 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19404 17565 603 41 0 19363 0
vsize: 77616
[startup+960.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17834 0 0 0 95958 57 0 0 25 0 1 0 541434431 80031744 17669 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19539 17669 603 41 0 19498 0
vsize: 78156
[startup+970.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17941 0 0 0 96958 57 0 0 25 0 1 0 541434431 80535552 17776 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19662 17776 603 41 0 19621 0
vsize: 78648
[startup+980.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18049 0 0 0 97957 58 0 0 25 0 1 0 541434431 80830464 17884 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19734 17884 603 41 0 19693 0
vsize: 78936
[startup+990.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18165 0 0 0 98957 58 0 0 25 0 1 0 541434431 81399808 18000 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19873 18000 603 41 0 19832 0
vsize: 79492
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18255 0 0 0 99957 58 0 0 25 0 1 0 541434431 81797120 18090 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19970 18090 603 41 0 19929 0
vsize: 79880
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18344 0 0 0 100957 58 0 0 25 0 1 0 541434431 82063360 18179 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20035 18179 603 41 0 19994 0
vsize: 80140
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18461 0 0 0 101957 59 0 0 25 0 1 0 541434431 82677760 18296 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20185 18296 603 41 0 20144 0
vsize: 80740
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18572 0 0 0 102957 59 0 0 25 0 1 0 541434431 83083264 18407 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20284 18407 603 41 0 20243 0
vsize: 81136
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18694 0 0 0 103957 60 0 0 25 0 1 0 541434431 83656704 18529 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20424 18529 603 41 0 20383 0
vsize: 81696
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18783 0 0 0 104956 60 0 0 25 0 1 0 541434431 83927040 18618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20490 18618 603 41 0 20449 0
vsize: 81960
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18912 0 0 0 105956 60 0 0 25 0 1 0 541434431 84463616 18747 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20621 18747 603 41 0 20580 0
vsize: 82484
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19019 0 0 0 106956 61 0 0 25 0 1 0 541434431 84869120 18854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20720 18854 603 41 0 20679 0
vsize: 82880
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19150 0 0 0 107956 61 0 0 25 0 1 0 541434431 85528576 18985 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20881 18985 603 41 0 20840 0
vsize: 83524
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19256 0 0 0 108955 62 0 0 25 0 1 0 541434431 85946368 19091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20983 19091 603 41 0 20942 0
vsize: 83932
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 109956 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 110956 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 111956 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 112957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 113957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 114957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223760 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 115957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 116958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 117958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 118958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 14821
Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 119958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21015 19141 603 41 0 20974 0
vsize: 84060
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 14821
Raw data (stat): 14821 (minisat+) Z 14820 10614 10613 0 -1 12 19308 0 0 0 119958 66 0 0 25 0 1 0 541434431 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.07
CPU time (s): 1200.25
CPU user time (s): 1199.59
CPU system time (s): 0.660899
CPU usage (%): 100.015
Max. virtual memory (Kb): 84060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####