PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-l152lav.opb
MD5SUM	9d4ce12b138a2bef65a1f401ec9d1f01
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4742
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.33
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 16445

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 07:13:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13486 boxname=wulflinc31 idbench=1038 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9d4ce12b138a2bef65a1f401ec9d1f01  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 13486
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        659800 kB
Buffers:         29620 kB
Cached:         317524 kB
SwapCached:        540 kB
Active:         114204 kB
Inactive:       234948 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        659548 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20112 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:33:40 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 13486 7 1200.28 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 |   97077   314005 |   32359       0        0     nan |  0.000 % |
c |       100 |   96947   313559 |   35594      82     1270    15.5 |  0.582 % |
c |       251 |   96883   313337 |   39154     212    15944    75.2 |  0.639 % |
c |       476 |   96883   313337 |   43069     437    24593    56.3 |  0.639 % |
c |       813 |   96398   311624 |   47376     699    28796    41.2 |  0.981 % |
c |      1320 |   96280   311210 |   52114    1189    64686    54.4 |  1.062 % |
c |      2079 |   96249   311105 |   57325    1943    92323    47.5 |  1.079 % |
c |      3223 |   96179   310853 |   63058    3077   320979   104.3 |  1.123 % |
c |      4931 |   96005   310207 |   69364    4745   498190   105.0 |  1.229 % |
c |      7493 |   95381   308039 |   76300    7204   629523    87.4 |  1.673 % |
c |     11337 |   94537   305108 |   83930   10849   722117    66.6 |  2.263 % |
c |     17103 |   94126   303709 |   92324   16521   986489    59.7 |  2.520 % |
c |     25752 |   93634   301995 |  101556   25094  1804121    71.9 |  2.821 % |
c |     38728 |   93305   300886 |  111712   38012  3779797    99.4 |  3.028 % |
c |     58192 |   93290   300833 |  122883   57465  9794628   170.4 |  3.032 % |
c |     87386 |   93201   300510 |  135171   86640 15885253   183.3 |  3.085 % |
c |    131175 |   93099   300164 |  148688  130408 28212586   216.3 |  3.150 % |
c |    196860 |   92835   299270 |  163557   74455 14452111   194.1 |  3.289 % |
#### 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.93 0.97 0.91 2/54 24189
Raw data (stat): 24189 (runsolver) R 24188 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543177929 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0008 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 4342 0 0 0 989 9 0 0 25 0 1 0 543177929 20004864 3978 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4884 3978 603 41 0 4843 0
vsize: 19536
[startup+20.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 4688 0 0 0 1988 9 0 0 25 0 1 0 543177929 21487616 4324 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5246 4324 603 41 0 5205 0
vsize: 20984
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 4829 0 0 0 2988 10 0 0 25 0 1 0 543177929 22028288 4465 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5378 4465 603 41 0 5337 0
vsize: 21512
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 4954 0 0 0 3987 11 0 0 25 0 1 0 543177929 22564864 4590 4294967295 134512640 134672761 3221224624 3221223824 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5509 4590 603 41 0 5468 0
vsize: 22036
[startup+50.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 5196 0 0 0 4986 12 0 0 25 0 1 0 543177929 23502848 4832 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5738 4832 603 41 0 5697 0
vsize: 22952
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 5597 0 0 0 5984 14 0 0 25 0 1 0 543177929 25260032 5233 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6167 5233 603 41 0 6126 0
vsize: 24668
[startup+70.0047 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 5951 0 0 0 6983 15 0 0 25 0 1 0 543177929 26607616 5587 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6496 5587 603 41 0 6455 0
vsize: 25984
[startup+80.0052 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 6251 0 0 0 7982 16 0 0 25 0 1 0 543177929 27820032 5887 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6792 5887 603 41 0 6751 0
vsize: 27168
[startup+90.0052 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 6745 0 0 0 8981 18 0 0 25 0 1 0 543177929 29962240 6381 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6381 603 41 0 7274 0
vsize: 29260
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 7420 0 0 0 9980 19 0 0 25 0 1 0 543177929 32677888 7056 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7978 7056 603 41 0 7937 0
vsize: 31912
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 7669 0 0 0 10978 20 0 0 25 0 1 0 543177929 33742848 7305 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8238 7305 603 41 0 8197 0
vsize: 32952
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 8153 0 0 0 11977 22 0 0 25 0 1 0 543177929 35741696 7789 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8726 7789 603 41 0 8685 0
vsize: 34904
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 8566 0 0 0 12975 24 0 0 25 0 1 0 543177929 37486592 8202 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9152 8202 603 41 0 9111 0
vsize: 36608
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 9121 0 0 0 13973 26 0 0 25 0 1 0 543177929 39768064 8757 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9709 8757 603 41 0 9668 0
vsize: 38836
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 9712 0 0 0 14971 28 0 0 25 0 1 0 543177929 42180608 9348 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10298 9348 603 41 0 10257 0
vsize: 41192
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 10258 0 0 0 15970 30 0 0 25 0 1 0 543177929 44335104 9894 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10824 9894 603 41 0 10783 0
vsize: 43296
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 10772 0 0 0 16968 32 0 0 25 0 1 0 543177929 46485504 10408 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10408 603 41 0 11308 0
vsize: 45396
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 11262 0 0 0 17966 33 0 0 25 0 1 0 543177929 48504832 10898 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11842 10898 603 41 0 11801 0
vsize: 47368
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 11702 0 0 0 18965 35 0 0 25 0 1 0 543177929 50253824 11338 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12269 11338 603 41 0 12228 0
vsize: 49076
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 12132 0 0 0 19963 37 0 0 25 0 1 0 543177929 51982336 11768 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12691 11768 603 41 0 12650 0
vsize: 50764
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 12473 0 0 0 20963 37 0 0 25 0 1 0 543177929 53452800 12109 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13050 12109 603 41 0 13009 0
vsize: 52200
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 12810 0 0 0 21962 39 0 0 25 0 1 0 543177929 54779904 12446 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13374 12446 603 41 0 13333 0
vsize: 53496
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 13119 0 0 0 22960 40 0 0 25 0 1 0 543177929 56111104 12755 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13699 12755 603 41 0 13658 0
vsize: 54796
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 13478 0 0 0 23959 41 0 0 25 0 1 0 543177929 57581568 13114 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14058 13114 603 41 0 14017 0
vsize: 56232
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 13860 0 0 0 24959 42 0 0 25 0 1 0 543177929 59052032 13496 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14417 13496 603 41 0 14376 0
vsize: 57668
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 14331 0 0 0 25957 44 0 0 25 0 1 0 543177929 61071360 13967 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14910 13967 603 41 0 14869 0
vsize: 59640
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 14747 0 0 0 26956 45 0 0 25 0 1 0 543177929 62693376 14383 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14383 603 41 0 15265 0
vsize: 61224
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 15198 0 0 0 27955 47 0 0 25 0 1 0 543177929 64585728 14834 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15768 14834 603 41 0 15727 0
vsize: 63072
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 15666 0 0 0 28953 48 0 0 25 0 1 0 543177929 66465792 15302 4294967295 134512640 134672761 3221224624 3221223728 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16227 15302 603 41 0 16186 0
vsize: 64908
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 16131 0 0 0 29952 50 0 0 25 0 1 0 543177929 68612096 15767 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16751 15767 603 41 0 16710 0
vsize: 67004
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 16542 0 0 0 30951 51 0 0 25 0 1 0 543177929 70234112 16178 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17147 16178 603 41 0 17106 0
vsize: 68588
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 16842 0 0 0 31950 53 0 0 25 0 1 0 543177929 71565312 16478 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17472 16478 603 41 0 17431 0
vsize: 69888
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 17292 0 0 0 32948 54 0 0 25 0 1 0 543177929 73293824 16928 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17894 16928 603 41 0 17853 0
vsize: 71576
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 17817 0 0 0 33946 56 0 0 25 0 1 0 543177929 75440128 17453 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18418 17453 603 41 0 18377 0
vsize: 73672
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 18284 0 0 0 34944 58 0 0 25 0 1 0 543177929 77455360 17920 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18910 17920 603 41 0 18869 0
vsize: 75640
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 18760 0 0 0 35943 60 0 0 25 0 1 0 543177929 79331328 18396 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19368 18396 603 41 0 19327 0
vsize: 77472
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 19239 0 0 0 36942 61 0 0 25 0 1 0 543177929 81346560 18875 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19860 18875 603 41 0 19819 0
vsize: 79440
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 19664 0 0 0 37941 62 0 0 25 0 1 0 543177929 83083264 19300 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20284 19300 603 41 0 20243 0
vsize: 81136
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 20114 0 0 0 38940 63 0 0 25 0 1 0 543177929 84828160 19750 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20710 19750 603 41 0 20669 0
vsize: 82840
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 20588 0 0 0 39938 65 0 0 25 0 1 0 543177929 86835200 20224 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21200 20224 603 41 0 21159 0
vsize: 84800
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 20935 0 0 0 40936 67 0 0 25 0 1 0 543177929 88178688 20571 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21528 20571 603 41 0 21487 0
vsize: 86112
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 21314 0 0 0 41936 68 0 0 25 0 1 0 543177929 89796608 20950 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21923 20950 603 41 0 21882 0
vsize: 87692
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 21749 0 0 0 42935 69 0 0 25 0 1 0 543177929 91533312 21385 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22347 21385 603 41 0 22306 0
vsize: 89388
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 22254 0 0 0 43934 70 0 0 25 0 1 0 543177929 93540352 21890 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22837 21890 603 41 0 22796 0
vsize: 91348
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 22794 0 0 0 44932 72 0 0 25 0 1 0 543177929 95821824 22430 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23394 22430 603 41 0 23353 0
vsize: 93576
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 23313 0 0 0 45931 73 0 0 25 0 1 0 543177929 97939456 22949 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23911 22949 603 41 0 23870 0
vsize: 95644
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 23782 0 0 0 46929 75 0 0 25 0 1 0 543177929 99790848 23418 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24363 23418 603 41 0 24322 0
vsize: 97452
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 24135 0 0 0 47928 76 0 0 25 0 1 0 543177929 101240832 23771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24717 23771 603 41 0 24676 0
vsize: 98868
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 24478 0 0 0 48928 77 0 0 25 0 1 0 543177929 102690816 24114 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25071 24114 603 41 0 25030 0
vsize: 100284
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 24799 0 0 0 49927 78 0 0 25 0 1 0 543177929 104034304 24435 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25399 24435 603 41 0 25358 0
vsize: 101596
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 25232 0 0 0 50926 79 0 0 25 0 1 0 543177929 105762816 24868 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25821 24868 603 41 0 25780 0
vsize: 103284
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 25722 0 0 0 51925 80 0 0 25 0 1 0 543177929 107769856 25358 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26311 25358 603 41 0 26270 0
vsize: 105244
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 26167 0 0 0 52924 81 0 0 25 0 1 0 543177929 109629440 25803 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26765 25803 603 41 0 26724 0
vsize: 107060
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 26591 0 0 0 53923 83 0 0 25 0 1 0 543177929 111362048 26227 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27188 26227 603 41 0 27147 0
vsize: 108752
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 27032 0 0 0 54921 84 0 0 25 0 1 0 543177929 113102848 26668 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27613 26668 603 41 0 27572 0
vsize: 110452
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 27468 0 0 0 55920 86 0 0 25 0 1 0 543177929 114831360 27104 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28035 27104 603 41 0 27994 0
vsize: 112140
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 27874 0 0 0 56919 86 0 0 25 0 1 0 543177929 116555776 27510 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28456 27510 603 41 0 28415 0
vsize: 113824
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 28260 0 0 0 57919 87 0 0 25 0 1 0 543177929 118153216 27896 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28846 27896 603 41 0 28805 0
vsize: 115384
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 28644 0 0 0 58918 88 0 0 25 0 1 0 543177929 119738368 28280 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29233 28280 603 41 0 29192 0
vsize: 116932
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 28969 0 0 0 59917 89 0 0 25 0 1 0 543177929 121077760 28605 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29560 28605 603 41 0 29519 0
vsize: 118240
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 29468 0 0 0 60916 91 0 0 25 0 1 0 543177929 123113472 29104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30057 29104 603 41 0 30016 0
vsize: 120228
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 29982 0 0 0 61914 93 0 0 25 0 1 0 543177929 125128704 29618 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30549 29618 603 41 0 30508 0
vsize: 122196
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 30654 0 0 0 62914 94 0 0 25 0 1 0 543177929 127967232 30290 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31242 30290 603 41 0 31201 0
vsize: 124968
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 31248 0 0 0 63913 95 0 0 25 0 1 0 543177929 130387968 30884 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31833 30884 603 41 0 31792 0
vsize: 127332
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 31628 0 0 0 64912 96 0 0 25 0 1 0 543177929 131866624 31264 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32194 31264 603 41 0 32153 0
vsize: 128776
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 32202 0 0 0 65911 98 0 0 25 0 1 0 543177929 134262784 31838 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32779 31838 603 41 0 32738 0
vsize: 131116
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 32685 0 0 0 66910 99 0 0 25 0 1 0 543177929 136257536 32321 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33266 32321 603 41 0 33225 0
vsize: 133064
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 33022 0 0 0 67909 100 0 0 25 0 1 0 543177929 137596928 32658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33593 32658 603 41 0 33552 0
vsize: 134372
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 33357 0 0 0 68908 101 0 0 25 0 1 0 543177929 138924032 32993 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33917 32993 603 41 0 33876 0
vsize: 135668
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 33564 0 0 0 69907 102 0 0 25 0 1 0 543177929 140378112 33200 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34272 33200 603 41 0 34231 0
vsize: 137088
[startup+710.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 33801 0 0 0 70906 103 0 0 25 0 1 0 543177929 141320192 33437 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34502 33437 603 41 0 34461 0
vsize: 138008
[startup+720.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 34279 0 0 0 71905 104 0 0 25 0 1 0 543177929 143196160 33915 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34960 33915 603 41 0 34919 0
vsize: 139840
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 34937 0 0 0 72903 106 0 0 25 0 1 0 543177929 145870848 34573 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35613 34573 603 41 0 35572 0
vsize: 142452
[startup+740.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 35467 0 0 0 73901 108 0 0 25 0 1 0 543177929 148135936 35103 4294967295 134512640 134672761 3221224624 3221223808 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36166 35103 603 41 0 36125 0
vsize: 144664
[startup+750.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 35961 0 0 0 74900 109 0 0 25 0 1 0 543177929 150134784 35597 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36654 35597 603 41 0 36613 0
vsize: 146616
[startup+760.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 36393 0 0 0 75899 111 0 0 25 0 1 0 543177929 151891968 36029 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37083 36029 603 41 0 37042 0
vsize: 148332
[startup+770.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 36836 0 0 0 76897 112 0 0 25 0 1 0 543177929 153628672 36472 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37507 36472 603 41 0 37466 0
vsize: 150028
[startup+780.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 37338 0 0 0 77896 114 0 0 25 0 1 0 543177929 155766784 36974 4294967295 134512640 134672761 3221224624 3221223808 134558846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38029 36974 603 41 0 37988 0
vsize: 152116
[startup+790.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 37601 0 0 0 78895 115 0 0 25 0 1 0 543177929 156852224 37237 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38294 37237 603 41 0 38253 0
vsize: 153176
[startup+800.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 37988 0 0 0 79894 116 0 0 25 0 1 0 543177929 158445568 37624 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38683 37624 603 41 0 38642 0
vsize: 154732
[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38374 0 0 0 80893 118 0 0 25 0 1 0 543177929 159932416 38010 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39046 38010 603 41 0 39005 0
vsize: 156184
[startup+820.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38802 0 0 0 81892 119 0 0 25 0 1 0 543177929 161660928 38438 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39468 38438 603 41 0 39427 0
vsize: 157872
[startup+830.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 82891 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 83892 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+850.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 84892 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 85892 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+870.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 86892 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+880.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 87892 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+890.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 88894 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+900.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 89894 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+910.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 90894 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 91894 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+930.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 92894 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+940.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 93895 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223796 134559060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+950.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 94895 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+960.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 95895 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+970.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 96895 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+980.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 97895 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+990.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 98896 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 99896 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 100896 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 101896 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223824 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 102896 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 103897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 104897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 105896 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 106897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 107897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 108897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 109897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 110897 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 111898 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 112898 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 113898 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 114898 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 115898 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 116899 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 117899 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 118899 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24189
Raw data (stat): 24189 (minisat+) R 24188 23176 23175 0 -1 0 38954 0 0 0 119899 120 0 0 25 0 1 0 543177929 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 24189
Raw data (stat): 24189 (minisat+) Z 24188 23176 23175 0 -1 12 38956 0 0 0 119899 128 0 0 25 0 1 0 543177929 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.28
CPU user time (s): 1199
CPU system time (s): 1.2838
CPU usage (%): 100.011
Max. virtual memory (Kb): 158528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####