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/miplib/normalized-mps-v2-13-7-l152lav.opb
MD5SUM00855a9538cee8df79108d56ee6867b4
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 benchmark1176.34
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 15702 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 05:32:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16892 boxname=wulflinc5 idbench=1300 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-l152lav.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-l152lav.opb
IDLAUNCH: 16892
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        470484 kB
Buffers:         34684 kB
Cached:         506392 kB
SwapCached:          0 kB
Active:         108648 kB
Inactive:       435236 kB
HighTotal:      131008 kB
HighFree:         4760 kB
LowTotal:       903652 kB
LowFree:        465724 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14640 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:52:05 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 16892 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.84 0.94 0.90 2/54 17459
Raw data (stat): 17459 (runsolver) R 17458 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484361297 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 4358 0 0 0 988 10 0 0 25 0 1 0 484361297 20140032 3994 4294967295 134512640 134672761 3221224624 3221223760 134565066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4917 3994 603 41 0 4876 0
vsize: 19668
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 4693 0 0 0 1987 10 0 0 25 0 1 0 484361297 21487616 4329 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5246 4329 603 41 0 5205 0
vsize: 20984
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 4837 0 0 0 2987 11 0 0 25 0 1 0 484361297 22163456 4473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5411 4473 603 41 0 5370 0
vsize: 21644
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 4963 0 0 0 3986 11 0 0 25 0 1 0 484361297 22564864 4599 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5509 4599 603 41 0 5468 0
vsize: 22036
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 5220 0 0 0 4986 12 0 0 25 0 1 0 484361297 23638016 4856 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5771 4856 603 41 0 5730 0
vsize: 23084
[startup+60.0018 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 5662 0 0 0 5985 13 0 0 25 0 1 0 484361297 25530368 5298 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6233 5298 603 41 0 6192 0
vsize: 24932
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 5985 0 0 0 6984 14 0 0 25 0 1 0 484361297 26742784 5621 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6529 5621 603 41 0 6488 0
vsize: 26116
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 6290 0 0 0 7984 15 0 0 25 0 1 0 484361297 28086272 5926 4294967295 134512640 134672761 3221224624 3221223808 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6857 5926 603 41 0 6816 0
vsize: 27428
[startup+90.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 6839 0 0 0 8982 17 0 0 25 0 1 0 484361297 30240768 6475 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6475 603 41 0 7342 0
vsize: 29532
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 7455 0 0 0 9980 18 0 0 25 0 1 0 484361297 32808960 7091 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8010 7091 603 41 0 7969 0
vsize: 32040
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 7747 0 0 0 10980 19 0 0 25 0 1 0 484361297 34144256 7383 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8336 7383 603 41 0 8295 0
vsize: 33344
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 8230 0 0 0 11979 21 0 0 25 0 1 0 484361297 36012032 7866 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8792 7866 603 41 0 8751 0
vsize: 35168
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 8707 0 0 0 12977 22 0 0 25 0 1 0 484361297 38019072 8343 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9282 8343 603 41 0 9241 0
vsize: 37128
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 9273 0 0 0 13976 24 0 0 25 0 1 0 484361297 40304640 8909 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9840 8909 603 41 0 9799 0
vsize: 39360
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 9863 0 0 0 14974 25 0 0 25 0 1 0 484361297 42721280 9499 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9499 603 41 0 10389 0
vsize: 41720
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 10407 0 0 0 15973 27 0 0 25 0 1 0 484361297 45006848 10043 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10988 10043 603 41 0 10947 0
vsize: 43952
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 10913 0 0 0 16972 29 0 0 25 0 1 0 484361297 47017984 10549 4294967295 134512640 134672761 3221224624 3221223760 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11479 10549 603 41 0 11438 0
vsize: 45916
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 11408 0 0 0 17970 30 0 0 25 0 1 0 484361297 49045504 11044 4294967295 134512640 134672761 3221224624 3221223728 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11974 11044 603 41 0 11933 0
vsize: 47896
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 11831 0 0 0 18969 31 0 0 25 0 1 0 484361297 50782208 11467 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12398 11467 603 41 0 12357 0
vsize: 49592
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 12260 0 0 0 19968 33 0 0 25 0 1 0 484361297 52510720 11896 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11896 603 41 0 12779 0
vsize: 51280
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 12593 0 0 0 20968 33 0 0 25 0 1 0 484361297 53858304 12229 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13149 12229 603 41 0 13108 0
vsize: 52596
[startup+220.005 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 12913 0 0 0 21966 35 0 0 25 0 1 0 484361297 55177216 12549 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13471 12549 603 41 0 13430 0
vsize: 53884
[startup+230.006 s]
Raw data (loadavg): 1.13 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 13231 0 0 0 22966 35 0 0 25 0 1 0 484361297 56504320 12867 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13795 12867 603 41 0 13754 0
vsize: 55180
[startup+240.005 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 13604 0 0 0 23965 36 0 0 25 0 1 0 484361297 57987072 13240 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14157 13240 603 41 0 14116 0
vsize: 56628
[startup+250.005 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 14045 0 0 0 24964 37 0 0 25 0 1 0 484361297 59858944 13681 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14614 13681 603 41 0 14573 0
vsize: 58456
[startup+260.006 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 14507 0 0 0 25963 38 0 0 25 0 1 0 484361297 61747200 14143 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15075 14143 603 41 0 15034 0
vsize: 60300
[startup+270.006 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 14978 0 0 0 26962 39 0 0 25 0 1 0 484361297 63639552 14614 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15537 14614 603 41 0 15496 0
vsize: 62148
[startup+280.007 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 15379 0 0 0 27961 40 0 0 25 0 1 0 484361297 65261568 15015 4294967295 134512640 134672761 3221224624 3221223728 134559946 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15933 15015 603 41 0 15892 0
vsize: 63732
[startup+290.006 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 15858 0 0 0 28960 41 0 0 25 0 1 0 484361297 67268608 15494 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16423 15494 603 41 0 16382 0
vsize: 65692
[startup+300.007 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 16326 0 0 0 29959 43 0 0 25 0 1 0 484361297 69423104 15962 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16949 15962 603 41 0 16908 0
vsize: 67796
[startup+310.007 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 16666 0 0 0 30958 44 0 0 25 0 1 0 484361297 70762496 16302 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17276 16302 603 41 0 17235 0
vsize: 69104
[startup+320.007 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 17040 0 0 0 31958 44 0 0 25 0 1 0 484361297 72364032 16676 4294967295 134512640 134672761 3221224624 3221223728 134559951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17667 16676 603 41 0 17626 0
vsize: 70668
[startup+330.007 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 17571 0 0 0 32956 46 0 0 25 0 1 0 484361297 74502144 17207 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18189 17207 603 41 0 18148 0
vsize: 72756
[startup+340.007 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 18037 0 0 0 33956 47 0 0 25 0 1 0 484361297 76386304 17673 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18649 17673 603 41 0 18608 0
vsize: 74596
[startup+350.008 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 18568 0 0 0 34955 48 0 0 25 0 1 0 484361297 78532608 18204 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19173 18204 603 41 0 19132 0
vsize: 76692
[startup+360.007 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 19012 0 0 0 35953 50 0 0 25 0 1 0 484361297 80408576 18648 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19631 18648 603 41 0 19590 0
vsize: 78524
[startup+370.008 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 19475 0 0 0 36952 51 0 0 25 0 1 0 484361297 82288640 19111 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20090 19111 603 41 0 20049 0
vsize: 80360
[startup+380.008 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 19949 0 0 0 37951 52 0 0 25 0 1 0 484361297 84156416 19585 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20546 19585 603 41 0 20505 0
vsize: 82184
[startup+390.007 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 20409 0 0 0 38950 53 0 0 25 0 1 0 484361297 86036480 20045 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21005 20045 603 41 0 20964 0
vsize: 84020
[startup+400.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 20824 0 0 0 39948 55 0 0 25 0 1 0 484361297 87773184 20460 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21429 20460 603 41 0 21388 0
vsize: 85716
[startup+410.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 21180 0 0 0 40946 56 0 0 25 0 1 0 484361297 89260032 20816 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21792 20816 603 41 0 21751 0
vsize: 87168
[startup+420.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 21603 0 0 0 41945 57 0 0 25 0 1 0 484361297 90869760 21239 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22185 21239 603 41 0 22144 0
vsize: 88740
[startup+430.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 22091 0 0 0 42944 59 0 0 25 0 1 0 484361297 92872704 21727 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22674 21727 603 41 0 22633 0
vsize: 90696
[startup+440.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 22624 0 0 0 43943 60 0 0 25 0 1 0 484361297 95150080 22260 4294967295 134512640 134672761 3221224624 3221223808 134558831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23230 22260 603 41 0 23189 0
vsize: 92920
[startup+450.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 23170 0 0 0 44943 61 0 0 25 0 1 0 484361297 97280000 22806 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23750 22806 603 41 0 23709 0
vsize: 95000
[startup+460.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 23684 0 0 0 45941 62 0 0 25 0 1 0 484361297 99385344 23320 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24264 23320 603 41 0 24223 0
vsize: 97056
[startup+470.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 24043 0 0 0 46941 63 0 0 25 0 1 0 484361297 100851712 23679 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24622 23679 603 41 0 24581 0
vsize: 98488
[startup+480.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 24432 0 0 0 47940 64 0 0 25 0 1 0 484361297 102559744 24068 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25039 24068 603 41 0 24998 0
vsize: 100156
[startup+490.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 24730 0 0 0 48939 65 0 0 25 0 1 0 484361297 103768064 24366 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25334 24366 603 41 0 25293 0
vsize: 101336
[startup+500.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 25170 0 0 0 49938 66 0 0 25 0 1 0 484361297 105492480 24806 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25755 24806 603 41 0 25714 0
vsize: 103020
[startup+510.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 25665 0 0 0 50938 67 0 0 25 0 1 0 484361297 107499520 25301 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26245 25301 603 41 0 26204 0
vsize: 104980
[startup+520.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 26140 0 0 0 51936 69 0 0 25 0 1 0 484361297 109494272 25776 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26732 25776 603 41 0 26691 0
vsize: 106928
[startup+530.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 26572 0 0 0 52936 69 0 0 25 0 1 0 484361297 111226880 26208 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27155 26208 603 41 0 27114 0
vsize: 108620
[startup+540.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 27026 0 0 0 53935 70 0 0 25 0 1 0 484361297 113102848 26662 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27613 26662 603 41 0 27572 0
vsize: 110452
[startup+550.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 27476 0 0 0 54934 71 0 0 25 0 1 0 484361297 114962432 27112 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28067 27112 603 41 0 28026 0
vsize: 112268
[startup+560.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 27891 0 0 0 55933 72 0 0 25 0 1 0 484361297 116555776 27527 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28456 27527 603 41 0 28415 0
vsize: 113824
[startup+570.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 28290 0 0 0 56932 74 0 0 25 0 1 0 484361297 118288384 27926 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28879 27926 603 41 0 28838 0
vsize: 115516
[startup+580.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 28675 0 0 0 57931 75 0 0 25 0 1 0 484361297 119873536 28311 4294967295 134512640 134672761 3221224624 3221223840 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29266 28311 603 41 0 29225 0
vsize: 117064
[startup+590.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 29041 0 0 0 58930 76 0 0 25 0 1 0 484361297 121348096 28677 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29626 28677 603 41 0 29585 0
vsize: 118504
[startup+600.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 29575 0 0 0 59929 77 0 0 25 0 1 0 484361297 123510784 29211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30154 29211 603 41 0 30113 0
vsize: 120616
[startup+610.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 30078 0 0 0 60928 79 0 0 25 0 1 0 484361297 125530112 29714 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30647 29714 603 41 0 30606 0
vsize: 122588
[startup+620.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 30820 0 0 0 61927 80 0 0 25 0 1 0 484361297 128638976 30456 4294967295 134512640 134672761 3221224624 3221223808 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31406 30456 603 41 0 31365 0
vsize: 125624
[startup+630.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 31363 0 0 0 62926 81 0 0 25 0 1 0 484361297 130789376 30999 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31931 30999 603 41 0 31890 0
vsize: 127724
[startup+640.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 31821 0 0 0 63924 82 0 0 25 0 1 0 484361297 132661248 31457 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32388 31457 603 41 0 32347 0
vsize: 129552
[startup+650.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 32357 0 0 0 64923 84 0 0 25 0 1 0 484361297 134918144 31993 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32939 31993 603 41 0 32898 0
vsize: 131756
[startup+660.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 32905 0 0 0 65922 85 0 0 25 0 1 0 484361297 137064448 32541 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33463 32541 603 41 0 33422 0
vsize: 133852
[startup+670.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 33180 0 0 0 66921 86 0 0 25 0 1 0 484361297 138256384 32816 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33754 32816 603 41 0 33713 0
vsize: 135016
[startup+680.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 33498 0 0 0 67920 87 0 0 25 0 1 0 484361297 139587584 33134 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34079 33134 603 41 0 34038 0
vsize: 136316
[startup+690.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 33663 0 0 0 68919 88 0 0 25 0 1 0 484361297 140779520 33299 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34370 33299 603 41 0 34329 0
vsize: 137480
[startup+700.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 34045 0 0 0 69918 89 0 0 25 0 1 0 484361297 142249984 33681 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34729 33681 603 41 0 34688 0
vsize: 138916
[startup+710.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 34640 0 0 0 70917 90 0 0 25 0 1 0 484361297 144666624 34276 4294967295 134512640 134672761 3221224624 3221223728 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35319 34276 603 41 0 35278 0
vsize: 141276
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 35229 0 0 0 71915 92 0 0 25 0 1 0 484361297 147066880 34865 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35905 34865 603 41 0 35864 0
vsize: 143620
[startup+730.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 35764 0 0 0 72915 93 0 0 25 0 1 0 484361297 149327872 35400 4294967295 134512640 134672761 3221224624 3221223808 134559392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36457 35400 603 41 0 36416 0
vsize: 145828
[startup+740.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 36224 0 0 0 73913 95 0 0 25 0 1 0 484361297 151220224 35860 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36919 35860 603 41 0 36878 0
vsize: 147676
[startup+750.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 36702 0 0 0 74912 96 0 0 25 0 1 0 484361297 153092096 36338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37376 36338 603 41 0 37335 0
vsize: 149504
[startup+760.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 37208 0 0 0 75911 97 0 0 25 0 1 0 484361297 155226112 36844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37897 36844 603 41 0 37856 0
vsize: 151588
[startup+770.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 37532 0 0 0 76911 98 0 0 25 0 1 0 484361297 156581888 37168 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38228 37168 603 41 0 38187 0
vsize: 152912
[startup+780.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 37911 0 0 0 77910 99 0 0 25 0 1 0 484361297 158048256 37547 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38586 37547 603 41 0 38545 0
vsize: 154344
[startup+790.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38324 0 0 0 78909 100 0 0 25 0 1 0 484361297 159797248 37960 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39013 37960 603 41 0 38972 0
vsize: 156052
[startup+800.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38758 0 0 0 79908 101 0 0 25 0 1 0 484361297 161525760 38394 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39435 38394 603 41 0 39394 0
vsize: 157740
[startup+810.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38945 0 0 0 80908 101 0 0 25 0 1 0 484361297 162332672 38581 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38581 603 41 0 39591 0
vsize: 158528
[startup+820.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 81908 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560293 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.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 82908 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223760 134560667 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 83908 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561198 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 84908 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223748 134566057 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 85909 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 86909 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223760 134560709 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 87909 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561193 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 88909 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 89909 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223824 134557895 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.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 90909 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+920.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 91910 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+930.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 92910 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+940.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 93910 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+950.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 94910 101 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+960.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 95910 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+970.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 96911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+980.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 97911 102 0 0 25 0 1 0 484361297 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+990.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 98911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 99911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 100911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 101912 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 102911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 103911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 104911 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560218 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.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 105912 102 0 0 25 0 1 0 484361297 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+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 106912 102 0 0 25 0 1 0 484361297 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+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 107912 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 108912 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 109913 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 110913 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 111913 102 0 0 25 0 1 0 484361297 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+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 112913 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 113913 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 114914 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 115914 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 116914 102 0 0 25 0 1 0 484361297 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+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 117914 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 118914 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17459
Raw data (stat): 17459 (minisat+) R 17458 24215 24214 0 -1 0 38954 0 0 0 119915 102 0 0 25 0 1 0 484361297 162332672 38590 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39632 38590 603 41 0 39591 0
vsize: 158528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 17459
Raw data (stat): 17459 (minisat+) Z 17458 24215 24214 0 -1 12 38956 0 0 0 119915 109 0 0 25 0 1 0 484361297 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.25
CPU user time (s): 1199.15
CPU system time (s): 1.09383
CPU usage (%): 100.012
Max. virtual memory (Kb): 158528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####