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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-l152lav.opb
MD5SUM9d4ce12b138a2bef65a1f401ec9d1f01
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers19
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.69
Number of variables1989
Total number of constraints2086
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2085
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint1989

Trace number 15164 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        806164 kB
Buffers:         22412 kB
Cached:         175988 kB
SwapCached:         24 kB
Active:          26688 kB
Inactive:       174352 kB
HighTotal:      131008 kB
HighFree:        54264 kB
LowTotal:       903652 kB
LowFree:        751900 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22028 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:24:03 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 18478 7 1200.25 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.85 0.98 0.94 2/54 26521
Raw data (stat): 26521 (runsolver) R 26520 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541692466 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.0003 s]
Raw data (loadavg): 0.87 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 4354 0 0 0 987 11 0 0 25 0 1 0 541692466 20140032 3990 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4917 3990 603 41 0 4876 0
vsize: 19668
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 4690 0 0 0 1986 12 0 0 25 0 1 0 541692466 21487616 4326 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5246 4326 603 41 0 5205 0
vsize: 20984
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 4836 0 0 0 2985 14 0 0 25 0 1 0 541692466 22028288 4472 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5378 4472 603 41 0 5337 0
vsize: 21512
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 4960 0 0 0 3984 14 0 0 25 0 1 0 541692466 22564864 4596 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5509 4596 603 41 0 5468 0
vsize: 22036
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 5219 0 0 0 4984 15 0 0 25 0 1 0 541692466 23638016 4855 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5771 4855 603 41 0 5730 0
vsize: 23084
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 5626 0 0 0 5982 17 0 0 25 0 1 0 541692466 25395200 5262 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5262 603 41 0 6159 0
vsize: 24800
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 5970 0 0 0 6981 19 0 0 25 0 1 0 541692466 26742784 5606 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6529 5606 603 41 0 6488 0
vsize: 26116
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 6275 0 0 0 7979 21 0 0 25 0 1 0 541692466 27955200 5911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6825 5911 603 41 0 6784 0
vsize: 27300
[startup+90.0041 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 6782 0 0 0 8978 22 0 0 25 0 1 0 541692466 30105600 6418 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7350 6418 603 41 0 7309 0
vsize: 29400
[startup+100.004 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 7437 0 0 0 9976 24 0 0 25 0 1 0 541692466 32677888 7073 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7978 7073 603 41 0 7937 0
vsize: 31912
[startup+110.005 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 7698 0 0 0 10975 25 0 0 25 0 1 0 541692466 33878016 7334 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7334 603 41 0 8230 0
vsize: 33084
[startup+120.005 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26521
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 8192 0 0 0 11973 27 0 0 25 0 1 0 541692466 35876864 7828 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8759 7828 603 41 0 8718 0
vsize: 35036
[startup+130.005 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 8633 0 0 0 12972 28 0 0 25 0 1 0 541692466 37756928 8269 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9218 8269 603 41 0 9177 0
vsize: 36872
[startup+140.006 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 9187 0 0 0 13971 30 0 0 25 0 1 0 541692466 40034304 8823 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9774 8823 603 41 0 9733 0
vsize: 39096
[startup+150.006 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 9778 0 0 0 14968 32 0 0 25 0 1 0 541692466 42450944 9414 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10364 9414 603 41 0 10323 0
vsize: 41456
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 10326 0 0 0 15967 34 0 0 25 0 1 0 541692466 44605440 9962 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 9962 603 41 0 10849 0
vsize: 43560
[startup+170.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 10843 0 0 0 16965 36 0 0 25 0 1 0 541692466 46747648 10479 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11413 10479 603 41 0 11372 0
vsize: 45652
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 11333 0 0 0 17963 38 0 0 25 0 1 0 541692466 48775168 10969 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11908 10969 603 41 0 11867 0
vsize: 47632
[startup+190.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 11764 0 0 0 18962 39 0 0 25 0 1 0 541692466 50524160 11400 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12335 11400 603 41 0 12294 0
vsize: 49340
[startup+200.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 12190 0 0 0 19961 40 0 0 25 0 1 0 541692466 52244480 11826 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12755 11826 603 41 0 12714 0
vsize: 51020
[startup+210.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 12538 0 0 0 20960 41 0 0 25 0 1 0 541692466 53723136 12174 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13116 12174 603 41 0 13075 0
vsize: 52464
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 12863 0 0 0 21959 43 0 0 25 0 1 0 541692466 55042048 12499 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13438 12499 603 41 0 13397 0
vsize: 53752
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 13169 0 0 0 22959 43 0 0 25 0 1 0 541692466 56246272 12805 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13732 12805 603 41 0 13691 0
vsize: 54928
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 13533 0 0 0 23957 45 0 0 25 0 1 0 541692466 57716736 13169 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14091 13169 603 41 0 14050 0
vsize: 56364
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 13941 0 0 0 24955 47 0 0 25 0 1 0 541692466 59453440 13577 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14515 13577 603 41 0 14474 0
vsize: 58060
[startup+260.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 14424 0 0 0 25954 49 0 0 25 0 1 0 541692466 61341696 14060 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14976 14060 603 41 0 14935 0
vsize: 59904
[startup+270.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 14854 0 0 0 26952 50 0 0 25 0 1 0 541692466 63098880 14490 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15405 14490 603 41 0 15364 0
vsize: 61620
[startup+280.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 15280 0 0 0 27951 51 0 0 25 0 1 0 541692466 64856064 14916 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15834 14916 603 41 0 15793 0
vsize: 63336
[startup+290.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 15771 0 0 0 28950 53 0 0 25 0 1 0 541692466 66867200 15407 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 15407 603 41 0 16284 0
vsize: 65300
[startup+300.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 16213 0 0 0 29949 54 0 0 25 0 1 0 541692466 69017600 15849 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16850 15849 603 41 0 16809 0
vsize: 67400
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 16603 0 0 0 30947 56 0 0 25 0 1 0 541692466 70496256 16239 4294967295 134512640 134672761 3221224624 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17211 16239 603 41 0 17170 0
vsize: 68844
[startup+320.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 16926 0 0 0 31947 57 0 0 25 0 1 0 541692466 71831552 16562 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17537 16562 603 41 0 17496 0
vsize: 70148
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 17434 0 0 0 32945 58 0 0 25 0 1 0 541692466 73965568 17070 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18058 17070 603 41 0 18017 0
vsize: 72232
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 17941 0 0 0 33943 60 0 0 25 0 1 0 541692466 75980800 17577 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18550 17577 603 41 0 18509 0
vsize: 74200
[startup+350.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 18432 0 0 0 34941 62 0 0 25 0 1 0 541692466 78000128 18068 4294967295 134512640 134672761 3221224624 3221223728 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19043 18068 603 41 0 19002 0
vsize: 76172
[startup+360.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 18875 0 0 0 35940 64 0 0 25 0 1 0 541692466 79867904 18511 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19499 18511 603 41 0 19458 0
vsize: 77996
[startup+370.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 19418 0 0 0 36938 66 0 0 25 0 1 0 541692466 82018304 19054 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20024 19054 603 41 0 19983 0
vsize: 80096
[startup+380.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 19814 0 0 0 37937 67 0 0 25 0 1 0 541692466 83615744 19450 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20414 19450 603 41 0 20373 0
vsize: 81656
[startup+390.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 20271 0 0 0 38936 68 0 0 25 0 1 0 541692466 85504000 19907 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20875 19907 603 41 0 20834 0
vsize: 83500
[startup+400.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 20713 0 0 0 39935 69 0 0 25 0 1 0 541692466 87367680 20349 4294967295 134512640 134672761 3221224624 3221223808 134558880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21330 20349 603 41 0 21289 0
vsize: 85320
[startup+410.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 21087 0 0 0 40934 70 0 0 25 0 1 0 541692466 88854528 20723 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21693 20723 603 41 0 21652 0
vsize: 86772
[startup+420.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 21476 0 0 0 41933 72 0 0 25 0 1 0 541692466 90464256 21112 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22086 21112 603 41 0 22045 0
vsize: 88344
[startup+430.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 21942 0 0 0 42932 73 0 0 25 0 1 0 541692466 92336128 21578 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22543 21578 603 41 0 22502 0
vsize: 90172
[startup+440.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 22468 0 0 0 43930 75 0 0 25 0 1 0 541692466 94474240 22104 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23065 22104 603 41 0 23024 0
vsize: 92260
[startup+450.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 23009 0 0 0 44928 77 0 0 25 0 1 0 541692466 96747520 22645 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23620 22645 603 41 0 23579 0
vsize: 94480
[startup+460.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 23531 0 0 0 45927 79 0 0 25 0 1 0 541692466 98856960 23167 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24135 23167 603 41 0 24094 0
vsize: 96540
[startup+470.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 23941 0 0 0 46926 79 0 0 25 0 1 0 541692466 100458496 23577 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24526 23577 603 41 0 24485 0
vsize: 98104
[startup+480.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 24342 0 0 0 47925 81 0 0 25 0 1 0 541692466 102162432 23978 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24942 23978 603 41 0 24901 0
vsize: 99768
[startup+490.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 24585 0 0 0 48924 82 0 0 25 0 1 0 541692466 103092224 24221 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25169 24221 603 41 0 25128 0
vsize: 100676
[startup+500.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 25016 0 0 0 49923 83 0 0 25 0 1 0 541692466 104820736 24652 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25591 24652 603 41 0 25550 0
vsize: 102364
[startup+510.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 25486 0 0 0 50922 84 0 0 25 0 1 0 541692466 106831872 25122 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26082 25122 603 41 0 26041 0
vsize: 104328
[startup+520.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 25995 0 0 0 51920 86 0 0 25 0 1 0 541692466 108834816 25631 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26571 25631 603 41 0 26530 0
vsize: 106284
[startup+530.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 26430 0 0 0 52919 87 0 0 25 0 1 0 541692466 110690304 26066 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27024 26066 603 41 0 26983 0
vsize: 108096
[startup+540.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 26860 0 0 0 53917 89 0 0 25 0 1 0 541692466 112431104 26496 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27449 26496 603 41 0 27408 0
vsize: 109796
[startup+550.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 27331 0 0 0 54915 91 0 0 25 0 1 0 541692466 114294784 26967 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27904 26967 603 41 0 27863 0
vsize: 111616
[startup+560.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 27745 0 0 0 55914 92 0 0 25 0 1 0 541692466 116027392 27381 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28327 27381 603 41 0 28286 0
vsize: 113308
[startup+570.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 28150 0 0 0 56913 94 0 0 25 0 1 0 541692466 117616640 27786 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28715 27786 603 41 0 28674 0
vsize: 114860
[startup+580.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 28547 0 0 0 57912 95 0 0 25 0 1 0 541692466 119345152 28183 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29137 28183 603 41 0 29096 0
vsize: 116548
[startup+590.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 28881 0 0 0 58911 96 0 0 25 0 1 0 541692466 120672256 28517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29461 28517 603 41 0 29420 0
vsize: 117844
[startup+600.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 29361 0 0 0 59910 97 0 0 25 0 1 0 541692466 122576896 28997 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29926 28997 603 41 0 29885 0
vsize: 119704
[startup+610.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 29893 0 0 0 60908 99 0 0 25 0 1 0 541692466 124858368 29529 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30483 29529 603 41 0 30442 0
vsize: 121932
[startup+620.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 30537 0 0 0 61907 101 0 0 25 0 1 0 541692466 127426560 30173 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31110 30173 603 41 0 31069 0
vsize: 124440
[startup+630.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 31176 0 0 0 62905 102 0 0 25 0 1 0 541692466 129990656 30812 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31736 30812 603 41 0 31695 0
vsize: 126944
[startup+640.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 31570 0 0 0 63904 104 0 0 25 0 1 0 541692466 131596288 31206 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32128 31206 603 41 0 32087 0
vsize: 128512
[startup+650.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 32178 0 0 0 64903 105 0 0 25 0 1 0 541692466 134127616 31814 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32746 31814 603 41 0 32705 0
vsize: 130984
[startup+660.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 32671 0 0 0 65901 107 0 0 25 0 1 0 541692466 136122368 32307 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33233 32307 603 41 0 33192 0
vsize: 132932
[startup+670.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 33021 0 0 0 66901 108 0 0 25 0 1 0 541692466 137596928 32657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33593 32657 603 41 0 33552 0
vsize: 134372
[startup+680.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 33368 0 0 0 67899 109 0 0 25 0 1 0 541692466 139051008 33004 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33948 33004 603 41 0 33907 0
vsize: 135792
[startup+690.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 33575 0 0 0 68898 110 0 0 25 0 1 0 541692466 140378112 33211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34272 33211 603 41 0 34231 0
vsize: 137088
[startup+700.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 33836 0 0 0 69898 111 0 0 25 0 1 0 541692466 141447168 33472 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34533 33472 603 41 0 34492 0
vsize: 138132
[startup+710.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 34347 0 0 0 70896 113 0 0 25 0 1 0 541692466 143466496 33983 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35026 33983 603 41 0 34985 0
vsize: 140104
[startup+720.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 34984 0 0 0 71895 115 0 0 25 0 1 0 541692466 146137088 34620 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35678 34620 603 41 0 35637 0
vsize: 142712
[startup+730.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 35535 0 0 0 72893 116 0 0 25 0 1 0 541692466 148393984 35171 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36229 35171 603 41 0 36188 0
vsize: 144916
[startup+740.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 36035 0 0 0 73892 118 0 0 25 0 1 0 541692466 150405120 35671 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36720 35671 603 41 0 36679 0
vsize: 146880
[startup+750.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 36471 0 0 0 74890 120 0 0 25 0 1 0 541692466 152162304 36107 4294967295 134512640 134672761 3221224624 3221223624 1075349791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37149 36107 603 41 0 37108 0
vsize: 148596
[startup+760.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 36950 0 0 0 75889 121 0 0 25 0 1 0 541692466 154165248 36586 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37638 36586 603 41 0 37597 0
vsize: 150552
[startup+770.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 37380 0 0 0 76888 122 0 0 25 0 1 0 541692466 155901952 37016 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38062 37016 603 41 0 38021 0
vsize: 152248
[startup+780.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 37704 0 0 0 77887 123 0 0 25 0 1 0 541692466 157253632 37340 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38392 37340 603 41 0 38351 0
vsize: 153568
[startup+790.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38139 0 0 0 78886 125 0 0 25 0 1 0 541692466 158986240 37775 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38815 37775 603 41 0 38774 0
vsize: 155260
[startup+800.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38533 0 0 0 79885 126 0 0 25 0 1 0 541692466 160600064 38169 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39209 38169 603 41 0 39168 0
vsize: 156836
[startup+810.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38848 0 0 0 80884 127 0 0 25 0 1 0 541692466 161935360 38484 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39535 38484 603 41 0 39494 0
vsize: 158140
[startup+820.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 81884 127 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+830.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 82884 127 0 0 25 0 1 0 541692466 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+840.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 83884 127 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+850.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 84883 128 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+860.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 85883 128 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+870.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 86883 128 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+880.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 87883 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+890.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 88883 129 0 0 25 0 1 0 541692466 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+900.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 89883 129 0 0 25 0 1 0 541692466 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+910.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 90883 129 0 0 25 0 1 0 541692466 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+920.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 91884 129 0 0 25 0 1 0 541692466 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+930.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 92884 129 0 0 25 0 1 0 541692466 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+940.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 93884 129 0 0 25 0 1 0 541692466 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+950.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 94884 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559955 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.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 95884 129 0 0 25 0 1 0 541692466 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+970.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 96884 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560031 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 97884 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560937 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.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 98884 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560054 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 99884 129 0 0 25 0 1 0 541692466 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+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 100884 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560942 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 101885 129 0 0 25 0 1 0 541692466 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+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 102885 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223808 134559415 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 103884 129 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560054 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 104884 130 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 105884 130 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560940 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 106884 130 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560054 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 107885 130 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560492 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 108885 130 0 0 25 0 1 0 541692466 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+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 109885 130 0 0 25 0 1 0 541692466 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 110885 130 0 0 25 0 1 0 541692466 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 111885 130 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223824 134557913 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 112885 130 0 0 25 0 1 0 541692466 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+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 113885 130 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560424 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 114885 130 0 0 25 0 1 0 541692466 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 115885 131 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223824 134557849 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 116885 131 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559925 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 117885 131 0 0 25 0 1 0 541692466 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+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 118885 131 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223772 134559754 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26523
Raw data (stat): 26521 (minisat+) R 26520 26298 26297 0 -1 0 38954 0 0 0 119885 131 0 0 25 0 1 0 541692466 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559890 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.11 s]
Raw data (loadavg): 0.99 0.98 0.94 1/54 26523
Raw data (stat): 26521 (minisat+) Z 26520 26298 26297 0 -1 12 38956 0 0 0 119885 138 0 0 25 0 1 0 541692466 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.11
CPU time (s): 1200.25
CPU user time (s): 1198.86
CPU system time (s): 1.38979
CPU usage (%): 100.012
Max. virtual memory (Kb): 158528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####