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 18481

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        760824 kB
Buffers:         24684 kB
Cached:         226848 kB
SwapCached:          0 kB
Active:          94888 kB
Inactive:       159492 kB
HighTotal:      131008 kB
HighFree:        36596 kB
LowTotal:       903652 kB
LowFree:        724228 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            13856 kB
Committed_AS:    63556 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:34:44 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 17919 7 1200.34 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]---> BDD-cost:  158
c ---[ 196]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   18
c ---[ 188]---> BDD-cost:   18
c ---[ 187]---> BDD-cost:   18
c ---[ 186]---> BDD-cost:   18
c ---[ 184]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   18
c ---[ 180]---> BDD-cost:   24
c ---[ 179]---> BDD-cost:   24
c ---[ 178]---> BDD-cost:   24
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   21
c ---[ 175]---> BDD-cost:   21
c ---[ 174]---> BDD-cost:   21
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 ---[ 171]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:   19
c ---[ 169]---> BDD-cost:   19
c ---[ 168]---> BDD-cost:   19
c ---[ 167]---> BDD-cost:   19
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   19
c ---[ 163]---> BDD-cost:   19
c ---[ 162]---> BDD-cost:   19
c ---[ 160]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 151]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> BDD-cost:  158
c ---[ 125]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> BDD-cost:  154
c ---[  73]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> BDD-cost:   24
c ---[  29]---> BDD-cost:   24
c ---[  28]---> BDD-cost:   24
c ---[  27]---> BDD-cost:   21
c ---[  26]---> BDD-cost:   21
c ---[  25]---> BDD-cost:   21
c ---[  24]---> BDD-cost:   21
c ---[  22]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   19
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   19
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   24
c ---[  10]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   24
c ---[   8]---> BDD-cost:   24
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   21
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   21
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   24
c ---[   1]---> BDD-cost:   24
c ---[   0]---> BDD-cost:   24
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 |  192427   454964 |   70560      94      279     3.0 |  5.598 % |
c |       250 |  192396   454896 |   77616     238      717     3.0 |  5.612 % |
c |       477 |  192171   454395 |   85378     437     1322     3.0 |  5.704 % |
c |       814 |  192089   454214 |   93916     762     2351     3.1 |  5.738 % |
c |      1320 |  191553   453019 |  103307    1195     3761     3.1 |  5.956 % |
c |      2079 |  191063   451931 |  113638    1885     6010     3.2 |  6.157 % |
c |      3218 |  190719   451160 |  125002    2975    10009     3.4 |  6.292 % |
c |      4927 |  190066   449707 |  137502    4604    16601     3.6 |  6.562 % |
c |      7491 |  188869   447024 |  151252    7012    26452     3.8 |  7.036 % |
c |     11335 |  187408   443757 |  166378   10626    42542     4.0 |  7.620 % |
c |     17102 |  186642   442041 |  183016   16293    73482     4.5 |  7.920 % |
c |     25751 |  185392   439241 |  201317   24799   121776     4.9 |  8.418 % |
c |     38726 |  184260   436704 |  221449   37635   211813     5.6 |  8.871 % |
c |     58187 |  183275   434500 |  243594   56905   382699     6.7 |  9.271 % |
c |     87379 |  182889   433634 |  267953   86050   660466     7.7 |  9.426 % |
c |    131168 |  182665   433132 |  294749  129797  1237694     9.5 |  9.522 % |
c |    196854 |  182378   432490 |  324224  195451  2455550    12.6 |  9.636 % |
c |    295381 |  182332   432387 |  356646  293971  5294629    18.0 |  9.656 % |
c |    443170 |  182242   432188 |  392311  113343  2518668    22.2 |  9.700 % |
#### 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.68 0.92 0.90 2/54 10331
Raw data (stat): 10331 (runsolver) R 10330 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487857404 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.73 0.92 0.90 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6074 0 0 0 984 14 0 0 25 0 1 0 487857404 30642176 5898 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7481 5898 603 41 0 7440 0
vsize: 29924
[startup+20.0012 s]
Raw data (loadavg): 0.77 0.92 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6112 0 0 0 1983 14 0 0 25 0 1 0 487857404 30777344 5936 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7514 5936 603 41 0 7473 0
vsize: 30056
[startup+30.0026 s]
Raw data (loadavg): 0.80 0.93 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6146 0 0 0 2983 14 0 0 25 0 1 0 487857404 30912512 5970 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7547 5970 603 41 0 7506 0
vsize: 30188
[startup+40.003 s]
Raw data (loadavg): 0.83 0.93 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6171 0 0 0 3983 14 0 0 25 0 1 0 487857404 30912512 5995 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7547 5995 603 41 0 7506 0
vsize: 30188
[startup+50.0034 s]
Raw data (loadavg): 0.86 0.93 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6206 0 0 0 4983 15 0 0 25 0 1 0 487857404 31047680 6030 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7580 6030 603 41 0 7539 0
vsize: 30320
[startup+60.0035 s]
Raw data (loadavg): 0.88 0.93 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6256 0 0 0 5983 15 0 0 25 0 1 0 487857404 31408128 6080 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7668 6080 603 41 0 7627 0
vsize: 30672
[startup+70.0033 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6272 0 0 0 6983 15 0 0 25 0 1 0 487857404 31408128 6096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7668 6096 603 41 0 7627 0
vsize: 30672
[startup+80.0038 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6304 0 0 0 7983 15 0 0 25 0 1 0 487857404 31543296 6128 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7701 6128 603 41 0 7660 0
vsize: 30804
[startup+90.0053 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6341 0 0 0 8983 15 0 0 25 0 1 0 487857404 31678464 6165 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7734 6165 603 41 0 7693 0
vsize: 30936
[startup+100.006 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6379 0 0 0 9983 15 0 0 25 0 1 0 487857404 31813632 6203 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7767 6203 603 41 0 7726 0
vsize: 31068
[startup+110.006 s]
Raw data (loadavg): 1.03 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6426 0 0 0 10983 15 0 0 25 0 1 0 487857404 31944704 6250 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7799 6250 603 41 0 7758 0
vsize: 31196
[startup+120.006 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6477 0 0 0 11983 15 0 0 25 0 1 0 487857404 32342016 6301 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7896 6301 603 41 0 7855 0
vsize: 31584
[startup+130.007 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6500 0 0 0 12984 15 0 0 25 0 1 0 487857404 32342016 6324 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7896 6324 603 41 0 7855 0
vsize: 31584
[startup+140.006 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6537 0 0 0 13983 16 0 0 25 0 1 0 487857404 32477184 6361 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7929 6361 603 41 0 7888 0
vsize: 31716
[startup+150.007 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6577 0 0 0 14983 16 0 0 25 0 1 0 487857404 32612352 6401 4294967295 134512640 134672761 3221224624 3221223792 134564668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7962 6401 603 41 0 7921 0
vsize: 31848
[startup+160.007 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6624 0 0 0 15983 16 0 0 25 0 1 0 487857404 32882688 6448 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8028 6448 603 41 0 7987 0
vsize: 32112
[startup+170.007 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6673 0 0 0 16983 16 0 0 25 0 1 0 487857404 33013760 6497 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 6497 603 41 0 8019 0
vsize: 32240
[startup+180.008 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6724 0 0 0 17983 16 0 0 25 0 1 0 487857404 33280000 6548 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8125 6548 603 41 0 8084 0
vsize: 32500
[startup+190.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6793 0 0 0 18983 17 0 0 25 0 1 0 487857404 33550336 6617 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8191 6617 603 41 0 8150 0
vsize: 32764
[startup+200.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6841 0 0 0 19983 17 0 0 25 0 1 0 487857404 33685504 6665 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8224 6665 603 41 0 8183 0
vsize: 32896
[startup+210.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6886 0 0 0 20984 17 0 0 25 0 1 0 487857404 33816576 6710 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8256 6710 603 41 0 8215 0
vsize: 33024
[startup+220.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6933 0 0 0 21983 17 0 0 25 0 1 0 487857404 34082816 6757 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8321 6757 603 41 0 8280 0
vsize: 33284
[startup+230.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 6989 0 0 0 22983 18 0 0 25 0 1 0 487857404 34480128 6813 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8418 6813 603 41 0 8377 0
vsize: 33672
[startup+240.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7055 0 0 0 23983 18 0 0 25 0 1 0 487857404 34750464 6879 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8484 6879 603 41 0 8443 0
vsize: 33936
[startup+250.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7123 0 0 0 24983 18 0 0 25 0 1 0 487857404 35020800 6947 4294967295 134512640 134672761 3221224624 3221223632 1075349729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8550 6947 603 41 0 8509 0
vsize: 34200
[startup+260.011 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7176 0 0 0 25983 19 0 0 25 0 1 0 487857404 35155968 7000 4294967295 134512640 134672761 3221224624 3221223760 134560694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8583 7000 603 41 0 8542 0
vsize: 34332
[startup+270.011 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7219 0 0 0 26983 19 0 0 25 0 1 0 487857404 35422208 7043 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8648 7043 603 41 0 8607 0
vsize: 34592
[startup+280.012 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7269 0 0 0 27983 19 0 0 25 0 1 0 487857404 35557376 7093 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8681 7093 603 41 0 8640 0
vsize: 34724
[startup+290.011 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7320 0 0 0 28983 19 0 0 25 0 1 0 487857404 35823616 7144 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8746 7144 603 41 0 8705 0
vsize: 34984
[startup+300.011 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7366 0 0 0 29983 19 0 0 25 0 1 0 487857404 35958784 7190 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8779 7190 603 41 0 8738 0
vsize: 35116
[startup+310.012 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7443 0 0 0 30983 20 0 0 25 0 1 0 487857404 36229120 7267 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8845 7267 603 41 0 8804 0
vsize: 35380
[startup+320.011 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7562 0 0 0 31983 20 0 0 25 0 1 0 487857404 36761600 7386 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8975 7386 603 41 0 8934 0
vsize: 35900
[startup+330.011 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7646 0 0 0 32982 20 0 0 25 0 1 0 487857404 37031936 7470 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9041 7470 603 41 0 9000 0
vsize: 36164
[startup+340.012 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7702 0 0 0 33983 20 0 0 25 0 1 0 487857404 37302272 7526 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9107 7526 603 41 0 9066 0
vsize: 36428
[startup+350.013 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7774 0 0 0 34982 21 0 0 25 0 1 0 487857404 37564416 7598 4294967295 134512640 134672761 3221224624 3221223748 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9171 7598 603 41 0 9130 0
vsize: 36684
[startup+360.013 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7828 0 0 0 35982 21 0 0 25 0 1 0 487857404 37834752 7652 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9237 7652 603 41 0 9196 0
vsize: 36948
[startup+370.013 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7879 0 0 0 36982 21 0 0 25 0 1 0 487857404 37969920 7703 4294967295 134512640 134672761 3221224624 3221223776 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9270 7703 603 41 0 9229 0
vsize: 37080
[startup+380.014 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7932 0 0 0 37982 22 0 0 25 0 1 0 487857404 38232064 7756 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9334 7756 603 41 0 9293 0
vsize: 37336
[startup+390.014 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 7995 0 0 0 38982 22 0 0 25 0 1 0 487857404 38367232 7819 4294967295 134512640 134672761 3221224624 3221223792 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9367 7819 603 41 0 9326 0
vsize: 37468
[startup+400.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8051 0 0 0 39982 22 0 0 25 0 1 0 487857404 38633472 7875 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9432 7875 603 41 0 9391 0
vsize: 37728
[startup+410.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8106 0 0 0 40982 22 0 0 25 0 1 0 487857404 38903808 7930 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9498 7930 603 41 0 9457 0
vsize: 37992
[startup+420.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8169 0 0 0 41982 23 0 0 25 0 1 0 487857404 39034880 7993 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9530 7993 603 41 0 9489 0
vsize: 38120
[startup+430.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8237 0 0 0 42982 23 0 0 25 0 1 0 487857404 39432192 8061 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9627 8061 603 41 0 9586 0
vsize: 38508
[startup+440.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8304 0 0 0 43982 23 0 0 25 0 1 0 487857404 39567360 8128 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9660 8128 603 41 0 9619 0
vsize: 38640
[startup+450.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8381 0 0 0 44981 24 0 0 25 0 1 0 487857404 39972864 8205 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9759 8205 603 41 0 9718 0
vsize: 39036
[startup+460.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8472 0 0 0 45981 24 0 0 25 0 1 0 487857404 40763392 8296 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9952 8296 603 41 0 9911 0
vsize: 39808
[startup+470.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8559 0 0 0 46981 24 0 0 25 0 1 0 487857404 41160704 8383 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10049 8383 603 41 0 10008 0
vsize: 40196
[startup+480.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8631 0 0 0 47981 24 0 0 25 0 1 0 487857404 41431040 8455 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10115 8455 603 41 0 10074 0
vsize: 40460
[startup+490.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8754 0 0 0 48981 25 0 0 25 0 1 0 487857404 41963520 8578 4294967295 134512640 134672761 3221224624 3221223748 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10245 8578 603 41 0 10204 0
vsize: 40980
[startup+500.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8874 0 0 0 49981 25 0 0 25 0 1 0 487857404 42360832 8698 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10342 8698 603 41 0 10301 0
vsize: 41368
[startup+510.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 8984 0 0 0 50980 26 0 0 25 0 1 0 487857404 42897408 8808 4294967295 134512640 134672761 3221224624 3221223760 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10473 8808 603 41 0 10432 0
vsize: 41892
[startup+520.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9131 0 0 0 51980 26 0 0 25 0 1 0 487857404 43433984 8955 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10604 8955 603 41 0 10563 0
vsize: 42416
[startup+530.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9390 0 0 0 52980 27 0 0 25 0 1 0 487857404 44498944 9214 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10864 9214 603 41 0 10823 0
vsize: 43456
[startup+540.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9490 0 0 0 53979 27 0 0 25 0 1 0 487857404 44900352 9314 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10962 9314 603 41 0 10921 0
vsize: 43848
[startup+550.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9614 0 0 0 54979 28 0 0 25 0 1 0 487857404 45305856 9438 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11061 9438 603 41 0 11020 0
vsize: 44244
[startup+560.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9706 0 0 0 55978 29 0 0 25 0 1 0 487857404 45711360 9530 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 9530 603 41 0 11119 0
vsize: 44640
[startup+570.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9819 0 0 0 56978 29 0 0 25 0 1 0 487857404 46108672 9643 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11257 9643 603 41 0 11216 0
vsize: 45028
[startup+580.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 9885 0 0 0 57978 29 0 0 25 0 1 0 487857404 46374912 9709 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 9709 603 41 0 11281 0
vsize: 45288
[startup+590.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10009 0 0 0 58978 30 0 0 25 0 1 0 487857404 46907392 9833 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11452 9833 603 41 0 11411 0
vsize: 45808
[startup+600.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10095 0 0 0 59978 30 0 0 25 0 1 0 487857404 47177728 9919 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11518 9919 603 41 0 11477 0
vsize: 46072
[startup+610.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10191 0 0 0 60978 30 0 0 25 0 1 0 487857404 47583232 10015 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11617 10015 603 41 0 11576 0
vsize: 46468
[startup+620.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10302 0 0 0 61978 30 0 0 25 0 1 0 487857404 48119808 10126 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11748 10126 603 41 0 11707 0
vsize: 46992
[startup+630.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10544 0 0 0 62977 31 0 0 25 0 1 0 487857404 49053696 10368 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11976 10368 603 41 0 11935 0
vsize: 47904
[startup+640.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10647 0 0 0 63976 32 0 0 25 0 1 0 487857404 49459200 10471 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 10471 603 41 0 12034 0
vsize: 48300
[startup+650.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10749 0 0 0 64976 32 0 0 25 0 1 0 487857404 49856512 10573 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 10573 603 41 0 12131 0
vsize: 48688
[startup+660.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10890 0 0 0 65975 33 0 0 25 0 1 0 487857404 50397184 10714 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12304 10714 603 41 0 12263 0
vsize: 49216
[startup+670.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 10979 0 0 0 66975 33 0 0 25 0 1 0 487857404 50798592 10803 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12402 10803 603 41 0 12361 0
vsize: 49608
[startup+680.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 11237 0 0 0 67975 34 0 0 25 0 1 0 487857404 51736576 11061 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12631 11061 603 41 0 12590 0
vsize: 50524
[startup+690.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 11403 0 0 0 68975 34 0 0 25 0 1 0 487857404 52412416 11227 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12796 11227 603 41 0 12755 0
vsize: 51184
[startup+700.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 11548 0 0 0 69975 34 0 0 25 0 1 0 487857404 53080064 11372 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 11372 603 41 0 12918 0
vsize: 51836
[startup+710.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 11636 0 0 0 70975 35 0 0 25 0 1 0 487857404 53350400 11460 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13025 11460 603 41 0 12984 0
vsize: 52100
[startup+720.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 11837 0 0 0 71974 35 0 0 25 0 1 0 487857404 54157312 11661 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13222 11661 603 41 0 13181 0
vsize: 52888
[startup+730.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 12031 0 0 0 72974 36 0 0 25 0 1 0 487857404 54960128 11855 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13418 11855 603 41 0 13377 0
vsize: 53672
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 12293 0 0 0 73973 37 0 0 25 0 1 0 487857404 56029184 12117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13679 12117 603 41 0 13638 0
vsize: 54716
[startup+750.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 12523 0 0 0 74973 37 0 0 25 0 1 0 487857404 56971264 12347 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13909 12347 603 41 0 13868 0
vsize: 55636
[startup+760.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 12614 0 0 0 75973 37 0 0 25 0 1 0 487857404 57241600 12438 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13975 12438 603 41 0 13934 0
vsize: 55900
[startup+770.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 12951 0 0 0 76972 39 0 0 25 0 1 0 487857404 59629568 12775 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14558 12775 603 41 0 14517 0
vsize: 58232
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 13153 0 0 0 77971 40 0 0 25 0 1 0 487857404 60436480 12977 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14755 12977 603 41 0 14714 0
vsize: 59020
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 13287 0 0 0 78971 40 0 0 25 0 1 0 487857404 60977152 13111 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14887 13111 603 41 0 14846 0
vsize: 59548
[startup+800.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 13522 0 0 0 79971 40 0 0 25 0 1 0 487857404 61906944 13346 4294967295 134512640 134672761 3221224624 3221223728 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15114 13346 603 41 0 15073 0
vsize: 60456
[startup+810.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 13742 0 0 0 80970 41 0 0 25 0 1 0 487857404 62853120 13566 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15345 13566 603 41 0 15304 0
vsize: 61380
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 13882 0 0 0 81970 42 0 0 25 0 1 0 487857404 63389696 13706 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15476 13706 603 41 0 15435 0
vsize: 61904
[startup+830.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14032 0 0 0 82969 42 0 0 25 0 1 0 487857404 64057344 13856 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15639 13856 603 41 0 15598 0
vsize: 62556
[startup+840.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14140 0 0 0 83969 43 0 0 25 0 1 0 487857404 64458752 13964 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15737 13964 603 41 0 15696 0
vsize: 62948
[startup+850.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14273 0 0 0 84968 43 0 0 25 0 1 0 487857404 64995328 14097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15868 14097 603 41 0 15827 0
vsize: 63472
[startup+860.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14452 0 0 0 85968 44 0 0 25 0 1 0 487857404 65662976 14276 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16031 14276 603 41 0 15990 0
vsize: 64124
[startup+870.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14581 0 0 0 86968 44 0 0 25 0 1 0 487857404 66203648 14405 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16163 14405 603 41 0 16122 0
vsize: 64652
[startup+880.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14724 0 0 0 87968 44 0 0 25 0 1 0 487857404 66744320 14548 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16295 14548 603 41 0 16254 0
vsize: 65180
[startup+890.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 14845 0 0 0 88968 44 0 0 25 0 1 0 487857404 67276800 14669 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16425 14669 603 41 0 16384 0
vsize: 65700
[startup+900.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 15087 0 0 0 89968 45 0 0 25 0 1 0 487857404 68214784 14911 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16654 14911 603 41 0 16613 0
vsize: 66616
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 15192 0 0 0 90968 45 0 0 25 0 1 0 487857404 68620288 15016 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15016 603 41 0 16712 0
vsize: 67012
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 15307 0 0 0 91967 46 0 0 25 0 1 0 487857404 69152768 15131 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16883 15131 603 41 0 16842 0
vsize: 67532
[startup+930.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 15604 0 0 0 92967 46 0 0 25 0 1 0 487857404 70230016 15428 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17146 15428 603 41 0 17105 0
vsize: 68584
[startup+940.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 15856 0 0 0 93967 47 0 0 25 0 1 0 487857404 71299072 15680 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17407 15680 603 41 0 17366 0
vsize: 69628
[startup+950.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 16047 0 0 0 94966 47 0 0 25 0 1 0 487857404 72110080 15871 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17605 15871 603 41 0 17564 0
vsize: 70420
[startup+960.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 16243 0 0 0 95966 48 0 0 25 0 1 0 487857404 72916992 16067 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17802 16067 603 41 0 17761 0
vsize: 71208
[startup+970.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 16547 0 0 0 96965 49 0 0 25 0 1 0 487857404 74121216 16371 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18096 16371 603 41 0 18055 0
vsize: 72384
[startup+980.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 16743 0 0 0 97965 49 0 0 25 0 1 0 487857404 74792960 16567 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18260 16567 603 41 0 18219 0
vsize: 73040
[startup+990.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 16933 0 0 0 98964 50 0 0 25 0 1 0 487857404 75599872 16757 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18457 16757 603 41 0 18416 0
vsize: 73828
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 17326 0 0 0 99964 51 0 0 25 0 1 0 487857404 77205504 17150 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18849 17150 603 41 0 18808 0
vsize: 75396
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 17947 0 0 0 100962 53 0 0 25 0 1 0 487857404 79753216 17771 4294967295 134512640 134672761 3221224624 3221223808 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19471 17771 603 41 0 19430 0
vsize: 77884
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 101962 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 102962 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 103962 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 104963 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 105963 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134564686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 106963 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 107963 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 108964 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 109964 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 110964 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 111964 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 112965 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 113965 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 114965 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 115965 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 116965 53 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 117965 54 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 118965 54 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 10331
Raw data (stat): 10331 (minisat+) R 10330 30854 30853 0 -1 0 18000 0 0 0 119976 54 0 0 25 0 1 0 487857404 79888384 17824 4294967295 134512640 134672761 3221224624 3221223808 134558632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17824 603 41 0 19463 0
vsize: 78016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 10331
Raw data (stat): 10331 (minisat+) Z 10330 30854 30853 0 -1 12 18002 0 0 0 119976 57 0 0 24 0 1 0 487857404 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.19
CPU time (s): 1200.34
CPU user time (s): 1199.76
CPU system time (s): 0.575912
CPU usage (%): 100.012
Max. virtual memory (Kb): 78016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####