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 15138

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        696192 kB
Buffers:          7656 kB
Cached:         303476 kB
SwapCached:        104 kB
Active:          51256 kB
Inactive:       262272 kB
HighTotal:      131008 kB
HighFree:        40348 kB
LowTotal:       903652 kB
LowFree:        655844 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19420 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:20:58 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 18486 7 1200.31 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]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
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]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  123819   394251 |   41273       0        0     nan |  0.000 % |
c |       100 |  123689   393805 |   45400      82     1033    12.6 |  0.582 % |
c |       250 |  123611   393519 |   49940     223    12255    55.0 |  0.635 % |
c |       476 |  123592   393454 |   54934     446    25868    58.0 |  0.651 % |
c |       813 |  123592   393454 |   60427     783    31769    40.6 |  0.651 % |
c |      1319 |  122327   388987 |   66470    1056    36336    34.4 |  1.522 % |
c |      2078 |  122067   388081 |   73117    1773    50521    28.5 |  1.722 % |
c |      3217 |  122033   387971 |   80429    2908   115105    39.6 |  1.750 % |
c |      4925 |  121872   387428 |   88472    4589   198107    43.2 |  1.864 % |
c |      7487 |  121369   385669 |   97319    7065   281333    39.8 |  2.222 % |
c |     11331 |  121046   384558 |  107051   10860   383375    35.3 |  2.446 % |
c |     17097 |  120433   382447 |  117756   16530   595557    36.0 |  2.816 % |
c |     25746 |  120172   381574 |  129532   25104  1198644    47.7 |  2.979 % |
c |     38722 |  120096   381316 |  142485   38063  3051886    80.2 |  3.020 % |
c |     58183 |  119808   380306 |  156734   57411  5055291    88.1 |  3.158 % |
c |     87381 |  119754   380120 |  172407   86599 15798491   182.4 |  3.183 % |
c |    131170 |  119668   379828 |  189648  130372 30883892   236.9 |  3.228 % |
#### 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.98 0.94 2/54 15068
Raw data (stat): 15068 (runsolver) R 15067 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541680333 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.0002 s]
Raw data (loadavg): 0.93 0.98 0.94 2/54 15068
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 4361 0 0 0 987 11 0 0 25 0 1 0 541680333 19894272 3997 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4857 3997 603 41 0 4816 0
vsize: 19428
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 4566 0 0 0 1985 12 0 0 25 0 1 0 541680333 20840448 4202 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5088 4202 603 41 0 5047 0
vsize: 20352
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 4675 0 0 0 2984 13 0 0 25 0 1 0 541680333 21295104 4311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5199 4311 603 41 0 5158 0
vsize: 20796
[startup+40.001 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 4831 0 0 0 3984 13 0 0 25 0 1 0 541680333 21835776 4467 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5331 4467 603 41 0 5290 0
vsize: 21324
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 5000 0 0 0 4984 14 0 0 25 0 1 0 541680333 22495232 4636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5492 4636 603 41 0 5451 0
vsize: 21968
[startup+60.0014 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 5270 0 0 0 5983 14 0 0 25 0 1 0 541680333 23732224 4906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5794 4906 603 41 0 5753 0
vsize: 23176
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 5606 0 0 0 6982 16 0 0 25 0 1 0 541680333 25079808 5242 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6123 5242 603 41 0 6082 0
vsize: 24492
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 6067 0 0 0 7981 17 0 0 25 0 1 0 541680333 26972160 5703 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6585 5703 603 41 0 6544 0
vsize: 26340
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 6665 0 0 0 8979 19 0 0 25 0 1 0 541680333 29392896 6301 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7176 6301 603 41 0 7135 0
vsize: 28704
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 7165 0 0 0 9978 21 0 0 25 0 1 0 541680333 31539200 6801 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7700 6801 603 41 0 7659 0
vsize: 30800
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 7474 0 0 0 10977 21 0 0 25 0 1 0 541680333 32874496 7110 4294967295 134512640 134672761 3221224544 3221223728 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8026 7110 603 41 0 7985 0
vsize: 32104
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 7841 0 0 0 11976 22 0 0 25 0 1 0 541680333 34336768 7477 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8383 7477 603 41 0 8342 0
vsize: 33532
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 8218 0 0 0 12975 24 0 0 25 0 1 0 541680333 35807232 7854 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8742 7854 603 41 0 8701 0
vsize: 34968
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 8643 0 0 0 13974 25 0 0 25 0 1 0 541680333 37552128 8279 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9168 8279 603 41 0 9127 0
vsize: 36672
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 8942 0 0 0 14974 25 0 0 25 0 1 0 541680333 38764544 8578 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9464 8578 603 41 0 9423 0
vsize: 37856
[startup+160.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 9102 0 0 0 15973 26 0 0 25 0 1 0 541680333 39436288 8738 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9628 8738 603 41 0 9587 0
vsize: 38512
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 9332 0 0 0 16973 26 0 0 25 0 1 0 541680333 40357888 8968 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9853 8968 603 41 0 9812 0
vsize: 39412
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 9690 0 0 0 17972 28 0 0 25 0 1 0 541680333 41844736 9326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10216 9326 603 41 0 10175 0
vsize: 40864
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 9939 0 0 0 18971 29 0 0 25 0 1 0 541680333 42782720 9575 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10445 9575 603 41 0 10404 0
vsize: 41780
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 10467 0 0 0 19969 31 0 0 25 0 1 0 541680333 44941312 10103 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10972 10103 603 41 0 10931 0
vsize: 43888
[startup+210.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 10993 0 0 0 20968 32 0 0 25 0 1 0 541680333 47091712 10629 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11497 10629 603 41 0 11456 0
vsize: 45988
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 11483 0 0 0 21968 33 0 0 25 0 1 0 541680333 49102848 11119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11988 11119 603 41 0 11947 0
vsize: 47952
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 11957 0 0 0 22967 34 0 0 25 0 1 0 541680333 51384320 11593 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12545 11593 603 41 0 12504 0
vsize: 50180
[startup+240.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 12318 0 0 0 23966 34 0 0 25 0 1 0 541680333 52736000 11954 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12875 11954 603 41 0 12834 0
vsize: 51500
[startup+250.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 12588 0 0 0 24966 35 0 0 25 0 1 0 541680333 53932032 12224 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13167 12224 603 41 0 13126 0
vsize: 52668
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 12872 0 0 0 25966 36 0 0 25 0 1 0 541680333 54992896 12508 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13426 12508 603 41 0 13385 0
vsize: 53704
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 13301 0 0 0 26965 36 0 0 25 0 1 0 541680333 56729600 12937 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13850 12937 603 41 0 13809 0
vsize: 55400
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 14089 0 0 0 27964 37 0 0 25 0 1 0 541680333 59981824 13725 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13725 603 41 0 14603 0
vsize: 58576
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 14835 0 0 0 28962 39 0 0 25 0 1 0 541680333 63090688 14471 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14471 603 41 0 15362 0
vsize: 61612
[startup+300.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 15505 0 0 0 29960 41 0 0 25 0 1 0 541680333 65794048 15141 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16063 15141 603 41 0 16022 0
vsize: 64252
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 16002 0 0 0 30960 42 0 0 25 0 1 0 541680333 67825664 15638 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16559 15638 603 41 0 16518 0
vsize: 66236
[startup+320.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15070
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 16477 0 0 0 31958 44 0 0 25 0 1 0 541680333 69840896 16113 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17051 16113 603 41 0 17010 0
vsize: 68204
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 17018 0 0 0 32957 45 0 0 25 0 1 0 541680333 72019968 16654 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17583 16654 603 41 0 17542 0
vsize: 70332
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 17607 0 0 0 33957 46 0 0 25 0 1 0 541680333 74452992 17243 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18177 17243 603 41 0 18136 0
vsize: 72708
[startup+350.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 18133 0 0 0 34955 48 0 0 25 0 1 0 541680333 76607488 17769 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18703 17769 603 41 0 18662 0
vsize: 74812
[startup+360.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 18647 0 0 0 35954 49 0 0 25 0 1 0 541680333 78635008 18283 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19198 18283 603 41 0 19157 0
vsize: 76792
[startup+370.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 19171 0 0 0 36952 51 0 0 25 0 1 0 541680333 80801792 18807 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19727 18807 603 41 0 19686 0
vsize: 78908
[startup+380.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 19671 0 0 0 37952 52 0 0 25 0 1 0 541680333 82837504 19307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20224 19307 603 41 0 20183 0
vsize: 80896
[startup+390.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 20183 0 0 0 38951 52 0 0 25 0 1 0 541680333 85000192 19819 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20752 19819 603 41 0 20711 0
vsize: 83008
[startup+400.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 20737 0 0 0 39950 54 0 0 25 0 1 0 541680333 87289856 20373 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21311 20373 603 41 0 21270 0
vsize: 85244
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 21258 0 0 0 40948 56 0 0 25 0 1 0 541680333 89444352 20894 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21837 20894 603 41 0 21796 0
vsize: 87348
[startup+420.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 21913 0 0 0 41946 57 0 0 25 0 1 0 541680333 91992064 21549 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22459 21549 603 41 0 22418 0
vsize: 89836
[startup+430.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 22509 0 0 0 42945 59 0 0 25 0 1 0 541680333 94527488 22145 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23078 22145 603 41 0 23037 0
vsize: 92312
[startup+440.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 23112 0 0 0 43943 61 0 0 25 0 1 0 541680333 96927744 22748 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23664 22748 603 41 0 23623 0
vsize: 94656
[startup+450.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 23718 0 0 0 44943 62 0 0 25 0 1 0 541680333 99487744 23354 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24289 23354 603 41 0 24248 0
vsize: 97156
[startup+460.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 24294 0 0 0 45941 63 0 0 25 0 1 0 541680333 101756928 23930 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24843 23930 603 41 0 24802 0
vsize: 99372
[startup+470.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 24825 0 0 0 46940 64 0 0 25 0 1 0 541680333 103923712 24461 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25372 24461 603 41 0 25331 0
vsize: 101488
[startup+480.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 25351 0 0 0 47939 66 0 0 25 0 1 0 541680333 106065920 24987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25895 24987 603 41 0 25854 0
vsize: 103580
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 25860 0 0 0 48938 68 0 0 25 0 1 0 541680333 108220416 25496 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26421 25496 603 41 0 26380 0
vsize: 105684
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 26417 0 0 0 49937 68 0 0 25 0 1 0 541680333 110514176 26053 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26981 26053 603 41 0 26940 0
vsize: 107924
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 26907 0 0 0 50936 70 0 0 25 0 1 0 541680333 112545792 26543 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27477 26543 603 41 0 27436 0
vsize: 109908
[startup+520.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 27473 0 0 0 51934 72 0 0 25 0 1 0 541680333 114839552 27109 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28037 27109 603 41 0 27996 0
vsize: 112148
[startup+530.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 27935 0 0 0 52933 73 0 0 25 0 1 0 541680333 116727808 27571 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28498 27571 603 41 0 28457 0
vsize: 113992
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 28413 0 0 0 53932 74 0 0 25 0 1 0 541680333 118759424 28049 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28994 28049 603 41 0 28953 0
vsize: 115976
[startup+550.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 28893 0 0 0 54931 75 0 0 25 0 1 0 541680333 120659968 28529 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29458 28529 603 41 0 29417 0
vsize: 117832
[startup+560.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 29370 0 0 0 55931 76 0 0 25 0 1 0 541680333 122695680 29006 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29955 29006 603 41 0 29914 0
vsize: 119820
[startup+570.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 29885 0 0 0 56930 76 0 0 25 0 1 0 541680333 124723200 29521 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30450 29521 603 41 0 30409 0
vsize: 121800
[startup+580.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 30359 0 0 0 57930 77 0 0 25 0 1 0 541680333 126656512 29995 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30922 29995 603 41 0 30881 0
vsize: 123688
[startup+590.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 30914 0 0 0 58929 78 0 0 25 0 1 0 541680333 128974848 30550 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31488 30550 603 41 0 31447 0
vsize: 125952
[startup+600.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 31490 0 0 0 59928 80 0 0 25 0 1 0 541680333 131411968 31126 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32083 31126 603 41 0 32042 0
vsize: 128332
[startup+610.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 31997 0 0 0 60926 81 0 0 25 0 1 0 541680333 133423104 31633 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32574 31633 603 41 0 32533 0
vsize: 130296
[startup+620.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 32427 0 0 0 61925 83 0 0 25 0 1 0 541680333 135159808 32063 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32998 32063 603 41 0 32957 0
vsize: 131992
[startup+630.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 32819 0 0 0 62924 84 0 0 25 0 1 0 541680333 136777728 32455 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33393 32455 603 41 0 33352 0
vsize: 133572
[startup+640.011 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 33147 0 0 0 63924 84 0 0 25 0 1 0 541680333 138113024 32783 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33719 32783 603 41 0 33678 0
vsize: 134876
[startup+650.011 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 33626 0 0 0 64923 86 0 0 25 0 1 0 541680333 140128256 33262 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34211 33262 603 41 0 34170 0
vsize: 136844
[startup+660.01 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 33989 0 0 0 65922 87 0 0 25 0 1 0 541680333 141602816 33625 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34571 33625 603 41 0 34530 0
vsize: 138284
[startup+670.011 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 34410 0 0 0 66921 88 0 0 25 0 1 0 541680333 143347712 34046 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34997 34046 603 41 0 34956 0
vsize: 139988
[startup+680.011 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 34863 0 0 0 67920 89 0 0 25 0 1 0 541680333 145092608 34499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35423 34499 603 41 0 35382 0
vsize: 141692
[startup+690.012 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 35321 0 0 0 68919 90 0 0 25 0 1 0 541680333 146972672 34957 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35882 34957 603 41 0 35841 0
vsize: 143528
[startup+700.012 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 35726 0 0 0 69918 91 0 0 25 0 1 0 541680333 148717568 35362 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36308 35362 603 41 0 36267 0
vsize: 145232
[startup+710.012 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 36033 0 0 0 70918 92 0 0 25 0 1 0 541680333 149934080 35669 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36605 35669 603 41 0 36564 0
vsize: 146420
[startup+720.012 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 36279 0 0 0 71917 92 0 0 25 0 1 0 541680333 150880256 35915 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36836 35915 603 41 0 36795 0
vsize: 147344
[startup+730.012 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 36557 0 0 0 72916 94 0 0 25 0 1 0 541680333 152072192 36193 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37127 36193 603 41 0 37086 0
vsize: 148508
[startup+740.013 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 36806 0 0 0 73916 94 0 0 25 0 1 0 541680333 153542656 36442 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37486 36442 603 41 0 37445 0
vsize: 149944
[startup+750.013 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 37237 0 0 0 74915 95 0 0 25 0 1 0 541680333 155410432 36873 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37942 36873 603 41 0 37901 0
vsize: 151768
[startup+760.013 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 37726 0 0 0 75914 97 0 0 25 0 1 0 541680333 157425664 37362 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38434 37362 603 41 0 38393 0
vsize: 153736
[startup+770.013 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 38496 0 0 0 76913 98 0 0 25 0 1 0 541680333 160526336 38132 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39191 38132 603 41 0 39150 0
vsize: 156764
[startup+780.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 39169 0 0 0 77911 99 0 0 25 0 1 0 541680333 163225600 38805 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39850 38805 603 41 0 39809 0
vsize: 159400
[startup+790.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 39839 0 0 0 78911 100 0 0 25 0 1 0 541680333 165933056 39475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40511 39475 603 41 0 40470 0
vsize: 162044
[startup+800.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 40452 0 0 0 79909 102 0 0 25 0 1 0 541680333 168493056 40088 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41136 40088 603 41 0 41095 0
vsize: 164544
[startup+810.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 41124 0 0 0 80907 104 0 0 25 0 1 0 541680333 171208704 40760 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41799 40760 603 41 0 41758 0
vsize: 167196
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 41775 0 0 0 81906 105 0 0 25 0 1 0 541680333 173924352 41411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42462 41411 603 41 0 42421 0
vsize: 169848
[startup+830.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 42388 0 0 0 82904 107 0 0 25 0 1 0 541680333 176361472 42024 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43057 42024 603 41 0 43016 0
vsize: 172228
[startup+840.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 42979 0 0 0 83904 108 0 0 25 0 1 0 541680333 178823168 42615 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43658 42615 603 41 0 43617 0
vsize: 174632
[startup+850.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 43580 0 0 0 84903 109 0 0 25 0 1 0 541680333 181264384 43216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44254 43216 603 41 0 44213 0
vsize: 177016
[startup+860.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 44016 0 0 0 85902 110 0 0 25 0 1 0 541680333 183144448 43652 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44713 43652 603 41 0 44672 0
vsize: 178852
[startup+870.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 44545 0 0 0 86901 112 0 0 25 0 1 0 541680333 185298944 44181 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45239 44181 603 41 0 45198 0
vsize: 180956
[startup+880.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 44990 0 0 0 87900 113 0 0 25 0 1 0 541680333 187047936 44626 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45666 44626 603 41 0 45625 0
vsize: 182664
[startup+890.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 45439 0 0 0 88899 114 0 0 25 0 1 0 541680333 188936192 45075 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46127 45075 603 41 0 46086 0
vsize: 184508
[startup+900.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 45913 0 0 0 89899 115 0 0 25 0 1 0 541680333 190816256 45549 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46586 45549 603 41 0 46545 0
vsize: 186344
[startup+910.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 46444 0 0 0 90898 116 0 0 25 0 1 0 541680333 192954368 46080 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47108 46080 603 41 0 47067 0
vsize: 188432
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 47013 0 0 0 91896 118 0 0 25 0 1 0 541680333 195366912 46649 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47697 46649 603 41 0 47656 0
vsize: 190788
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 47461 0 0 0 92895 119 0 0 25 0 1 0 541680333 197107712 47097 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48122 47097 603 41 0 48081 0
vsize: 192488
[startup+940.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 47872 0 0 0 93894 120 0 0 25 0 1 0 541680333 198856704 47508 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48549 47508 603 41 0 48508 0
vsize: 194196
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 48311 0 0 0 94893 121 0 0 25 0 1 0 541680333 200581120 47947 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48970 47947 603 41 0 48929 0
vsize: 195880
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 48810 0 0 0 95892 122 0 0 25 0 1 0 541680333 202600448 48446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49463 48446 603 41 0 49422 0
vsize: 197852
[startup+970.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 49195 0 0 0 96892 123 0 0 25 0 1 0 541680333 204222464 48831 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49859 48831 603 41 0 49818 0
vsize: 199436
[startup+980.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 49458 0 0 0 97891 124 0 0 25 0 1 0 541680333 205303808 49094 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50123 49094 603 41 0 50082 0
vsize: 200492
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 49533 0 0 0 98891 124 0 0 25 0 1 0 541680333 205570048 49169 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50188 49169 603 41 0 50147 0
vsize: 200752
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 49821 0 0 0 99890 125 0 0 25 0 1 0 541680333 206786560 49457 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50485 49457 603 41 0 50444 0
vsize: 201940
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 50130 0 0 0 100889 126 0 0 25 0 1 0 541680333 208003072 49766 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50782 49766 603 41 0 50741 0
vsize: 203128
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 50601 0 0 0 101888 127 0 0 25 0 1 0 541680333 210010112 50237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51272 50237 603 41 0 51231 0
vsize: 205088
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 50943 0 0 0 102888 128 0 0 25 0 1 0 541680333 211341312 50579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51597 50579 603 41 0 51556 0
vsize: 206388
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 51485 0 0 0 103886 130 0 0 25 0 1 0 541680333 213618688 51121 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52153 51122 603 41 0 52112 0
vsize: 208612
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 51820 0 0 0 104885 131 0 0 25 0 1 0 541680333 214970368 51456 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52483 51456 603 41 0 52442 0
vsize: 209932
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 52070 0 0 0 105885 132 0 0 25 0 1 0 541680333 215896064 51706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52709 51706 603 41 0 52668 0
vsize: 210836
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 52437 0 0 0 106884 133 0 0 25 0 1 0 541680333 217395200 52073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53075 52073 603 41 0 53034 0
vsize: 212300
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 52898 0 0 0 107883 134 0 0 25 0 1 0 541680333 219385856 52534 4294967295 134512640 134672761 3221224544 3221223648 134560322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53561 52534 603 41 0 53520 0
vsize: 214244
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 53207 0 0 0 108883 134 0 0 25 0 1 0 541680333 220585984 52843 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53854 52843 603 41 0 53813 0
vsize: 215416
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 53309 0 0 0 109883 134 0 0 25 0 1 0 541680333 220991488 52945 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53953 52945 603 41 0 53912 0
vsize: 215812
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 53344 0 0 0 110883 135 0 0 25 0 1 0 541680333 221126656 52980 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53986 52980 603 41 0 53945 0
vsize: 215944
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 53666 0 0 0 111882 136 0 0 25 0 1 0 541680333 222461952 53302 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54312 53302 603 41 0 54271 0
vsize: 217248
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 54122 0 0 0 112881 137 0 0 25 0 1 0 541680333 224333824 53758 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54769 53758 603 41 0 54728 0
vsize: 219076
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 54515 0 0 0 113881 138 0 0 25 0 1 0 541680333 225951744 54151 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55164 54151 603 41 0 55123 0
vsize: 220656
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 54856 0 0 0 114881 138 0 0 25 0 1 0 541680333 227409920 54492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55520 54492 603 41 0 55479 0
vsize: 222080
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 55177 0 0 0 115880 139 0 0 25 0 1 0 541680333 228601856 54813 4294967295 134512640 134672761 3221224544 3221223696 134559753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55811 54813 603 41 0 55770 0
vsize: 223244
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 55547 0 0 0 116880 140 0 0 25 0 1 0 541680333 230182912 55183 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56197 55183 603 41 0 56156 0
vsize: 224788
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 55895 0 0 0 117879 140 0 0 25 0 1 0 541680333 231620608 55531 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56548 55531 603 41 0 56507 0
vsize: 226192
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 56229 0 0 0 118879 141 0 0 25 0 1 0 541680333 232919040 55865 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56865 55865 603 41 0 56824 0
vsize: 227460
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15072
Raw data (stat): 15068 (minisat+) R 15067 10614 10613 0 -1 0 56524 0 0 0 119879 141 0 0 25 0 1 0 541680333 234233856 56160 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57186 56160 603 41 0 57145 0
vsize: 228744
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 15072
Raw data (stat): 15068 (minisat+) Z 15067 10614 10613 0 -1 12 56526 0 0 0 119879 151 0 0 25 0 1 0 541680333 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.31
CPU user time (s): 1198.79
CPU system time (s): 1.51977
CPU usage (%): 100.015
Max. virtual memory (Kb): 228744
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####