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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-cracpb1.opb
MD5SUM098fe473d82d5f7d4121673eb775be76
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 22199
Optimality of the best value was proved NO
Number of terms in the objective function 572
Biggest coefficient in the objective function 5000
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 547769
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 5000
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 547769
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark30.1944
Number of variables572
Total number of constraints716
Number of constraints which are clauses3
Number of constraints which are cardinality constraints (but not clauses)644
Number of constraints which are nor clauses,nor cardinality constraints69
Minimum length of a constraint1
Maximum length of a constraint518

Trace number 17057 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 09:35:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11765 boxname=wulflinc8 idbench=905 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  098fe473d82d5f7d4121673eb775be76  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-cracpb1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-cracpb1.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-cracpb1.opb
IDLAUNCH: 11765
/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:        820116 kB
Buffers:         24888 kB
Cached:         167144 kB
SwapCached:          0 kB
Active:          61488 kB
Inactive:       133396 kB
HighTotal:      131008 kB
HighFree:         9240 kB
LowTotal:       903652 kB
LowFree:        810876 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13952 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:55:42 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 11765 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 215 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################
c   -- Clauses(.)/Splits(s): ...
c ---[ 214]---> Adder-cost: 1416   maxlim: 2733   bits: 12/12
c ---[ 213]---> Sorter-cost:  634     Base:
c ---[ 212]---> Sorter-cost:  238     Base:
c ---[ 211]---> Sorter-cost:  238     Base:
c ---[ 210]---> Sorter-cost:  206     Base:
c ---[ 209]---> Sorter-cost:  356     Base:
c ---[ 208]---> Sorter-cost:  356     Base:
c ---[ 207]---> Sorter-cost:  264     Base:
c ---[ 206]---> Sorter-cost:  126     Base:
c ---[ 205]---> Sorter-cost:  356     Base:
c ---[ 204]---> Sorter-cost:  106     Base:
c ---[ 203]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:   34
c ---[ 201]---> Sorter-cost:  170     Base:
c ---[ 200]---> BDD-cost:   29
c ---[ 199]---> Sorter-cost:  180     Base:
c ---[ 198]---> BDD-cost:   31
c ---[ 197]---> BDD-cost:   21
c ---[ 195]---> Sorter-cost:  561     Base:
c ---[ 193]---> BDD-cost:   41
c ---[ 191]---> Sorter-cost:  255     Base:
c ---[ 189]---> Sorter-cost:  207     Base:
c ---[ 187]---> Sorter-cost:  491     Base:
c ---[ 185]---> Sorter-cost:  239     Base:
c ---[ 183]---> Sorter-cost:  281     Base:
c ---[ 181]---> Sorter-cost:  181     Base:
c ---[ 179]---> Sorter-cost:  291     Base:
c ---[ 177]---> Sorter-cost:  127     Base:
c ---[ 175]---> BDD-cost:   33
c ---[ 173]---> Sorter-cost:  207     Base:
c ---[ 171]---> Sorter-cost:  117     Base:
c ---[ 169]---> Sorter-cost:   77     Base:
c ---[ 167]---> Sorter-cost:  171     Base:
c ---[ 165]---> Sorter-cost:  127     Base:
c ---[ 163]---> BDD-cost:   29
c ---[ 161]---> BDD-cost:   25
c ---[ 159]---> Adder-cost: 155   maxlim: 27   bits: 6/5
c ---[ 157]---> Sorter-cost:  631     Base:
c ---[ 155]---> Sorter-cost:  689     Base:
c ---[ 153]---> Sorter-cost:  609     Base:
c ---[ 151]---> Sorter-cost:  971     Base:
c ---[ 149]---> Sorter-cost:  991     Base:
c ---[ 147]---> Sorter-cost:  755     Base:
c ---[ 145]---> Sorter-cost:  371     Base:
c ---[ 143]---> Sorter-cost:  927     Base:
c ---[ 141]---> Sorter-cost:  355     Base:
c ---[ 139]---> Sorter-cost:  313     Base:
c ---[ 137]---> Sorter-cost:  279     Base:
c ---[ 135]---> Sorter-cost:  501     Base:
c ---[ 133]---> Sorter-cost:  225     Base:
c ---[ 131]---> Sorter-cost:  517     Base:
c ---[ 129]---> Sorter-cost:  197     Base:
c ---[ 127]---> BDD-cost:   66
c ---[ 126]---> Adder-cost: 732   maxlim: 1601   bits: 12/11
c ---[ 125]---> Adder-cost: 1184   maxlim: 406   bits: 10/9
c ---[ 124]---> Adder-cost: 255   maxlim: 863   bits: 11/10
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   35
c ---[ 121]---> Sorter-cost:  172     Base:
c ---[ 120]---> BDD-cost:   31
c ---[ 118]---> BDD-cost:   51
c ---[ 115]---> BDD-cost:   80
c ---[ 114]---> Sorter-cost:  238     Base:
c ---[ 113]---> Sorter-cost:  478     Base:
c ---[ 112]---> Sorter-cost:  254     Base:
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> Sorter-cost:  474     Base:
c ---[ 109]---> BDD-cost:   29
c ---[ 108]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:   43
c ---[  98]---> BDD-cost:   92
c ---[  96]---> BDD-cost:  183
c ---[  94]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   29
c ---[  90]---> BDD-cost:   29
c ---[  88]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   31
c ---[  80]---> BDD-cost:   23
c ---[  78]---> BDD-cost:    7
c ---[  76]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   38
c ---[  70]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   35
c ---[  66]---> BDD-cost:   37
c ---[  64]---> BDD-cost:    7
c ---[  62]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   43
c ---[  56]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   29
c ---[  52]---> BDD-cost:    7
c ---[  50]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   24
c ---[  46]---> BDD-cost:    5
c ---[  44]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    4
c ---[  26]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   48
c ---[  18]---> BDD-cost:   51
c ---[  16]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    6
c ---[  12]---> BDD-cost:   51
c ---[  10]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   22
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   67939   195555 |   22646       0        0     nan |  0.000 % |
c |       100 |   67862   195385 |   24910      96     1024    10.7 |  2.636 % |
c |       250 |   67626   194856 |   27401     168     1418     8.4 |  3.012 % |
c |       475 |   67213   193932 |   30141     362     3093     8.5 |  3.698 % |
c |       812 |   67166   193828 |   33156     695    14012    20.2 |  3.772 % |
c |      1318 |   66656   192653 |   36471    1147    23771    20.7 |  4.563 % |
c |      2077 |   66084   191337 |   40118    1847    30811    16.7 |  5.422 % |
c |      3216 |   65666   190398 |   44130    2926    85116    29.1 |  6.126 % |
c |      4924 |   65289   189510 |   48543    4602   161836    35.2 |  6.697 % |
c |      7486 |   64879   188564 |   53398    7110   452576    63.7 |  7.372 % |
c |     11330 |   64473   187562 |   58737   10913   683305    62.6 |  7.983 % |
c |     17096 |   63798   186003 |   64611   16614  1038263    62.5 |  9.074 % |
c |     25745 |   63601   185525 |   71072   25238  1695999    67.2 |  9.379 % |
c |     38720 |   63580   185480 |   78180   38210  2907699    76.1 |  9.414 % |
c |     58183 |   63250   184652 |   85998   57643  5496284    95.4 |  9.904 % |
c |     87378 |   63094   184239 |   94597   86809  9124448   105.1 | 10.123 % |
c |    131168 |   62940   183865 |  104057   49841  5416549   108.7 | 10.354 % |
c |    196852 |   62652   183106 |  114463   24518  1690817    69.0 | 10.741 % |
c |    295380 |   62156   181879 |  125909   22629  1840136    81.3 | 11.502 % |
#### 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.53 0.83 0.90 2/54 27791
Raw data (stat): 27791 (runsolver) R 27790 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 472258007 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0009 s]
Raw data (loadavg): 0.60 0.83 0.90 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 2385 0 0 0 993 6 0 0 25 0 1 0 472258007 12300288 2305 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2305 603 41 0 2962 0
vsize: 12012
[startup+20.0015 s]
Raw data (loadavg): 0.66 0.84 0.90 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 2949 0 0 0 1991 7 0 0 25 0 1 0 472258007 14626816 2869 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3571 2869 603 41 0 3530 0
vsize: 14284
[startup+30.0018 s]
Raw data (loadavg): 0.71 0.84 0.90 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 3361 0 0 0 2990 9 0 0 25 0 1 0 472258007 16379904 3281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3999 3281 603 41 0 3958 0
vsize: 15996
[startup+40.002 s]
Raw data (loadavg): 0.76 0.85 0.90 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 3787 0 0 0 3988 11 0 0 25 0 1 0 472258007 17993728 3707 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3707 603 41 0 4352 0
vsize: 17572
[startup+50.0028 s]
Raw data (loadavg): 0.79 0.85 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 4219 0 0 0 4988 11 0 0 25 0 1 0 472258007 19734528 4139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4818 4139 603 41 0 4777 0
vsize: 19272
[startup+60.0031 s]
Raw data (loadavg): 0.82 0.86 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 4842 0 0 0 5986 14 0 0 25 0 1 0 472258007 22417408 4762 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5473 4762 603 41 0 5432 0
vsize: 21892
[startup+70.0036 s]
Raw data (loadavg): 0.85 0.86 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 5381 0 0 0 6984 15 0 0 25 0 1 0 472258007 24702976 5301 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6031 5301 603 41 0 5990 0
vsize: 24124
[startup+80.0051 s]
Raw data (loadavg): 0.87 0.86 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 5701 0 0 0 7983 16 0 0 25 0 1 0 472258007 25899008 5621 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6323 5621 603 41 0 6282 0
vsize: 25292
[startup+90.0054 s]
Raw data (loadavg): 0.89 0.87 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 6243 0 0 0 8982 18 0 0 25 0 1 0 472258007 28188672 6163 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6882 6163 603 41 0 6841 0
vsize: 27528
[startup+100.006 s]
Raw data (loadavg): 0.91 0.87 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 6969 0 0 0 9980 20 0 0 25 0 1 0 472258007 31158272 6889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7607 6889 603 41 0 7566 0
vsize: 30428
[startup+110.006 s]
Raw data (loadavg): 0.92 0.87 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 7579 0 0 0 10979 21 0 0 25 0 1 0 472258007 33574912 7499 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8197 7499 603 41 0 8156 0
vsize: 32788
[startup+120.007 s]
Raw data (loadavg): 0.93 0.88 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 8181 0 0 0 11977 23 0 0 25 0 1 0 472258007 35999744 8101 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8789 8101 603 41 0 8748 0
vsize: 35156
[startup+130.008 s]
Raw data (loadavg): 0.94 0.88 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 8643 0 0 0 12976 24 0 0 25 0 1 0 472258007 37879808 8563 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9248 8563 603 41 0 9207 0
vsize: 36992
[startup+140.009 s]
Raw data (loadavg): 0.95 0.89 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 8992 0 0 0 13975 26 0 0 25 0 1 0 472258007 39362560 8912 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8912 603 41 0 9569 0
vsize: 38440
[startup+150.009 s]
Raw data (loadavg): 0.96 0.89 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 9374 0 0 0 14974 27 0 0 25 0 1 0 472258007 41107456 9294 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10036 9294 603 41 0 9995 0
vsize: 40144
[startup+160.009 s]
Raw data (loadavg): 0.96 0.89 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 9904 0 0 0 15972 28 0 0 25 0 1 0 472258007 43249664 9824 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10559 9824 603 41 0 10518 0
vsize: 42236
[startup+170.009 s]
Raw data (loadavg): 0.97 0.89 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 10348 0 0 0 16970 31 0 0 25 0 1 0 472258007 45129728 10268 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11018 10268 603 41 0 10977 0
vsize: 44072
[startup+180.009 s]
Raw data (loadavg): 0.97 0.90 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 10708 0 0 0 17968 32 0 0 25 0 1 0 472258007 46604288 10628 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11378 10628 603 41 0 11337 0
vsize: 45512
[startup+190.011 s]
Raw data (loadavg): 0.98 0.90 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 11186 0 0 0 18968 33 0 0 25 0 1 0 472258007 48484352 11106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11837 11106 603 41 0 11796 0
vsize: 47348
[startup+200.01 s]
Raw data (loadavg): 0.98 0.90 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 11648 0 0 0 19965 36 0 0 25 0 1 0 472258007 50360320 11568 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12295 11568 603 41 0 12254 0
vsize: 49180
[startup+210.011 s]
Raw data (loadavg): 0.98 0.91 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 12093 0 0 0 20964 37 0 0 25 0 1 0 472258007 52240384 12013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 12013 603 41 0 12713 0
vsize: 51016
[startup+220.011 s]
Raw data (loadavg): 0.98 0.91 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 12408 0 0 0 21963 38 0 0 25 0 1 0 472258007 53448704 12328 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13049 12328 603 41 0 13008 0
vsize: 52196
[startup+230.012 s]
Raw data (loadavg): 0.99 0.91 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 12828 0 0 0 22962 40 0 0 25 0 1 0 472258007 55185408 12748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13473 12748 603 41 0 13432 0
vsize: 53892
[startup+240.012 s]
Raw data (loadavg): 0.99 0.91 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13312 0 0 0 23960 41 0 0 25 0 1 0 472258007 57204736 13232 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13966 13232 603 41 0 13925 0
vsize: 55864
[startup+250.013 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 24960 42 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+260.014 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 25959 42 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+270.013 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 26959 43 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+280.015 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 27959 43 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+290.015 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 28959 43 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+300.015 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 29959 44 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+310.015 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 30959 44 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+320.016 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 31958 45 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+330.016 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 32958 45 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+340.016 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 33958 45 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+350.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 34958 45 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+360.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 35958 45 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+370.017 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 36957 46 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+380.017 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 37958 46 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+390.018 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 38958 46 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+400.018 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 39958 46 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+410.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13597 0 0 0 40957 46 0 0 25 0 1 0 472258007 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+420.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13599 0 0 0 41957 46 0 0 25 0 1 0 472258007 58277888 13519 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+430.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13599 0 0 0 42957 47 0 0 25 0 1 0 472258007 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+440.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13599 0 0 0 43957 47 0 0 25 0 1 0 472258007 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+450.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13599 0 0 0 44957 47 0 0 25 0 1 0 472258007 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+460.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13599 0 0 0 45957 48 0 0 25 0 1 0 472258007 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+470.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13600 0 0 0 46956 48 0 0 25 0 1 0 472258007 58277888 13520 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14228 13520 603 41 0 14187 0
vsize: 56912
[startup+480.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 13978 0 0 0 47955 49 0 0 25 0 1 0 472258007 59891712 13898 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14622 13898 603 41 0 14581 0
vsize: 58488
[startup+490.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14307 0 0 0 48954 51 0 0 25 0 1 0 472258007 61235200 14227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14950 14227 603 41 0 14909 0
vsize: 59800
[startup+500.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 49953 52 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+510.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 50952 52 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+520.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 51952 53 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+530.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 52952 53 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+540.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 53952 53 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+550.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 54952 53 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+560.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 55952 54 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+570.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 56952 54 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+580.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 57952 54 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+590.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 58952 54 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+600.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 59951 55 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+610.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 60951 55 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+620.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 61951 55 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 62951 56 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 63951 56 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 64951 56 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 65951 56 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 66951 56 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 67951 56 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 68951 57 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 69951 57 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 70950 57 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 71950 58 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 72950 58 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 73949 59 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14587 0 0 0 74949 59 0 0 25 0 1 0 472258007 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14589 0 0 0 75949 60 0 0 25 0 1 0 472258007 62312448 14509 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14509 603 41 0 15172 0
vsize: 60852
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14592 0 0 0 76948 60 0 0 25 0 1 0 472258007 62312448 14512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14512 603 41 0 15172 0
vsize: 60852
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14724 0 0 0 77948 61 0 0 25 0 1 0 472258007 62844928 14644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15343 14644 603 41 0 15302 0
vsize: 61372
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 14993 0 0 0 78947 62 0 0 25 0 1 0 472258007 63913984 14913 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15604 14913 603 41 0 15563 0
vsize: 62416
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 79947 63 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 80947 63 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 81947 63 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 82947 64 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 83947 64 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 84946 64 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+860.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 85946 64 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 86946 65 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 87946 65 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 88945 65 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+900.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 89945 65 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+910.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 90945 66 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+920.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 91945 66 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+930.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 92945 66 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+940.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 93945 66 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 94945 67 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+960.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 95945 67 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+970.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 96945 67 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+980.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 97945 67 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+990.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 98944 68 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 99944 68 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 100944 68 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15068 0 0 0 101944 68 0 0 25 0 1 0 472258007 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15127 0 0 0 102944 69 0 0 25 0 1 0 472258007 64479232 15047 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15047 603 41 0 15701 0
vsize: 62968
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15558 0 0 0 103943 70 0 0 25 0 1 0 472258007 66379776 15478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16206 15478 603 41 0 16165 0
vsize: 64824
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 15892 0 0 0 104942 71 0 0 25 0 1 0 472258007 67743744 15812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16539 15812 603 41 0 16498 0
vsize: 66156
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 16265 0 0 0 105941 72 0 0 25 0 1 0 472258007 69230592 16185 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16902 16185 603 41 0 16861 0
vsize: 67608
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 16634 0 0 0 106941 72 0 0 25 0 1 0 472258007 70737920 16554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16554 603 41 0 17229 0
vsize: 69080
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 16966 0 0 0 107940 73 0 0 25 0 1 0 472258007 72114176 16886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17606 16886 603 41 0 17565 0
vsize: 70424
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 17338 0 0 0 108939 74 0 0 25 0 1 0 472258007 73732096 17258 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18001 17258 603 41 0 17960 0
vsize: 72004
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 17749 0 0 0 109938 75 0 0 25 0 1 0 472258007 75350016 17669 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18396 17669 603 41 0 18355 0
vsize: 73584
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 18138 0 0 0 110937 77 0 0 25 0 1 0 472258007 76951552 18058 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18787 18058 603 41 0 18746 0
vsize: 75148
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 18497 0 0 0 111936 78 0 0 25 0 1 0 472258007 78434304 18417 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19149 18417 603 41 0 19108 0
vsize: 76596
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 18824 0 0 0 112935 79 0 0 25 0 1 0 472258007 79765504 18744 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19474 18744 603 41 0 19433 0
vsize: 77896
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 19161 0 0 0 113933 81 0 0 25 0 1 0 472258007 81108992 19081 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19802 19081 603 41 0 19761 0
vsize: 79208
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 19501 0 0 0 114933 81 0 0 25 0 1 0 472258007 82636800 19421 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20175 19421 603 41 0 20134 0
vsize: 80700
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 19911 0 0 0 115932 83 0 0 25 0 1 0 472258007 84246528 19831 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20568 19831 603 41 0 20527 0
vsize: 82272
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 20252 0 0 0 116931 84 0 0 25 0 1 0 472258007 85721088 20172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20928 20172 603 41 0 20887 0
vsize: 83712
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 20528 0 0 0 117930 85 0 0 25 0 1 0 472258007 86798336 20448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21191 20448 603 41 0 21150 0
vsize: 84764
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 20825 0 0 0 118929 86 0 0 25 0 1 0 472258007 88010752 20745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21487 20745 603 41 0 21446 0
vsize: 85948
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27791
Raw data (stat): 27791 (minisat+) R 27790 26667 26666 0 -1 0 20977 0 0 0 119929 87 0 0 25 0 1 0 472258007 88551424 20897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21619 20897 603 41 0 21578 0
vsize: 86476
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27791
Raw data (stat): 27791 (minisat+) Z 27790 26667 26666 0 -1 12 20979 0 0 0 119929 91 0 0 25 0 1 0 472258007 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.21
CPU user time (s): 1199.29
CPU system time (s): 0.91486
CPU usage (%): 100.008
Max. virtual memory (Kb): 86476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####