PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-l152lav.opb
MD5SUM	9d4ce12b138a2bef65a1f401ec9d1f01
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4742
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	1175.33
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 16440

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-21 07:12:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13493 boxname=wulflinc4 idbench=1038 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d4ce12b138a2bef65a1f401ec9d1f01  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-l152lav.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 13493
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        704896 kB
Buffers:         31812 kB
Cached:         275276 kB
SwapCached:          0 kB
Active:          55340 kB
Inactive:       254560 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        704644 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14300 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:32:51 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 13493 7 1200.23 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.92 0.97 0.91 2/54 3690
Raw data (stat): 3690 (runsolver) R 3689 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484961192 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+10.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 13776 0 0 0 967 31 0 0 25 0 1 0 484961192 63496192 12877 4294967295 134512640 134672761 3221224528 3221223712 134559354 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.0008 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 13992 0 0 0 1967 32 0 0 25 0 1 0 484961192 64425984 13093 4294967295 134512640 134672761 3221224528 3221223728 134557806 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.002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14177 0 0 0 2965 33 0 0 25 0 1 0 484961192 65101824 13278 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15894 13278 603 41 0 15853 0
vsize: 63576
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14271 0 0 0 3964 34 0 0 25 0 1 0 484961192 65503232 13372 4294967295 134512640 134672761 3221224528 3221223696 134560808 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.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14336 0 0 0 4964 34 0 0 25 0 1 0 484961192 65773568 13437 4294967295 134512640 134672761 3221224528 3221223632 134560289 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.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14434 0 0 0 5964 34 0 0 25 0 1 0 484961192 66187264 13535 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 13535 603 41 0 16118 0
vsize: 64636
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14537 0 0 0 6964 34 0 0 25 0 1 0 484961192 66596864 13638 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16259 13638 603 41 0 16218 0
vsize: 65036
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14625 0 0 0 7964 34 0 0 25 0 1 0 484961192 66994176 13726 4294967295 134512640 134672761 3221224528 3221223696 134560869 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14691 0 0 0 8964 34 0 0 25 0 1 0 484961192 67244032 13792 4294967295 134512640 134672761 3221224528 3221223632 134560196 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14742 0 0 0 9964 35 0 0 25 0 1 0 484961192 67522560 13843 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16485 13843 603 41 0 16444 0
vsize: 65940
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14802 0 0 0 10964 35 0 0 25 0 1 0 484961192 67641344 13903 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16514 13903 603 41 0 16473 0
vsize: 66056
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 14878 0 0 0 11964 35 0 0 25 0 1 0 484961192 68046848 13979 4294967295 134512640 134672761 3221224528 3221223632 134560405 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15118 0 0 0 12963 36 0 0 25 0 1 0 484961192 68976640 14219 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16840 14219 603 41 0 16799 0
vsize: 67360
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15210 0 0 0 13963 36 0 0 25 0 1 0 484961192 69386240 14311 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16940 14311 603 41 0 16899 0
vsize: 67760
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15347 0 0 0 14963 37 0 0 25 0 1 0 484961192 69898240 14448 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17065 14448 603 41 0 17024 0
vsize: 68260
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15483 0 0 0 15963 37 0 0 25 0 1 0 484961192 70553600 14584 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17225 14584 603 41 0 17184 0
vsize: 68900
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15624 0 0 0 16962 38 0 0 25 0 1 0 484961192 71086080 14725 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17355 14725 603 41 0 17314 0
vsize: 69420
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15766 0 0 0 17961 38 0 0 25 0 1 0 484961192 71626752 14867 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17487 14867 603 41 0 17446 0
vsize: 69948
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15835 0 0 0 18962 38 0 0 25 0 1 0 484961192 71897088 14936 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17553 14936 603 41 0 17512 0
vsize: 70212
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15884 0 0 0 19961 39 0 0 25 0 1 0 484961192 72155136 14985 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17616 14985 603 41 0 17575 0
vsize: 70464
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 15897 0 0 0 20962 39 0 0 25 0 1 0 484961192 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16017 0 0 0 21961 39 0 0 25 0 1 0 484961192 72679424 15118 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17744 15118 603 41 0 17703 0
vsize: 70976
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16198 0 0 0 22961 40 0 0 25 0 1 0 484961192 73355264 15299 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17909 15299 603 41 0 17868 0
vsize: 71636
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16355 0 0 0 23960 41 0 0 25 0 1 0 484961192 74018816 15456 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18071 15456 603 41 0 18030 0
vsize: 72284
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16396 0 0 0 24961 41 0 0 25 0 1 0 484961192 74272768 15497 4294967295 134512640 134672761 3221224528 3221223696 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 15497 603 41 0 18092 0
vsize: 72532
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16412 0 0 0 25961 41 0 0 25 0 1 0 484961192 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16430 0 0 0 26961 41 0 0 25 0 1 0 484961192 74399744 15531 4294967295 134512640 134672761 3221224528 3221223632 134560529 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16454 0 0 0 27961 41 0 0 25 0 1 0 484961192 74518528 15555 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 15555 603 41 0 18152 0
vsize: 72772
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16528 0 0 0 28961 41 0 0 25 0 1 0 484961192 74776576 15629 4294967295 134512640 134672761 3221224528 3221223632 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18256 15629 603 41 0 18215 0
vsize: 73024
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16574 0 0 0 29961 41 0 0 25 0 1 0 484961192 74907648 15675 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18288 15675 603 41 0 18247 0
vsize: 73152
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16747 0 0 0 30960 42 0 0 25 0 1 0 484961192 75714560 15848 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18485 15848 603 41 0 18444 0
vsize: 73940
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 16927 0 0 0 31960 42 0 0 25 0 1 0 484961192 76574720 16028 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18695 16028 603 41 0 18654 0
vsize: 74780
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 17065 0 0 0 32960 43 0 0 25 0 1 0 484961192 77103104 16166 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18824 16166 603 41 0 18783 0
vsize: 75296
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 17350 0 0 0 33960 43 0 0 25 0 1 0 484961192 78315520 16451 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19120 16451 603 41 0 19079 0
vsize: 76480
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 17534 0 0 0 34960 43 0 0 25 0 1 0 484961192 79106048 16635 4294967295 134512640 134672761 3221224528 3221223632 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19313 16635 603 41 0 19272 0
vsize: 77252
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 17785 0 0 0 35959 44 0 0 25 0 1 0 484961192 80052224 16886 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19544 16886 603 41 0 19503 0
vsize: 78176
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 18053 0 0 0 36959 44 0 0 25 0 1 0 484961192 81121280 17154 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19805 17154 603 41 0 19764 0
vsize: 79220
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 18397 0 0 0 37958 45 0 0 25 0 1 0 484961192 82599936 17498 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20166 17498 603 41 0 20125 0
vsize: 80664
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 18819 0 0 0 38957 46 0 0 25 0 1 0 484961192 84348928 17920 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20593 17920 603 41 0 20552 0
vsize: 82372
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 19059 0 0 0 39957 46 0 0 25 0 1 0 484961192 85282816 18160 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20821 18160 603 41 0 20780 0
vsize: 83284
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 19265 0 0 0 40957 47 0 0 25 0 1 0 484961192 86093824 18366 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21019 18366 603 41 0 20978 0
vsize: 84076
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 19485 0 0 0 41957 47 0 0 25 0 1 0 484961192 87048192 18586 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21252 18586 603 41 0 21211 0
vsize: 85008
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 19769 0 0 0 42956 48 0 0 25 0 1 0 484961192 88125440 18870 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21515 18870 603 41 0 21474 0
vsize: 86060
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 19916 0 0 0 43956 49 0 0 25 0 1 0 484961192 88776704 19017 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21674 19017 603 41 0 21633 0
vsize: 86696
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 19991 0 0 0 44956 49 0 0 25 0 1 0 484961192 89051136 19092 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 19092 603 41 0 21700 0
vsize: 86964
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20091 0 0 0 45955 49 0 0 25 0 1 0 484961192 89448448 19192 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21838 19192 603 41 0 21797 0
vsize: 87352
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20123 0 0 0 46954 49 0 0 25 0 1 0 484961192 89583616 19224 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21871 19224 603 41 0 21830 0
vsize: 87484
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20259 0 0 0 47954 50 0 0 25 0 1 0 484961192 90124288 19360 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22003 19360 603 41 0 21962 0
vsize: 88012
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20329 0 0 0 48954 50 0 0 25 0 1 0 484961192 90529792 19430 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22102 19430 603 41 0 22061 0
vsize: 88408
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20384 0 0 0 49953 50 0 0 25 0 1 0 484961192 90664960 19485 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22135 19485 603 41 0 22094 0
vsize: 88540
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20404 0 0 0 50953 51 0 0 25 0 1 0 484961192 90804224 19505 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22169 19505 603 41 0 22128 0
vsize: 88676
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20418 0 0 0 51953 51 0 0 25 0 1 0 484961192 90804224 19519 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22169 19519 603 41 0 22128 0
vsize: 88676
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20433 0 0 0 52953 52 0 0 25 0 1 0 484961192 90939392 19534 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22202 19534 603 41 0 22161 0
vsize: 88808
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20456 0 0 0 53952 52 0 0 25 0 1 0 484961192 90939392 19557 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22202 19557 603 41 0 22161 0
vsize: 88808
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20482 0 0 0 54952 52 0 0 25 0 1 0 484961192 91074560 19583 4294967295 134512640 134672761 3221224528 3221223632 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22235 19583 603 41 0 22194 0
vsize: 88940
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20511 0 0 0 55952 52 0 0 25 0 1 0 484961192 91209728 19612 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22268 19612 603 41 0 22227 0
vsize: 89072
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20528 0 0 0 56952 53 0 0 25 0 1 0 484961192 91344896 19629 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22301 19629 603 41 0 22260 0
vsize: 89204
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20562 0 0 0 57952 53 0 0 25 0 1 0 484961192 91480064 19663 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22334 19663 603 41 0 22293 0
vsize: 89336
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20597 0 0 0 58952 53 0 0 25 0 1 0 484961192 91619328 19698 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19698 603 41 0 22327 0
vsize: 89472
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20615 0 0 0 59952 53 0 0 25 0 1 0 484961192 91619328 19716 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19716 603 41 0 22327 0
vsize: 89472
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20626 0 0 0 60951 54 0 0 25 0 1 0 484961192 91619328 19727 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19727 603 41 0 22327 0
vsize: 89472
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20636 0 0 0 61951 55 0 0 25 0 1 0 484961192 91754496 19737 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22401 19737 603 41 0 22360 0
vsize: 89604
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20690 0 0 0 62950 55 0 0 25 0 1 0 484961192 91889664 19791 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22434 19791 603 41 0 22393 0
vsize: 89736
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20785 0 0 0 63950 56 0 0 25 0 1 0 484961192 92291072 19886 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22532 19886 603 41 0 22491 0
vsize: 90128
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 20982 0 0 0 64950 56 0 0 25 0 1 0 484961192 93106176 20083 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22731 20083 603 41 0 22690 0
vsize: 90924
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 21208 0 0 0 65949 57 0 0 25 0 1 0 484961192 94035968 20309 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22958 20309 603 41 0 22917 0
vsize: 91832
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 21439 0 0 0 66948 58 0 0 25 0 1 0 484961192 95047680 20540 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23205 20540 603 41 0 23164 0
vsize: 92820
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 21709 0 0 0 67947 59 0 0 25 0 1 0 484961192 96112640 20810 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23465 20810 603 41 0 23424 0
vsize: 93860
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 21920 0 0 0 68947 59 0 0 25 0 1 0 484961192 97034240 21021 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23690 21021 603 41 0 23649 0
vsize: 94760
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 22057 0 0 0 69946 60 0 0 25 0 1 0 484961192 97554432 21158 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23817 21158 603 41 0 23776 0
vsize: 95268
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 22165 0 0 0 70947 61 0 0 25 0 1 0 484961192 98041856 21266 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23936 21266 603 41 0 23895 0
vsize: 95744
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 22280 0 0 0 71946 61 0 0 25 0 1 0 484961192 98557952 21381 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24062 21381 603 41 0 24021 0
vsize: 96248
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 22453 0 0 0 72946 61 0 0 25 0 1 0 484961192 99192832 21554 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24217 21554 603 41 0 24176 0
vsize: 96868
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 22688 0 0 0 73946 62 0 0 25 0 1 0 484961192 100110336 21789 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24441 21789 603 41 0 24400 0
vsize: 97764
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 22936 0 0 0 74944 63 0 0 25 0 1 0 484961192 101179392 22037 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24702 22037 603 41 0 24661 0
vsize: 98808
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 23231 0 0 0 75943 65 0 0 25 0 1 0 484961192 102367232 22332 4294967295 134512640 134672761 3221224528 3221223712 134559569 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24992 22332 603 41 0 24951 0
vsize: 99968
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 23470 0 0 0 76943 65 0 0 25 0 1 0 484961192 103424000 22571 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25250 22571 603 41 0 25209 0
vsize: 101000
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 23750 0 0 0 77942 66 0 0 25 0 1 0 484961192 104468480 22851 4294967295 134512640 134672761 3221224528 3221223712 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25505 22851 603 41 0 25464 0
vsize: 102020
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 24022 0 0 0 78941 67 0 0 25 0 1 0 484961192 105664512 23123 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25797 23123 603 41 0 25756 0
vsize: 103188
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 24291 0 0 0 79940 68 0 0 25 0 1 0 484961192 106692608 23392 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26048 23392 603 41 0 26007 0
vsize: 104192
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 24582 0 0 0 80939 69 0 0 25 0 1 0 484961192 107884544 23683 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26339 23683 603 41 0 26298 0
vsize: 105356
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 24837 0 0 0 81939 70 0 0 25 0 1 0 484961192 108953600 23938 4294967295 134512640 134672761 3221224528 3221223632 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26600 23938 603 41 0 26559 0
vsize: 106400
[startup+830.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 25101 0 0 0 82938 71 0 0 25 0 1 0 484961192 110018560 24202 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26860 24202 603 41 0 26819 0
vsize: 107440
[startup+840.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 25376 0 0 0 83937 72 0 0 25 0 1 0 484961192 111181824 24477 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27144 24477 603 41 0 27103 0
vsize: 108576
[startup+850.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 25591 0 0 0 84937 72 0 0 25 0 1 0 484961192 112123904 24692 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27374 24692 603 41 0 27333 0
vsize: 109496
[startup+860.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 25851 0 0 0 85936 73 0 0 25 0 1 0 484961192 113156096 24952 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27626 24952 603 41 0 27585 0
vsize: 110504
[startup+870.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 26130 0 0 0 86935 74 0 0 25 0 1 0 484961192 114221056 25231 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27886 25231 603 41 0 27845 0
vsize: 111544
[startup+880.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 26421 0 0 0 87935 75 0 0 25 0 1 0 484961192 115396608 25522 4294967295 134512640 134672761 3221224528 3221223712 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28173 25522 603 41 0 28132 0
vsize: 112692
[startup+890.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 26690 0 0 0 88934 76 0 0 25 0 1 0 484961192 116563968 25791 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28458 25791 603 41 0 28417 0
vsize: 113832
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 26932 0 0 0 89934 76 0 0 25 0 1 0 484961192 117489664 26033 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28684 26033 603 41 0 28643 0
vsize: 114736
[startup+910.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 27196 0 0 0 90934 77 0 0 25 0 1 0 484961192 118677504 26297 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28974 26297 603 41 0 28933 0
vsize: 115896
[startup+920.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 27462 0 0 0 91933 77 0 0 25 0 1 0 484961192 119726080 26563 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29230 26563 603 41 0 29189 0
vsize: 116920
[startup+930.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 27756 0 0 0 92933 78 0 0 25 0 1 0 484961192 120950784 26857 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29529 26857 603 41 0 29488 0
vsize: 118116
[startup+940.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28018 0 0 0 93934 79 0 0 25 0 1 0 484961192 122015744 27119 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29789 27119 603 41 0 29748 0
vsize: 119156
[startup+950.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28264 0 0 0 94933 79 0 0 25 0 1 0 484961192 122945536 27365 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30016 27365 603 41 0 29975 0
vsize: 120064
[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28322 0 0 0 95932 80 0 0 25 0 1 0 484961192 123219968 27423 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 27423 603 41 0 30042 0
vsize: 120332
[startup+970.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28374 0 0 0 96932 80 0 0 25 0 1 0 484961192 123490304 27475 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30149 27475 603 41 0 30108 0
vsize: 120596
[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28411 0 0 0 97932 81 0 0 25 0 1 0 484961192 123625472 27512 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27512 603 41 0 30141 0
vsize: 120728
[startup+990.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28430 0 0 0 98932 81 0 0 25 0 1 0 484961192 123625472 27531 4294967295 134512640 134672761 3221224528 3221223632 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27531 603 41 0 30141 0
vsize: 120728
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28457 0 0 0 99932 81 0 0 25 0 1 0 484961192 123760640 27558 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30215 27558 603 41 0 30174 0
vsize: 120860
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28492 0 0 0 100932 81 0 0 25 0 1 0 484961192 123887616 27593 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30246 27593 603 41 0 30205 0
vsize: 120984
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28521 0 0 0 101932 81 0 0 25 0 1 0 484961192 124022784 27622 4294967295 134512640 134672761 3221224528 3221223632 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30279 27622 603 41 0 30238 0
vsize: 121116
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28556 0 0 0 102932 81 0 0 25 0 1 0 484961192 124149760 27657 4294967295 134512640 134672761 3221224528 3221223632 134560344 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28577 0 0 0 103932 81 0 0 25 0 1 0 484961192 124280832 27678 4294967295 134512640 134672761 3221224528 3221223632 134560235 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28600 0 0 0 104932 81 0 0 25 0 1 0 484961192 124399616 27701 4294967295 134512640 134672761 3221224528 3221223632 134560504 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28616 0 0 0 105933 81 0 0 25 0 1 0 484961192 124399616 27717 4294967295 134512640 134672761 3221224528 3221223632 134559859 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28646 0 0 0 106933 81 0 0 25 0 1 0 484961192 124526592 27747 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30402 27747 603 41 0 30361 0
vsize: 121608
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28658 0 0 0 107933 82 0 0 25 0 1 0 484961192 124661760 27759 4294967295 134512640 134672761 3221224528 3221223632 134560235 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28675 0 0 0 108933 82 0 0 25 0 1 0 484961192 124661760 27776 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30435 27776 603 41 0 30394 0
vsize: 121740
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28702 0 0 0 109933 82 0 0 25 0 1 0 484961192 124780544 27803 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30464 27803 603 41 0 30423 0
vsize: 121856
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28722 0 0 0 110933 82 0 0 25 0 1 0 484961192 124919808 27823 4294967295 134512640 134672761 3221224528 3221223632 134560529 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28742 0 0 0 111933 82 0 0 25 0 1 0 484961192 124919808 27843 4294967295 134512640 134672761 3221224528 3221223632 134560390 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28761 0 0 0 112934 82 0 0 25 0 1 0 484961192 125054976 27862 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30531 27862 603 41 0 30490 0
vsize: 122124
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28779 0 0 0 113934 82 0 0 25 0 1 0 484961192 125054976 27880 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30531 27880 603 41 0 30490 0
vsize: 122124
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28803 0 0 0 114934 82 0 0 25 0 1 0 484961192 125186048 27904 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30563 27904 603 41 0 30522 0
vsize: 122252
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28822 0 0 0 115934 82 0 0 25 0 1 0 484961192 125325312 27923 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30597 27923 603 41 0 30556 0
vsize: 122388
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28851 0 0 0 116934 82 0 0 25 0 1 0 484961192 125460480 27952 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30630 27952 603 41 0 30589 0
vsize: 122520
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28885 0 0 0 117934 82 0 0 25 0 1 0 484961192 125579264 27986 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30659 27986 603 41 0 30618 0
vsize: 122636
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28920 0 0 0 118934 82 0 0 25 0 1 0 484961192 125714432 28021 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30692 28021 603 41 0 30651 0
vsize: 122768
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3690
Raw data (stat): 3690 (minisat+) R 3689 5897 5896 0 -1 0 28952 0 0 0 119934 82 0 0 25 0 1 0 484961192 125849600 28053 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30725 28053 603 41 0 30684 0
vsize: 122900
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3690
Raw data (stat): 3690 (minisat+) Z 3689 5897 5896 0 -1 12 28954 0 0 0 119934 88 0 0 24 0 1 0 484961192 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.14
CPU time (s): 1200.23
CPU user time (s): 1199.34
CPU system time (s): 0.881865
CPU usage (%): 100.007
Max. virtual memory (Kb): 122900
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####