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/miplib/normalized-mps-v2-13-7-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1176.34
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 19204

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 18:16:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16899 boxname=wulflinc28 idbench=1300 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb
IDLAUNCH: 16899
/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:        503256 kB
Buffers:         33880 kB
Cached:         470304 kB
SwapCached:        104 kB
Active:         206356 kB
Inactive:       300252 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        503004 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            18996 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:36:18 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 16899 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> BDD-cost:75537
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> BDD-cost:56893
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  412764  1190247 |  137588       0        0     nan |  0.000 % |
c |       100 |  412764  1190247 |  151346     100     3757    37.6 |  0.066 % |
c |       250 |  412764  1190247 |  166481     250     7598    30.4 |  0.066 % |
c |       475 |  412764  1190247 |  183129     475    54404   114.5 |  0.066 % |
c |       812 |  412764  1190247 |  201442     812   195316   240.5 |  0.066 % |
c |      1319 |  412764  1190247 |  221586    1319   263810   200.0 |  0.066 % |
c |      2082 |  412764  1190247 |  243745    2082   346507   166.4 |  0.066 % |
c |      3223 |  412764  1190247 |  268120    3223   918568   285.0 |  0.066 % |
c |      4931 |  412764  1190247 |  294932    4931  1706139   346.0 |  0.066 % |
c |      7496 |  412764  1190247 |  324425    7496  3061447   408.4 |  0.066 % |
c |     11343 |  412764  1190247 |  356867   11343  5012779   441.9 |  0.066 % |
c |     17115 |  412764  1190247 |  392554   17115  7966858   465.5 |  0.066 % |
c |     25765 |  412764  1190247 |  431810   25765 14434558   560.2 |  0.066 % |
#### 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.91 0.97 0.95 2/54 29573
Raw data (stat): 29573 (runsolver) R 29572 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547173095 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99995 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 13776 0 0 0 965 33 0 0 25 0 1 0 547173095 63496192 12877 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15502 12877 603 41 0 15461 0
vsize: 62008
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 13992 0 0 0 1964 34 0 0 25 0 1 0 547173095 64425984 13093 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15729 13093 603 41 0 15688 0
vsize: 62916
[startup+30.001 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14177 0 0 0 2963 35 0 0 25 0 1 0 547173095 65101824 13278 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15894 13278 603 41 0 15853 0
vsize: 63576
[startup+40.001 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14271 0 0 0 3962 35 0 0 25 0 1 0 547173095 65503232 13372 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15992 13372 603 41 0 15951 0
vsize: 63968
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14336 0 0 0 4963 35 0 0 25 0 1 0 547173095 65773568 13437 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16058 13437 603 41 0 16017 0
vsize: 64232
[startup+60.001 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14433 0 0 0 5962 36 0 0 25 0 1 0 547173095 66187264 13534 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 13534 603 41 0 16118 0
vsize: 64636
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14536 0 0 0 6962 36 0 0 25 0 1 0 547173095 66596864 13637 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16259 13637 603 41 0 16218 0
vsize: 65036
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14625 0 0 0 7962 37 0 0 25 0 1 0 547173095 66994176 13726 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16356 13726 603 41 0 16315 0
vsize: 65424
[startup+90.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14691 0 0 0 8962 37 0 0 25 0 1 0 547173095 67244032 13792 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16417 13792 603 41 0 16376 0
vsize: 65668
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14736 0 0 0 9962 37 0 0 25 0 1 0 547173095 67383296 13837 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16451 13837 603 41 0 16410 0
vsize: 65804
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14799 0 0 0 10962 37 0 0 25 0 1 0 547173095 67641344 13900 4294967295 134512640 134672761 3221224528 3221223632 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16514 13900 603 41 0 16473 0
vsize: 66056
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 14878 0 0 0 11962 37 0 0 25 0 1 0 547173095 68046848 13979 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16613 13979 603 41 0 16572 0
vsize: 66452
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15090 0 0 0 12962 38 0 0 25 0 1 0 547173095 68841472 14191 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16807 14191 603 41 0 16766 0
vsize: 67228
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15201 0 0 0 13962 38 0 0 25 0 1 0 547173095 69386240 14302 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16940 14302 603 41 0 16899 0
vsize: 67760
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15334 0 0 0 14962 38 0 0 25 0 1 0 547173095 69898240 14435 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17065 14435 603 41 0 17024 0
vsize: 68260
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15482 0 0 0 15962 38 0 0 25 0 1 0 547173095 70553600 14583 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17225 14583 603 41 0 17184 0
vsize: 68900
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15611 0 0 0 16962 38 0 0 25 0 1 0 547173095 71086080 14712 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17355 14712 603 41 0 17314 0
vsize: 69420
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15743 0 0 0 17962 39 0 0 25 0 1 0 547173095 71495680 14844 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17455 14844 603 41 0 17414 0
vsize: 69820
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15831 0 0 0 18962 39 0 0 25 0 1 0 547173095 71897088 14932 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17553 14932 603 41 0 17512 0
vsize: 70212
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15881 0 0 0 19962 39 0 0 25 0 1 0 547173095 72155136 14982 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17616 14982 603 41 0 17575 0
vsize: 70464
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15897 0 0 0 20962 39 0 0 25 0 1 0 547173095 72155136 14998 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17616 14998 603 41 0 17575 0
vsize: 70464
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 15986 0 0 0 21962 39 0 0 25 0 1 0 547173095 72552448 15087 4294967295 134512640 134672761 3221224528 3221223632 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17713 15087 603 41 0 17672 0
vsize: 70852
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16184 0 0 0 22962 40 0 0 25 0 1 0 547173095 73355264 15285 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17909 15285 603 41 0 17868 0
vsize: 71636
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16348 0 0 0 23961 40 0 0 25 0 1 0 547173095 74018816 15449 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18071 15449 603 41 0 18030 0
vsize: 72284
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16394 0 0 0 24961 40 0 0 25 0 1 0 547173095 74272768 15495 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 15495 603 41 0 18092 0
vsize: 72532
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16412 0 0 0 25961 41 0 0 25 0 1 0 547173095 74272768 15513 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 15513 603 41 0 18092 0
vsize: 72532
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16430 0 0 0 26961 41 0 0 25 0 1 0 547173095 74399744 15531 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18164 15531 603 41 0 18123 0
vsize: 72656
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16445 0 0 0 27962 41 0 0 25 0 1 0 547173095 74399744 15546 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18164 15546 603 41 0 18123 0
vsize: 72656
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16506 0 0 0 28962 41 0 0 25 0 1 0 547173095 74641408 15607 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18223 15607 603 41 0 18182 0
vsize: 72892
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16573 0 0 0 29962 41 0 0 25 0 1 0 547173095 74907648 15674 4294967295 134512640 134672761 3221224528 3221223632 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18288 15674 603 41 0 18247 0
vsize: 73152
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16730 0 0 0 30962 41 0 0 25 0 1 0 547173095 75579392 15831 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18452 15831 603 41 0 18411 0
vsize: 73808
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 16889 0 0 0 31961 42 0 0 25 0 1 0 547173095 76439552 15990 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18662 15990 603 41 0 18621 0
vsize: 74648
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 17025 0 0 0 32959 43 0 0 25 0 1 0 547173095 76967936 16126 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18791 16126 603 41 0 18750 0
vsize: 75164
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 17304 0 0 0 33958 44 0 0 25 0 1 0 547173095 78045184 16405 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 16405 603 41 0 19013 0
vsize: 76216
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 17504 0 0 0 34958 44 0 0 25 0 1 0 547173095 78987264 16605 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19284 16605 603 41 0 19243 0
vsize: 77136
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 17736 0 0 0 35958 45 0 0 25 0 1 0 547173095 79917056 16837 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19511 16837 603 41 0 19470 0
vsize: 78044
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 18006 0 0 0 36957 46 0 0 25 0 1 0 547173095 80986112 17107 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19772 17107 603 41 0 19731 0
vsize: 79088
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 18320 0 0 0 37956 47 0 0 25 0 1 0 547173095 82194432 17421 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 17421 603 41 0 20026 0
vsize: 80268
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 18764 0 0 0 38954 49 0 0 25 0 1 0 547173095 84078592 17865 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20527 17865 603 41 0 20486 0
vsize: 82108
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 19006 0 0 0 39954 49 0 0 25 0 1 0 547173095 85012480 18107 4294967295 134512640 134672761 3221224528 3221223632 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20755 18107 603 41 0 20714 0
vsize: 83020
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 19217 0 0 0 40953 50 0 0 25 0 1 0 547173095 85958656 18318 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 18318 603 41 0 20945 0
vsize: 83944
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 19427 0 0 0 41953 50 0 0 25 0 1 0 547173095 86777856 18528 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21186 18528 603 41 0 21145 0
vsize: 84744
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 19725 0 0 0 42953 51 0 0 25 0 1 0 547173095 87990272 18826 4294967295 134512640 134672761 3221224528 3221223632 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21482 18826 603 41 0 21441 0
vsize: 85928
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 19896 0 0 0 43952 52 0 0 25 0 1 0 547173095 88641536 18997 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21641 18997 603 41 0 21600 0
vsize: 86564
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 19984 0 0 0 44952 52 0 0 25 0 1 0 547173095 89051136 19085 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 19085 603 41 0 21700 0
vsize: 86964
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20063 0 0 0 45952 52 0 0 25 0 1 0 547173095 89321472 19164 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21807 19164 603 41 0 21766 0
vsize: 87228
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20109 0 0 0 46952 52 0 0 25 0 1 0 547173095 89583616 19210 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21871 19210 603 41 0 21830 0
vsize: 87484
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20250 0 0 0 47952 53 0 0 25 0 1 0 547173095 90124288 19351 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22003 19351 603 41 0 21962 0
vsize: 88012
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20326 0 0 0 48952 53 0 0 25 0 1 0 547173095 90394624 19427 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22069 19427 603 41 0 22028 0
vsize: 88276
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20380 0 0 0 49952 53 0 0 25 0 1 0 547173095 90664960 19481 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22135 19481 603 41 0 22094 0
vsize: 88540
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20398 0 0 0 50952 53 0 0 25 0 1 0 547173095 90804224 19499 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 19499 603 41 0 22128 0
vsize: 88676
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20418 0 0 0 51952 53 0 0 25 0 1 0 547173095 90804224 19519 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 19519 603 41 0 22128 0
vsize: 88676
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20429 0 0 0 52952 53 0 0 25 0 1 0 547173095 90939392 19530 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22202 19530 603 41 0 22161 0
vsize: 88808
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20455 0 0 0 53952 53 0 0 25 0 1 0 547173095 90939392 19556 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22202 19556 603 41 0 22161 0
vsize: 88808
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20481 0 0 0 54953 53 0 0 25 0 1 0 547173095 91074560 19582 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22235 19582 603 41 0 22194 0
vsize: 88940
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20507 0 0 0 55953 54 0 0 25 0 1 0 547173095 91209728 19608 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 19608 603 41 0 22227 0
vsize: 89072
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20525 0 0 0 56953 54 0 0 25 0 1 0 547173095 91209728 19626 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 19626 603 41 0 22227 0
vsize: 89072
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20557 0 0 0 57953 54 0 0 25 0 1 0 547173095 91344896 19658 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22301 19658 603 41 0 22260 0
vsize: 89204
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20595 0 0 0 58953 54 0 0 25 0 1 0 547173095 91619328 19696 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22368 19696 603 41 0 22327 0
vsize: 89472
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20612 0 0 0 59953 54 0 0 25 0 1 0 547173095 91619328 19713 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22368 19713 603 41 0 22327 0
vsize: 89472
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20621 0 0 0 60953 54 0 0 25 0 1 0 547173095 91619328 19722 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22368 19722 603 41 0 22327 0
vsize: 89472
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20634 0 0 0 61953 54 0 0 25 0 1 0 547173095 91754496 19735 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22401 19735 603 41 0 22360 0
vsize: 89604
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20688 0 0 0 62954 54 0 0 25 0 1 0 547173095 91889664 19789 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22434 19789 603 41 0 22393 0
vsize: 89736
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20773 0 0 0 63954 54 0 0 25 0 1 0 547173095 92291072 19874 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22532 19874 603 41 0 22491 0
vsize: 90128
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 20975 0 0 0 64953 55 0 0 25 0 1 0 547173095 93106176 20076 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22731 20076 603 41 0 22690 0
vsize: 90924
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 21198 0 0 0 65953 55 0 0 25 0 1 0 547173095 94035968 20299 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22958 20299 603 41 0 22917 0
vsize: 91832
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 21433 0 0 0 66952 56 0 0 25 0 1 0 547173095 95047680 20534 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23205 20534 603 41 0 23164 0
vsize: 92820
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 21708 0 0 0 67951 58 0 0 25 0 1 0 547173095 96112640 20809 4294967295 134512640 134672761 3221224528 3221223680 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23465 20809 603 41 0 23424 0
vsize: 93860
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 21913 0 0 0 68948 59 0 0 25 0 1 0 547173095 97034240 21014 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23690 21014 603 41 0 23649 0
vsize: 94760
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 22053 0 0 0 69948 60 0 0 25 0 1 0 547173095 97554432 21154 4294967295 134512640 134672761 3221224528 3221223632 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23817 21154 603 41 0 23776 0
vsize: 95268
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 22165 0 0 0 70948 60 0 0 25 0 1 0 547173095 98041856 21266 4294967295 134512640 134672761 3221224528 3221223632 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23936 21266 603 41 0 23895 0
vsize: 95744
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 22280 0 0 0 71948 60 0 0 25 0 1 0 547173095 98557952 21381 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24062 21381 603 41 0 24021 0
vsize: 96248
[startup+730.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 22456 0 0 0 72948 60 0 0 25 0 1 0 547173095 99192832 21557 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24217 21557 603 41 0 24176 0
vsize: 96868
[startup+740.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 22695 0 0 0 73948 61 0 0 25 0 1 0 547173095 100245504 21796 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24474 21796 603 41 0 24433 0
vsize: 97896
[startup+750.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 22946 0 0 0 74947 61 0 0 25 0 1 0 547173095 101179392 22047 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24702 22047 603 41 0 24661 0
vsize: 98808
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 23245 0 0 0 75947 62 0 0 25 0 1 0 547173095 102502400 22346 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25025 22346 603 41 0 24984 0
vsize: 100100
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 23483 0 0 0 76947 62 0 0 25 0 1 0 547173095 103424000 22584 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25250 22584 603 41 0 25209 0
vsize: 101000
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 23764 0 0 0 77947 63 0 0 25 0 1 0 547173095 104603648 22865 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25538 22865 603 41 0 25497 0
vsize: 102152
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 24043 0 0 0 78946 64 0 0 25 0 1 0 547173095 105664512 23144 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25797 23144 603 41 0 25756 0
vsize: 103188
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 24312 0 0 0 79946 64 0 0 25 0 1 0 547173095 106827776 23413 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26081 23413 603 41 0 26040 0
vsize: 104324
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 24617 0 0 0 80946 64 0 0 25 0 1 0 547173095 108019712 23718 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26372 23718 603 41 0 26331 0
vsize: 105488
[startup+820.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 24875 0 0 0 81945 65 0 0 25 0 1 0 547173095 109084672 23976 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26632 23976 603 41 0 26591 0
vsize: 106528
[startup+830.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 25135 0 0 0 82945 66 0 0 25 0 1 0 547173095 110145536 24236 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26891 24236 603 41 0 26850 0
vsize: 107564
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 25410 0 0 0 83944 66 0 0 25 0 1 0 547173095 111316992 24511 4294967295 134512640 134672761 3221224528 3221223632 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27177 24511 603 41 0 27136 0
vsize: 108708
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 25627 0 0 0 84944 67 0 0 25 0 1 0 547173095 112246784 24728 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27404 24728 603 41 0 27363 0
vsize: 109616
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 25893 0 0 0 85943 68 0 0 25 0 1 0 547173095 113291264 24994 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27659 24994 603 41 0 27618 0
vsize: 110636
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 26166 0 0 0 86942 69 0 0 25 0 1 0 547173095 114339840 25267 4294967295 134512640 134672761 3221224528 3221223632 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27915 25267 603 41 0 27874 0
vsize: 111660
[startup+880.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 26479 0 0 0 87942 69 0 0 25 0 1 0 547173095 115662848 25580 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28238 25580 603 41 0 28197 0
vsize: 112952
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 26754 0 0 0 88941 70 0 0 25 0 1 0 547173095 116834304 25855 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28524 25855 603 41 0 28483 0
vsize: 114096
[startup+900.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 26981 0 0 0 89941 71 0 0 25 0 1 0 547173095 117760000 26082 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28750 26082 603 41 0 28709 0
vsize: 115000
[startup+910.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 27240 0 0 0 90940 71 0 0 25 0 1 0 547173095 118812672 26341 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29007 26341 603 41 0 28966 0
vsize: 116028
[startup+920.009 s]
Raw data (loadavg): 1.15 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 27532 0 0 0 91940 72 0 0 25 0 1 0 547173095 119996416 26633 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29296 26633 603 41 0 29255 0
vsize: 117184
[startup+930.008 s]
Raw data (loadavg): 1.12 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 27807 0 0 0 92939 73 0 0 25 0 1 0 547173095 121085952 26908 4294967295 134512640 134672761 3221224528 3221223696 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29562 26908 603 41 0 29521 0
vsize: 118248
[startup+940.008 s]
Raw data (loadavg): 1.10 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28070 0 0 0 93939 74 0 0 25 0 1 0 547173095 122150912 27171 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29822 27171 603 41 0 29781 0
vsize: 119288
[startup+950.009 s]
Raw data (loadavg): 1.09 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28275 0 0 0 94937 75 0 0 25 0 1 0 547173095 123084800 27376 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30050 27376 603 41 0 30009 0
vsize: 120200
[startup+960.008 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28329 0 0 0 95936 75 0 0 25 0 1 0 547173095 123219968 27430 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 27430 603 41 0 30042 0
vsize: 120332
[startup+970.009 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28376 0 0 0 96936 76 0 0 25 0 1 0 547173095 123490304 27477 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30149 27477 603 41 0 30108 0
vsize: 120596
[startup+980.01 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28417 0 0 0 97936 76 0 0 25 0 1 0 547173095 123625472 27518 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27518 603 41 0 30141 0
vsize: 120728
[startup+990.009 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28432 0 0 0 98936 76 0 0 25 0 1 0 547173095 123625472 27533 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27533 603 41 0 30141 0
vsize: 120728
[startup+1000.01 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28460 0 0 0 99936 76 0 0 25 0 1 0 547173095 123760640 27561 4294967295 134512640 134672761 3221224528 3221223632 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30215 27561 603 41 0 30174 0
vsize: 120860
[startup+1010.01 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28495 0 0 0 100936 76 0 0 25 0 1 0 547173095 123887616 27596 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30246 27596 603 41 0 30205 0
vsize: 120984
[startup+1020.01 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28524 0 0 0 101936 76 0 0 25 0 1 0 547173095 124022784 27625 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30279 27625 603 41 0 30238 0
vsize: 121116
[startup+1030.01 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28556 0 0 0 102936 76 0 0 25 0 1 0 547173095 124149760 27657 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30310 27657 603 41 0 30269 0
vsize: 121240
[startup+1040.01 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28577 0 0 0 103936 76 0 0 25 0 1 0 547173095 124280832 27678 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30342 27678 603 41 0 30301 0
vsize: 121368
[startup+1050.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28600 0 0 0 104937 76 0 0 25 0 1 0 547173095 124399616 27701 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30371 27701 603 41 0 30330 0
vsize: 121484
[startup+1060.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28616 0 0 0 105937 76 0 0 25 0 1 0 547173095 124399616 27717 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30371 27717 603 41 0 30330 0
vsize: 121484
[startup+1070.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28641 0 0 0 106937 76 0 0 25 0 1 0 547173095 124526592 27742 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30402 27742 603 41 0 30361 0
vsize: 121608
[startup+1080.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28658 0 0 0 107937 76 0 0 25 0 1 0 547173095 124661760 27759 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30435 27759 603 41 0 30394 0
vsize: 121740
[startup+1090.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28674 0 0 0 108937 76 0 0 25 0 1 0 547173095 124661760 27775 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30435 27775 603 41 0 30394 0
vsize: 121740
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28694 0 0 0 109938 76 0 0 25 0 1 0 547173095 124780544 27795 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30464 27795 603 41 0 30423 0
vsize: 121856
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28722 0 0 0 110938 77 0 0 25 0 1 0 547173095 124919808 27823 4294967295 134512640 134672761 3221224528 3221223632 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30498 27823 603 41 0 30457 0
vsize: 121992
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28742 0 0 0 111938 77 0 0 25 0 1 0 547173095 124919808 27843 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30498 27843 603 41 0 30457 0
vsize: 121992
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28756 0 0 0 112938 77 0 0 25 0 1 0 547173095 125054976 27857 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30531 27857 603 41 0 30490 0
vsize: 122124
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28776 0 0 0 113938 77 0 0 25 0 1 0 547173095 125054976 27877 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30531 27877 603 41 0 30490 0
vsize: 122124
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28795 0 0 0 114938 77 0 0 25 0 1 0 547173095 125186048 27896 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30563 27896 603 41 0 30522 0
vsize: 122252
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28819 0 0 0 115938 77 0 0 25 0 1 0 547173095 125325312 27920 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30597 27920 603 41 0 30556 0
vsize: 122388
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28842 0 0 0 116938 77 0 0 25 0 1 0 547173095 125325312 27943 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30597 27943 603 41 0 30556 0
vsize: 122388
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28877 0 0 0 117938 77 0 0 25 0 1 0 547173095 125444096 27978 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30626 27978 603 41 0 30585 0
vsize: 122504
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28910 0 0 0 118938 77 0 0 25 0 1 0 547173095 125579264 28011 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30659 28011 603 41 0 30618 0
vsize: 122636
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 29573
Raw data (stat): 29573 (minisat+) R 29572 10614 10613 0 -1 0 28944 0 0 0 119939 77 0 0 25 0 1 0 547173095 125714432 28045 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30692 28045 603 41 0 30651 0
vsize: 122768
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 29573
Raw data (stat): 29573 (minisat+) Z 29572 10614 10613 0 -1 12 28946 0 0 0 119939 83 0 0 25 0 1 0 547173095 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.22
CPU user time (s): 1199.39
CPU system time (s): 0.831873
CPU usage (%): 100.013
Max. virtual memory (Kb): 122768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####