PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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	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	1175.69
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 18177

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 13:47:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18485 boxname=wulflinc15 idbench=1422 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d4ce12b138a2bef65a1f401ec9d1f01  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-l152lav.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-l152lav.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-l152lav.opb
IDLAUNCH: 18485
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        805648 kB
Buffers:         29000 kB
Cached:         178300 kB
SwapCached:        440 kB
Active:          12668 kB
Inactive:       196752 kB
HighTotal:      131008 kB
HighFree:        62524 kB
LowTotal:       903652 kB
LowFree:        743124 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13760 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:08:00 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 18485 7 1200.21 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.93 2/54 8878
Raw data (stat): 8878 (runsolver) R 8877 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487333388 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 13773 0 0 0 964 34 0 0 25 0 1 0 487333388 63496192 12874 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15502 12874 603 41 0 15461 0
vsize: 62008
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 13988 0 0 0 1963 35 0 0 25 0 1 0 487333388 64425984 13089 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15729 13089 603 41 0 15688 0
vsize: 62916
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14176 0 0 0 2962 36 0 0 25 0 1 0 487333388 65101824 13277 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15894 13277 603 41 0 15853 0
vsize: 63576
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14261 0 0 0 3962 36 0 0 25 0 1 0 487333388 65503232 13362 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15992 13362 603 41 0 15951 0
vsize: 63968
[startup+50.0008 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14333 0 0 0 4962 36 0 0 25 0 1 0 487333388 65773568 13434 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 13434 603 41 0 16017 0
vsize: 64232
[startup+60.0006 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14426 0 0 0 5962 37 0 0 25 0 1 0 487333388 66187264 13527 4294967295 134512640 134672761 3221224528 3221223632 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16159 13527 603 41 0 16118 0
vsize: 64636
[startup+70.0004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14530 0 0 0 6961 37 0 0 25 0 1 0 487333388 66596864 13631 4294967295 134512640 134672761 3221224528 3221223632 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16259 13631 603 41 0 16218 0
vsize: 65036
[startup+80.0012 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14613 0 0 0 7961 38 0 0 25 0 1 0 487333388 66994176 13714 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16356 13714 603 41 0 16315 0
vsize: 65424
[startup+90.0011 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14686 0 0 0 8960 38 0 0 25 0 1 0 487333388 67244032 13787 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16417 13787 603 41 0 16376 0
vsize: 65668
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14733 0 0 0 9960 38 0 0 25 0 1 0 487333388 67383296 13834 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16451 13834 603 41 0 16410 0
vsize: 65804
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14799 0 0 0 10960 38 0 0 25 0 1 0 487333388 67641344 13900 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 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.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 14872 0 0 0 11960 39 0 0 25 0 1 0 487333388 68046848 13973 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16613 13973 603 41 0 16572 0
vsize: 66452
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15027 0 0 0 12960 39 0 0 25 0 1 0 487333388 68571136 14128 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16741 14128 603 41 0 16700 0
vsize: 66964
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15173 0 0 0 13960 39 0 0 25 0 1 0 487333388 69251072 14274 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16907 14274 603 41 0 16866 0
vsize: 67628
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15318 0 0 0 14960 40 0 0 25 0 1 0 487333388 69763072 14419 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17032 14419 603 41 0 16991 0
vsize: 68128
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15472 0 0 0 15959 40 0 0 25 0 1 0 487333388 70418432 14573 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17192 14573 603 41 0 17151 0
vsize: 68768
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15557 0 0 0 16959 41 0 0 25 0 1 0 487333388 70819840 14658 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17290 14658 603 41 0 17249 0
vsize: 69160
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15686 0 0 0 17959 41 0 0 25 0 1 0 487333388 71360512 14787 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17422 14787 603 41 0 17381 0
vsize: 69688
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15822 0 0 0 18959 41 0 0 25 0 1 0 487333388 71897088 14923 4294967295 134512640 134672761 3221224528 3221223632 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17553 14923 603 41 0 17512 0
vsize: 70212
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15881 0 0 0 19959 42 0 0 25 0 1 0 487333388 72155136 14982 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17616 14982 603 41 0 17575 0
vsize: 70464
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15895 0 0 0 20959 42 0 0 25 0 1 0 487333388 72155136 14996 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17616 14996 603 41 0 17575 0
vsize: 70464
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 15948 0 0 0 21959 42 0 0 25 0 1 0 487333388 72417280 15049 4294967295 134512640 134672761 3221224528 3221223632 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17680 15049 603 41 0 17639 0
vsize: 70720
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16165 0 0 0 22958 42 0 0 25 0 1 0 487333388 73220096 15266 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17876 15266 603 41 0 17835 0
vsize: 71504
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16313 0 0 0 23958 43 0 0 25 0 1 0 487333388 73895936 15414 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18041 15414 603 41 0 18000 0
vsize: 72164
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16383 0 0 0 24958 43 0 0 25 0 1 0 487333388 74153984 15484 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18104 15484 603 41 0 18063 0
vsize: 72416
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16398 0 0 0 25958 43 0 0 25 0 1 0 487333388 74272768 15499 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 15499 603 41 0 18092 0
vsize: 72532
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16414 0 0 0 26958 43 0 0 25 0 1 0 487333388 74272768 15515 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 15515 603 41 0 18092 0
vsize: 72532
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16435 0 0 0 27959 43 0 0 25 0 1 0 487333388 74399744 15536 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18164 15536 603 41 0 18123 0
vsize: 72656
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16501 0 0 0 28958 43 0 0 25 0 1 0 487333388 74641408 15602 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18223 15602 603 41 0 18182 0
vsize: 72892
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16561 0 0 0 29958 43 0 0 25 0 1 0 487333388 74907648 15662 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18288 15662 603 41 0 18247 0
vsize: 73152
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16689 0 0 0 30958 44 0 0 25 0 1 0 487333388 75444224 15790 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18419 15790 603 41 0 18378 0
vsize: 73676
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16790 0 0 0 31958 44 0 0 25 0 1 0 487333388 75976704 15891 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 15891 603 41 0 18508 0
vsize: 74196
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 16977 0 0 0 32957 45 0 0 25 0 1 0 487333388 76709888 16078 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18728 16078 603 41 0 18687 0
vsize: 74912
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 17221 0 0 0 33956 46 0 0 25 0 1 0 487333388 77774848 16322 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18988 16322 603 41 0 18947 0
vsize: 75952
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 17431 0 0 0 34955 47 0 0 25 0 1 0 487333388 78585856 16532 4294967295 134512640 134672761 3221224528 3221223632 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19186 16532 603 41 0 19145 0
vsize: 76744
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 17658 0 0 0 35954 48 0 0 25 0 1 0 487333388 79511552 16759 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19412 16759 603 41 0 19371 0
vsize: 77648
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 17931 0 0 0 36953 49 0 0 25 0 1 0 487333388 80728064 17032 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19709 17032 603 41 0 19668 0
vsize: 78836
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 18203 0 0 0 37952 50 0 0 25 0 1 0 487333388 81788928 17304 4294967295 134512640 134672761 3221224528 3221223680 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19968 17304 603 41 0 19927 0
vsize: 79872
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 18632 0 0 0 38951 51 0 0 25 0 1 0 487333388 83537920 17733 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20395 17733 603 41 0 20354 0
vsize: 81580
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 18928 0 0 0 39951 52 0 0 25 0 1 0 487333388 84754432 18029 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20692 18029 603 41 0 20651 0
vsize: 82768
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 19152 0 0 0 40950 52 0 0 25 0 1 0 487333388 85684224 18253 4294967295 134512640 134672761 3221224528 3221223632 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20919 18253 603 41 0 20878 0
vsize: 83676
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 19364 0 0 0 41950 53 0 0 25 0 1 0 487333388 86507520 18465 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21120 18465 603 41 0 21079 0
vsize: 84480
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 19630 0 0 0 42949 54 0 0 25 0 1 0 487333388 87580672 18731 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21382 18731 603 41 0 21341 0
vsize: 85528
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 19838 0 0 0 43948 55 0 0 25 0 1 0 487333388 88506368 18939 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21608 18939 603 41 0 21567 0
vsize: 86432
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 19972 0 0 0 44948 55 0 0 25 0 1 0 487333388 89051136 19073 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 19073 603 41 0 21700 0
vsize: 86964
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20012 0 0 0 45948 55 0 0 25 0 1 0 487333388 89186304 19113 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21774 19113 603 41 0 21733 0
vsize: 87096
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20106 0 0 0 46948 56 0 0 25 0 1 0 487333388 89583616 19207 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21871 19207 603 41 0 21830 0
vsize: 87484
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20232 0 0 0 47947 56 0 0 25 0 1 0 487333388 90124288 19333 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22003 19333 603 41 0 21962 0
vsize: 88012
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20298 0 0 0 48947 57 0 0 25 0 1 0 487333388 90394624 19399 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22069 19399 603 41 0 22028 0
vsize: 88276
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20363 0 0 0 49947 57 0 0 25 0 1 0 487333388 90664960 19464 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22135 19464 603 41 0 22094 0
vsize: 88540
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20395 0 0 0 50947 57 0 0 25 0 1 0 487333388 90804224 19496 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 19496 603 41 0 22128 0
vsize: 88676
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20412 0 0 0 51947 58 0 0 25 0 1 0 487333388 90804224 19513 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 19513 603 41 0 22128 0
vsize: 88676
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20423 0 0 0 52947 58 0 0 25 0 1 0 487333388 90804224 19524 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 19524 603 41 0 22128 0
vsize: 88676
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20453 0 0 0 53947 58 0 0 25 0 1 0 487333388 90939392 19554 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22202 19554 603 41 0 22161 0
vsize: 88808
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20473 0 0 0 54946 58 0 0 25 0 1 0 487333388 91074560 19574 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22235 19574 603 41 0 22194 0
vsize: 88940
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20499 0 0 0 55946 59 0 0 25 0 1 0 487333388 91209728 19600 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 19600 603 41 0 22227 0
vsize: 89072
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20522 0 0 0 56946 59 0 0 25 0 1 0 487333388 91209728 19623 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 19623 603 41 0 22227 0
vsize: 89072
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20552 0 0 0 57946 59 0 0 25 0 1 0 487333388 91344896 19653 4294967295 134512640 134672761 3221224528 3221223632 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22301 19653 603 41 0 22260 0
vsize: 89204
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20584 0 0 0 58946 59 0 0 25 0 1 0 487333388 91480064 19685 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22334 19685 603 41 0 22293 0
vsize: 89336
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20607 0 0 0 59945 60 0 0 25 0 1 0 487333388 91619328 19708 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22368 19708 603 41 0 22327 0
vsize: 89472
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20617 0 0 0 60945 60 0 0 25 0 1 0 487333388 91619328 19718 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22368 19718 603 41 0 22327 0
vsize: 89472
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20633 0 0 0 61945 60 0 0 25 0 1 0 487333388 91754496 19734 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22401 19734 603 41 0 22360 0
vsize: 89604
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20649 0 0 0 62945 61 0 0 25 0 1 0 487333388 91754496 19750 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22401 19750 603 41 0 22360 0
vsize: 89604
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20714 0 0 0 63944 61 0 0 25 0 1 0 487333388 92024832 19815 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22467 19815 603 41 0 22426 0
vsize: 89868
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 20911 0 0 0 64943 62 0 0 25 0 1 0 487333388 92831744 20012 4294967295 134512640 134672761 3221224528 3221223620 1075351193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22664 20012 603 41 0 22623 0
vsize: 90656
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 21135 0 0 0 65943 63 0 0 25 0 1 0 487333388 93761536 20236 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22891 20236 603 41 0 22850 0
vsize: 91564
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 21361 0 0 0 66942 64 0 0 25 0 1 0 487333388 94781440 20462 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23140 20462 603 41 0 23099 0
vsize: 92560
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 21615 0 0 0 67942 64 0 0 25 0 1 0 487333388 95842304 20716 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23399 20716 603 41 0 23358 0
vsize: 93596
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 21842 0 0 0 68941 65 0 0 25 0 1 0 487333388 96772096 20943 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23626 20943 603 41 0 23585 0
vsize: 94504
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 22030 0 0 0 69940 66 0 0 25 0 1 0 487333388 97427456 21131 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23786 21131 603 41 0 23745 0
vsize: 95144
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 22135 0 0 0 70940 66 0 0 25 0 1 0 487333388 97914880 21236 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23905 21236 603 41 0 23864 0
vsize: 95620
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8878
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 22190 0 0 0 71940 67 0 0 25 0 1 0 487333388 98168832 21291 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23967 21291 603 41 0 23926 0
vsize: 95868
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.93 3/57 8919
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 22372 0 0 0 72939 67 0 0 25 0 1 0 487333388 98934784 21473 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24154 21473 603 41 0 24113 0
vsize: 96616
[startup+740.021 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 22592 0 0 0 73938 68 0 0 25 0 1 0 487333388 99717120 21693 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24345 21693 603 41 0 24304 0
vsize: 97380
[startup+750.02 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 22834 0 0 0 74936 70 0 0 25 0 1 0 487333388 100777984 21935 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24604 21935 603 41 0 24563 0
vsize: 98416
[startup+760.021 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 23119 0 0 0 75935 71 0 0 25 0 1 0 487333388 101974016 22220 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24896 22220 603 41 0 24855 0
vsize: 99584
[startup+770.02 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 23363 0 0 0 76935 72 0 0 25 0 1 0 487333388 102887424 22464 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 22464 603 41 0 25078 0
vsize: 100476
[startup+780.021 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 23619 0 0 0 77934 73 0 0 25 0 1 0 487333388 103948288 22720 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25378 22720 603 41 0 25337 0
vsize: 101512
[startup+790.021 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 23908 0 0 0 78933 73 0 0 25 0 1 0 487333388 105140224 23009 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25669 23009 603 41 0 25628 0
vsize: 102676
[startup+800.021 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 8931
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 24182 0 0 0 79932 75 0 0 25 0 1 0 487333388 106315776 23283 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25956 23283 603 41 0 25915 0
vsize: 103824
[startup+810.021 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 24436 0 0 0 80932 75 0 0 25 0 1 0 487333388 107356160 23537 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26210 23537 603 41 0 26169 0
vsize: 104840
[startup+820.022 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 24736 0 0 0 81931 76 0 0 25 0 1 0 487333388 108552192 23837 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26502 23837 603 41 0 26461 0
vsize: 106008
[startup+830.022 s]
Raw data (loadavg): 1.09 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 24977 0 0 0 82930 77 0 0 25 0 1 0 487333388 109486080 24078 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26730 24078 603 41 0 26689 0
vsize: 106920
[startup+840.023 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 25236 0 0 0 83930 78 0 0 25 0 1 0 487333388 110534656 24337 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 24337 603 41 0 26945 0
vsize: 107944
[startup+850.023 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 25479 0 0 0 84929 79 0 0 25 0 1 0 487333388 111583232 24580 4294967295 134512640 134672761 3221224528 3221223664 134565054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27242 24580 603 41 0 27201 0
vsize: 108968
[startup+860.023 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 25708 0 0 0 85928 80 0 0 25 0 1 0 487333388 112504832 24809 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27467 24809 603 41 0 27426 0
vsize: 109868
[startup+870.023 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 25984 0 0 0 86927 81 0 0 25 0 1 0 487333388 113696768 25085 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27758 25085 603 41 0 27717 0
vsize: 111032
[startup+880.024 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 26244 0 0 0 87926 82 0 0 25 0 1 0 487333388 114737152 25345 4294967295 134512640 134672761 3221224528 3221223632 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28012 25345 603 41 0 27971 0
vsize: 112048
[startup+890.024 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 26538 0 0 0 88925 83 0 0 25 0 1 0 487333388 115908608 25639 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28298 25639 603 41 0 28257 0
vsize: 113192
[startup+900.024 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 26826 0 0 0 89925 84 0 0 25 0 1 0 487333388 117108736 25927 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28591 25927 603 41 0 28550 0
vsize: 114364
[startup+910.024 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 27029 0 0 0 90924 85 0 0 25 0 1 0 487333388 117886976 26130 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28781 26130 603 41 0 28740 0
vsize: 115124
[startup+920.024 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 27284 0 0 0 91924 86 0 0 25 0 1 0 487333388 118939648 26385 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29038 26385 603 41 0 28997 0
vsize: 116152
[startup+930.024 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 27599 0 0 0 92923 87 0 0 25 0 1 0 487333388 120266752 26700 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29362 26700 603 41 0 29321 0
vsize: 117448
[startup+940.024 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 27846 0 0 0 93922 88 0 0 25 0 1 0 487333388 121221120 26947 4294967295 134512640 134672761 3221224528 3221223484 1075350251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29595 26947 603 41 0 29554 0
vsize: 118380
[startup+950.025 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28101 0 0 0 94921 89 0 0 25 0 1 0 487333388 122269696 27202 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29851 27202 603 41 0 29810 0
vsize: 119404
[startup+960.026 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28295 0 0 0 95920 90 0 0 25 0 1 0 487333388 123084800 27396 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30050 27396 603 41 0 30009 0
vsize: 120200
[startup+970.026 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28330 0 0 0 96920 90 0 0 25 0 1 0 487333388 123219968 27431 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30083 27431 603 41 0 30042 0
vsize: 120332
[startup+980.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28380 0 0 0 97920 91 0 0 25 0 1 0 487333388 123490304 27481 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30149 27481 603 41 0 30108 0
vsize: 120596
[startup+990.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28419 0 0 0 98919 91 0 0 25 0 1 0 487333388 123625472 27520 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30182 27520 603 41 0 30141 0
vsize: 120728
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28435 0 0 0 99919 91 0 0 25 0 1 0 487333388 123760640 27536 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30215 27536 603 41 0 30174 0
vsize: 120860
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28464 0 0 0 100919 92 0 0 25 0 1 0 487333388 123760640 27565 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30215 27565 603 41 0 30174 0
vsize: 120860
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28498 0 0 0 101919 92 0 0 25 0 1 0 487333388 123887616 27599 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30246 27599 603 41 0 30205 0
vsize: 120984
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28529 0 0 0 102919 92 0 0 25 0 1 0 487333388 124022784 27630 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30279 27630 603 41 0 30238 0
vsize: 121116
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28559 0 0 0 103919 93 0 0 25 0 1 0 487333388 124149760 27660 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30310 27660 603 41 0 30269 0
vsize: 121240
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28579 0 0 0 104919 93 0 0 25 0 1 0 487333388 124280832 27680 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30342 27680 603 41 0 30301 0
vsize: 121368
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28601 0 0 0 105919 93 0 0 25 0 1 0 487333388 124399616 27702 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30371 27702 603 41 0 30330 0
vsize: 121484
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28619 0 0 0 106919 93 0 0 25 0 1 0 487333388 124399616 27720 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30371 27720 603 41 0 30330 0
vsize: 121484
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8933
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28646 0 0 0 107919 94 0 0 25 0 1 0 487333388 124526592 27747 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30402 27747 603 41 0 30361 0
vsize: 121608
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28662 0 0 0 108918 94 0 0 25 0 1 0 487333388 124661760 27763 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 27763 603 41 0 30394 0
vsize: 121740
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28677 0 0 0 109918 94 0 0 25 0 1 0 487333388 124661760 27778 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 27778 603 41 0 30394 0
vsize: 121740
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28702 0 0 0 110918 95 0 0 25 0 1 0 487333388 124780544 27803 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30464 27803 603 41 0 30423 0
vsize: 121856
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28726 0 0 0 111918 95 0 0 25 0 1 0 487333388 124919808 27827 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30498 27827 603 41 0 30457 0
vsize: 121992
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28743 0 0 0 112918 95 0 0 25 0 1 0 487333388 124919808 27844 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30498 27844 603 41 0 30457 0
vsize: 121992
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28761 0 0 0 113918 95 0 0 25 0 1 0 487333388 125054976 27862 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30531 27862 603 41 0 30490 0
vsize: 122124
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28779 0 0 0 114918 95 0 0 25 0 1 0 487333388 125054976 27880 4294967295 134512640 134672761 3221224528 3221223632 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30531 27880 603 41 0 30490 0
vsize: 122124
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28803 0 0 0 115918 96 0 0 25 0 1 0 487333388 125186048 27904 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30563 27904 603 41 0 30522 0
vsize: 122252
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28821 0 0 0 116918 96 0 0 25 0 1 0 487333388 125325312 27922 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30597 27922 603 41 0 30556 0
vsize: 122388
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28851 0 0 0 117918 96 0 0 25 0 1 0 487333388 125460480 27952 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30630 27952 603 41 0 30589 0
vsize: 122520
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28883 0 0 0 118918 97 0 0 25 0 1 0 487333388 125579264 27984 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30659 27984 603 41 0 30618 0
vsize: 122636
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8935
Raw data (stat): 8878 (minisat+) R 8877 29151 29150 0 -1 0 28920 0 0 0 119917 97 0 0 25 0 1 0 487333388 125714432 28021 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30692 28021 603 41 0 30651 0
vsize: 122768
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 8935
Raw data (stat): 8878 (minisat+) Z 8877 29151 29150 0 -1 12 28922 0 0 0 119917 102 0 0 23 0 1 0 487333388 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.11
CPU time (s): 1200.21
CPU user time (s): 1199.18
CPU system time (s): 1.02984
CPU usage (%): 100.008
Max. virtual memory (Kb): 122768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####