PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-lp4l.opb
MD5SUM	3c39e3c2b993ee2185e2a1a3e73b9723
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3744
Optimality of the best value was proved	NO
Number of terms in the objective function	1086
Biggest coefficient in the objective function	283
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	197191
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	283
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	197191
Number of bits of the biggest sum of numbers	18
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	1086
Total number of constraints	1171
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1170
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1086
Trace number 17041

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 09:25:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11921 boxname=wulflinc11 idbench=917 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-lp4l.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-lp4l.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-lp4l.opb
IDLAUNCH: 11921
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        744256 kB
Buffers:         30284 kB
Cached:         239064 kB
SwapCached:          0 kB
Active:         100588 kB
Inactive:       171544 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        744004 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12652 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:45:13 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 11921 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> Adder-cost: 592   maxlim: 2471   bits: 12/12
c ---[ 166]---> BDD-cost:   41
c ---[ 164]---> BDD-cost:   67
c ---[ 162]---> BDD-cost:   99
c ---[ 160]---> BDD-cost:   79
c ---[ 158]---> BDD-cost:   45
c ---[ 156]---> BDD-cost:   69
c ---[ 154]---> BDD-cost:   55
c ---[ 152]---> BDD-cost:   37
c ---[ 150]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   79
c ---[ 144]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   75
c ---[ 140]---> BDD-cost:   77
c ---[ 138]---> BDD-cost:   41
c ---[ 136]---> BDD-cost:   75
c ---[ 134]---> BDD-cost:  107
c ---[ 132]---> BDD-cost:   91
c ---[ 130]---> BDD-cost:  127
c ---[ 128]---> BDD-cost:  123
c ---[ 126]---> BDD-cost:   89
c ---[ 124]---> BDD-cost:   57
c ---[ 122]---> BDD-cost:   89
c ---[ 120]---> BDD-cost:   71
c ---[ 118]---> BDD-cost:  103
c ---[ 116]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:  125
c ---[ 112]---> BDD-cost:   91
c ---[ 110]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:   89
c ---[ 106]---> BDD-cost:   71
c ---[ 104]---> BDD-cost:  129
c ---[ 102]---> BDD-cost:  113
c ---[ 100]---> BDD-cost:  123
c ---[  98]---> BDD-cost:   89
c ---[  96]---> BDD-cost:   61
c ---[  94]---> BDD-cost:   59
c ---[  92]---> BDD-cost:   33
c ---[  90]---> BDD-cost:  123
c ---[  88]---> BDD-cost:  121
c ---[  86]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   45
c ---[  82]---> BDD-cost:   69
c ---[  80]---> BDD-cost:   59
c ---[  78]---> BDD-cost:   33
c ---[  76]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   69
c ---[  72]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   67
c ---[  68]---> BDD-cost:   95
c ---[  66]---> BDD-cost:   85
c ---[  64]---> BDD-cost:  107
c ---[  62]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   43
c ---[  48]---> BDD-cost:   75
c ---[  46]---> BDD-cost:  105
c ---[  44]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   63
c ---[  32]---> BDD-cost:    5
c ---[  30]---> BDD-cost:  169
c ---[  28]---> BDD-cost:  155
c ---[  26]---> BDD-cost:  115
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   83
c ---[  20]---> BDD-cost:  111
c ---[  18]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  161
c ---[  14]---> BDD-cost:  151
c ---[  12]---> BDD-cost:  117
c ---[  10]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   85
c ---[   6]---> BDD-cost:   71
c ---[   4]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   37
c ---[   0]---> Adder-cost: 2160   maxlim: 1059   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   48795   150667 |   16265       0        0     nan |  0.000 % |
c |       101 |   48771   150585 |   17891      99      866     8.7 |  1.208 % |
c |       253 |   48771   150585 |   19680     251    15185    60.5 |  1.208 % |
c |       478 |   48640   150132 |   21648     455    21314    46.8 |  1.417 % |
c |       816 |   48267   148829 |   23813     738    22879    31.0 |  1.987 % |
c |      1322 |   48202   148616 |   26194    1233    31747    25.7 |  2.102 % |
c ==============================================================================
c [1mFound solution: 4400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8142   maxlim: 192791   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1637 |  105092   351761 |   35030    1547    38035    24.6 |  2.102 % |
c |      1737 |  105092   351761 |   38533    1647    40048    24.3 |  1.232 % |
c |      1887 |  105092   351761 |   42386    1797    44469    24.7 |  1.232 % |
c |      2112 |  105045   351596 |   46624    2012    50359    25.0 |  1.259 % |
c |      2451 |  105045   351596 |   51287    2351    74124    31.5 |  1.259 % |
c |      2958 |  105045   351596 |   56416    2858   129083    45.2 |  1.259 % |
c |      3717 |  105021   351512 |   62057    3612   187465    51.9 |  1.270 % |
c ==============================================================================
c [1mFound solution: 4399[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192792   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3965 |  105037   351597 |   35012    3859   208293    54.0 |  1.270 % |
c |      4065 |  105030   351573 |   38513    3958   208900    52.8 |  1.291 % |
c |      4215 |  104949   351298 |   42364    4088   211019    51.6 |  1.355 % |
c |      4441 |  104949   351298 |   46600    4314   234616    54.4 |  1.355 % |
c |      4786 |  104949   351298 |   51261    4659   258137    55.4 |  1.355 % |
c |      5293 |  104949   351298 |   56387    5166   277454    53.7 |  1.355 % |
c |      6053 |  104949   351298 |   62025    5926   320028    54.0 |  1.355 % |
c |      7198 |  104949   351298 |   68228    7071   670489    94.8 |  1.355 % |
c |      8909 |  104949   351298 |   75051    8782  1165749   132.7 |  1.355 % |
c |     11471 |  104937   351256 |   82556   11338  1644203   145.0 |  1.361 % |
c |     15315 |  104905   351145 |   90812   15172  2316541   152.7 |  1.393 % |
c ==============================================================================
c [1mFound solution: 4350[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192841   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15640 |  104908   351189 |   34969   15497  2339609   151.0 |  1.393 % |
c |     15740 |  104908   351189 |   38465   15597  2342183   150.2 |  1.409 % |
c |     15893 |  104908   351189 |   42312   15750  2359749   149.8 |  1.409 % |
c |     16118 |  104908   351189 |   46543   15975  2370167   148.4 |  1.409 % |
c |     16456 |  104908   351189 |   51198   16313  2387710   146.4 |  1.409 % |
c |     16962 |  104908   351189 |   56317   16819  2483345   147.7 |  1.409 % |
c |     17721 |  104908   351189 |   61949   17578  2627421   149.5 |  1.409 % |
c |     18862 |  104908   351189 |   68144   18719  2792725   149.2 |  1.409 % |
c |     20570 |  104908   351189 |   74959   20427  3087136   151.1 |  1.409 % |
c |     23134 |  104893   351136 |   82455   22989  3588189   156.1 |  1.414 % |
c ==============================================================================
c [1mFound solution: 4298[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192893   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26844 |  104898   351211 |   34966   26699  4301039   161.1 |  1.414 % |
c |     26944 |  104898   351211 |   38462   26799  4305591   160.7 |  1.441 % |
c |     27094 |  104898   351211 |   42308   26949  4311694   160.0 |  1.441 % |
c |     27322 |  104898   351211 |   46539   27177  4348093   160.0 |  1.441 % |
c |     27660 |  104898   351211 |   51193   27515  4393154   159.7 |  1.441 % |
c ==============================================================================
c [1mFound solution: 4194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192997   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27764 |  104903   351280 |   34967   27619  4400461   159.3 |  1.441 % |
c |     27864 |  104903   351280 |   38463   27719  4411791   159.2 |  1.467 % |
c |     28016 |  104903   351280 |   42310   27871  4421781   158.7 |  1.467 % |
c |     28241 |  104903   351280 |   46541   28096  4472976   159.2 |  1.467 % |
c |     28580 |  104903   351280 |   51195   28435  4515156   158.8 |  1.467 % |
c |     29086 |  104903   351280 |   56314   28941  4585464   158.4 |  1.467 % |
c |     29846 |  104874   351177 |   61946   29688  4736395   159.5 |  1.483 % |
c |     30985 |  104874   351177 |   68140   30827  4999696   162.2 |  1.483 % |
c |     32694 |  104821   350990 |   74954   32523  5450383   167.6 |  1.510 % |
c |     35256 |  104806   350937 |   82450   35075  5935124   169.2 |  1.515 % |
c |     39101 |  104806   350937 |   90695   38920  6987802   179.5 |  1.515 % |
c |     44869 |  104806   350937 |   99764   44688  8467515   189.5 |  1.515 % |
c |     53518 |  104806   350937 |  109741   53337 10968008   205.6 |  1.515 % |
c |     66500 |  104700   350576 |  120715   66294 14735560   222.3 |  1.606 % |
c ==============================================================================
c [1mFound solution: 4121[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193070   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69640 |  104709   350670 |   34903   69434 15651610   225.4 |  1.606 % |
c |     69740 |  104709   350670 |   38393   19012  3886389   204.4 |  1.638 % |
c |     69894 |  104709   350670 |   42232   19166  3917017   204.4 |  1.638 % |
c |     70121 |  104709   350670 |   46455   19393  3928121   202.6 |  1.638 % |
c |     70459 |  104709   350670 |   51101   19731  3990068   202.2 |  1.638 % |
c |     70965 |  104709   350670 |   56211   20237  4141672   204.7 |  1.638 % |
c |     71724 |  104709   350670 |   61832   20996  4338825   206.7 |  1.638 % |
c |     72866 |  104709   350670 |   68016   22138  4607579   208.1 |  1.638 % |
c |     74575 |  104700   350639 |   74817   23845  4926765   206.6 |  1.643 % |
c |     77138 |  104700   350639 |   82299   26408  5480854   207.5 |  1.643 % |
c ==============================================================================
c [1mFound solution: 4043[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193148   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80841 |  104672   350581 |   34890   30101  6386982   212.2 |  1.643 % |
c |     80941 |  104672   350581 |   38379   30201  6400044   211.9 |  1.712 % |
c |     81093 |  104672   350581 |   42216   30353  6413301   211.3 |  1.712 % |
c |     81318 |  104672   350581 |   46438   30578  6444519   210.8 |  1.712 % |
c |     81658 |  104672   350581 |   51082   30918  6503598   210.3 |  1.712 % |
c |     82165 |  104631   350440 |   56190   31417  6550425   208.5 |  1.744 % |
c |     82924 |  104631   350440 |   61809   32176  6708464   208.5 |  1.744 % |
c |     84064 |  104622   350409 |   67990   33312  7083497   212.6 |  1.749 % |
c |     85772 |  104622   350409 |   74789   35020  7492948   214.0 |  1.749 % |
c |     88334 |  104622   350409 |   82268   37582  8312550   221.2 |  1.749 % |
c |     92178 |  104622   350409 |   90495   41426  9514083   229.7 |  1.749 % |
c |     97944 |  104622   350409 |   99545   47192 11465134   242.9 |  1.749 % |
c |    106593 |  104622   350409 |  109499   55841 14011388   250.9 |  1.749 % |
c |    119568 |  104568   350219 |  120449   68810 18366261   266.9 |  1.803 % |
c |    139032 |  104568   350219 |  132494   88274 25930698   293.8 |  1.803 % |
c ==============================================================================
c [1mFound solution: 4011[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193180   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165351 |  104516   350069 |   34838  114580 33490901   292.3 |  1.803 % |
c |    165451 |  104516   350069 |   38321   23164  3211315   138.6 |  1.882 % |
c |    165604 |  104516   350069 |   42153   23317  3256163   139.6 |  1.882 % |
c |    165829 |  104516   350069 |   46369   23542  3286511   139.6 |  1.882 % |
c |    166167 |  104516   350069 |   51006   23880  3370576   141.1 |  1.882 % |
c |    166674 |  104516   350069 |   56106   24387  3586967   147.1 |  1.882 % |
c |    167434 |  104516   350069 |   61717   25147  3906003   155.3 |  1.882 % |
c |    168573 |  104516   350069 |   67889   26286  4086362   155.5 |  1.882 % |
c |    170281 |  104516   350069 |   74678   27994  4586881   163.9 |  1.882 % |
c |    172843 |  104516   350069 |   82146   30556  5421200   177.4 |  1.882 % |
c |    176690 |  104516   350069 |   90360   34403  6332141   184.1 |  1.882 % |
c |    182456 |  104516   350069 |   99396   40169  8018374   199.6 |  1.882 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 -CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 -CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 -CO100081_bit0 -CO100082_bit0 -CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 -CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 CO100109_bit0 -CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 -CO100135_bit0 -CO100136_bit0 CO100137_bit0 -CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 -CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 -CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 -CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 -CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 CO100292_bit0 -CO100293_bit0 -CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 -CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 -CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 CO100453_bit0 -CO100454_bit0 -CO100455_bit0 -CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 -CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 -CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 -CO100704_bit0 -CO100705_bit0 CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 -CO100751_bit0 -CO100752_bit0 CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 -CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit#### 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.45 0.84 0.91 2/54 32084
Raw data (stat): 32084 (runsolver) R 32083 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485757494 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.0006 s]
Raw data (loadavg): 0.53 0.85 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 6395 0 0 0 984 13 0 0 25 0 1 0 485757494 27475968 5559 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6708 5559 603 41 0 6667 0
vsize: 26832
[startup+20.0018 s]
Raw data (loadavg): 0.60 0.85 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 7052 0 0 0 1983 14 0 0 25 0 1 0 485757494 29478912 6044 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7197 6044 603 41 0 7156 0
vsize: 28788
[startup+30.0028 s]
Raw data (loadavg): 0.66 0.86 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 7656 0 0 0 2982 16 0 0 25 0 1 0 485757494 31948800 6648 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7800 6648 603 41 0 7759 0
vsize: 31200
[startup+40.0029 s]
Raw data (loadavg): 0.71 0.86 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 8152 0 0 0 3980 18 0 0 25 0 1 0 485757494 33968128 7144 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8293 7144 603 41 0 8252 0
vsize: 33172
[startup+50.0042 s]
Raw data (loadavg): 0.76 0.87 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 8552 0 0 0 4979 19 0 0 25 0 1 0 485757494 35590144 7544 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8689 7544 603 41 0 8648 0
vsize: 34756
[startup+60.0049 s]
Raw data (loadavg): 0.79 0.87 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 9028 0 0 0 5978 21 0 0 25 0 1 0 485757494 37122048 7909 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9063 7909 603 41 0 9022 0
vsize: 36252
[startup+70.0053 s]
Raw data (loadavg): 0.83 0.87 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 9505 0 0 0 6975 23 0 0 25 0 1 0 485757494 39129088 8386 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9553 8386 603 41 0 9512 0
vsize: 38212
[startup+80.0055 s]
Raw data (loadavg): 0.85 0.88 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 10000 0 0 0 7974 24 0 0 25 0 1 0 485757494 41148416 8881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10046 8881 603 41 0 10005 0
vsize: 40184
[startup+90.0066 s]
Raw data (loadavg): 0.87 0.88 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 10465 0 0 0 8973 26 0 0 25 0 1 0 485757494 42909696 9346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10476 9346 603 41 0 10435 0
vsize: 41904
[startup+100.007 s]
Raw data (loadavg): 0.89 0.88 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 10979 0 0 0 9971 27 0 0 25 0 1 0 485757494 45056000 9860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11000 9860 603 41 0 10959 0
vsize: 44000
[startup+110.008 s]
Raw data (loadavg): 0.91 0.89 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 11542 0 0 0 10968 31 0 0 25 0 1 0 485757494 46161920 10132 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11270 10132 603 41 0 11229 0
vsize: 45080
[startup+120.009 s]
Raw data (loadavg): 0.92 0.89 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 11977 0 0 0 11967 32 0 0 25 0 1 0 485757494 47902720 10567 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11695 10567 603 41 0 11654 0
vsize: 46780
[startup+130.008 s]
Raw data (loadavg): 0.93 0.89 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 12507 0 0 0 12966 33 0 0 25 0 1 0 485757494 50057216 11097 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12221 11097 603 41 0 12180 0
vsize: 48884
[startup+140.008 s]
Raw data (loadavg): 0.94 0.90 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 12888 0 0 0 13965 34 0 0 25 0 1 0 485757494 51793920 11478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12645 11478 603 41 0 12604 0
vsize: 50580
[startup+150.009 s]
Raw data (loadavg): 0.95 0.90 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 13370 0 0 0 14964 35 0 0 25 0 1 0 485757494 53809152 11960 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13137 11960 603 41 0 13096 0
vsize: 52548
[startup+160.009 s]
Raw data (loadavg): 0.96 0.90 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 13888 0 0 0 15963 36 0 0 25 0 1 0 485757494 55816192 12478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13627 12478 603 41 0 13586 0
vsize: 54508
[startup+170.009 s]
Raw data (loadavg): 0.96 0.91 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 14375 0 0 0 16962 38 0 0 25 0 1 0 485757494 57831424 12965 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14119 12965 603 41 0 14078 0
vsize: 56476
[startup+180.009 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 15030 0 0 0 17961 39 0 0 25 0 1 0 485757494 60526592 13620 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14777 13620 603 41 0 14736 0
vsize: 59108
[startup+190.01 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 15553 0 0 0 18959 41 0 0 25 0 1 0 485757494 62685184 14143 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15304 14143 603 41 0 15263 0
vsize: 61216
[startup+200.01 s]
Raw data (loadavg): 0.98 0.91 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 16012 0 0 0 19959 42 0 0 25 0 1 0 485757494 64561152 14602 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15762 14602 603 41 0 15721 0
vsize: 63048
[startup+210.011 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 16412 0 0 0 20958 42 0 0 25 0 1 0 485757494 66174976 15002 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16156 15002 603 41 0 16115 0
vsize: 64624
[startup+220.011 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 16785 0 0 0 21957 43 0 0 25 0 1 0 485757494 67661824 15375 4294967295 134512640 134672761 3221224544 3221223744 134557796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16519 15376 603 41 0 16478 0
vsize: 66076
[startup+230.011 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 17313 0 0 0 22956 45 0 0 25 0 1 0 485757494 69816320 15903 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17045 15903 603 41 0 17004 0
vsize: 68180
[startup+240.012 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 17842 0 0 0 23955 46 0 0 25 0 1 0 485757494 71958528 16432 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17568 16432 603 41 0 17527 0
vsize: 70272
[startup+250.011 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 18343 0 0 0 24954 48 0 0 25 0 1 0 485757494 74088448 16933 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18088 16933 603 41 0 18047 0
vsize: 72352
[startup+260.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 18830 0 0 0 25953 49 0 0 25 0 1 0 485757494 76095488 17420 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18578 17420 603 41 0 18537 0
vsize: 74312
[startup+270.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 19148 0 0 0 26952 49 0 0 25 0 1 0 485757494 77303808 17738 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18873 17738 603 41 0 18832 0
vsize: 75492
[startup+280.012 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 19644 0 0 0 27952 50 0 0 25 0 1 0 485757494 79314944 18234 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19364 18234 603 41 0 19323 0
vsize: 77456
[startup+290.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 20111 0 0 0 28951 51 0 0 25 0 1 0 485757494 81334272 18701 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19857 18701 603 41 0 19816 0
vsize: 79428
[startup+300.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 20609 0 0 0 29950 52 0 0 25 0 1 0 485757494 83329024 19199 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20344 19199 603 41 0 20303 0
vsize: 81376
[startup+310.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 21144 0 0 0 30950 53 0 0 25 0 1 0 485757494 85479424 19734 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20869 19734 603 41 0 20828 0
vsize: 83476
[startup+320.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 21722 0 0 0 31948 55 0 0 25 0 1 0 485757494 87887872 20312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21457 20312 603 41 0 21416 0
vsize: 85828
[startup+330.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 22222 0 0 0 32946 56 0 0 25 0 1 0 485757494 90161152 20812 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22012 20812 603 41 0 21971 0
vsize: 88048
[startup+340.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 22645 0 0 0 33946 57 0 0 25 0 1 0 485757494 91910144 21235 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22439 21235 603 41 0 22398 0
vsize: 89756
[startup+350.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23156 0 0 0 34945 58 0 0 25 0 1 0 485757494 93511680 21648 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+360.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23156 0 0 0 35945 58 0 0 25 0 1 0 485757494 93511680 21648 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+370.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23156 0 0 0 36945 58 0 0 25 0 1 0 485757494 93511680 21648 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+380.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23156 0 0 0 37945 58 0 0 25 0 1 0 485757494 93511680 21648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+390.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23156 0 0 0 38945 58 0 0 25 0 1 0 485757494 93511680 21648 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+400.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23156 0 0 0 39946 58 0 0 25 0 1 0 485757494 93511680 21648 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+410.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 40946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+420.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 41946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+430.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 42946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+440.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 43946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+450.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 44946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+460.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 45946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+470.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 46946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+480.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 47946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+490.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 48946 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+500.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 49947 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223648 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+510.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 50947 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+520.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 51947 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+530.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 52947 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+540.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 53947 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+550.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 54948 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+560.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 55948 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+570.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 56948 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+580.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23199 0 0 0 57948 58 0 0 25 0 1 0 485757494 93511680 21649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23510 0 0 0 58948 59 0 0 25 0 1 0 485757494 94830592 21960 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23152 21960 603 41 0 23111 0
vsize: 92608
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 23989 0 0 0 59947 60 0 0 25 0 1 0 485757494 96829440 22439 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23640 22439 603 41 0 23599 0
vsize: 94560
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 24418 0 0 0 60946 62 0 0 25 0 1 0 485757494 98533376 22868 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24056 22868 603 41 0 24015 0
vsize: 96224
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 24992 0 0 0 61945 63 0 0 25 0 1 0 485757494 100945920 23442 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24645 23442 603 41 0 24604 0
vsize: 98580
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 25584 0 0 0 62943 65 0 0 25 0 1 0 485757494 103378944 24034 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25239 24034 603 41 0 25198 0
vsize: 100956
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 26100 0 0 0 63942 66 0 0 25 0 1 0 485757494 105398272 24550 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25732 24550 603 41 0 25691 0
vsize: 102928
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 26559 0 0 0 64941 67 0 0 25 0 1 0 485757494 107290624 25009 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26194 25009 603 41 0 26153 0
vsize: 104776
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 26942 0 0 0 65941 68 0 0 25 0 1 0 485757494 108904448 25392 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26588 25392 603 41 0 26547 0
vsize: 106352
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 27440 0 0 0 66940 69 0 0 25 0 1 0 485757494 110915584 25890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27079 25890 603 41 0 27038 0
vsize: 108316
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 27879 0 0 0 67939 70 0 0 25 0 1 0 485757494 112693248 26329 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27513 26329 603 41 0 27472 0
vsize: 110052
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 28257 0 0 0 68938 71 0 0 25 0 1 0 485757494 114298880 26707 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27905 26707 603 41 0 27864 0
vsize: 111620
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 28659 0 0 0 69936 73 0 0 25 0 1 0 485757494 115892224 27109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28294 27109 603 41 0 28253 0
vsize: 113176
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 28980 0 0 0 70936 73 0 0 25 0 1 0 485757494 117219328 27430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28618 27430 603 41 0 28577 0
vsize: 114472
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 29313 0 0 0 71935 74 0 0 25 0 1 0 485757494 118546432 27763 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28942 27763 603 41 0 28901 0
vsize: 115768
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 29661 0 0 0 72935 75 0 0 25 0 1 0 485757494 120016896 28111 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29301 28111 603 41 0 29260 0
vsize: 117204
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 30031 0 0 0 73934 75 0 0 25 0 1 0 485757494 121483264 28481 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29659 28481 603 41 0 29618 0
vsize: 118636
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 30373 0 0 0 74934 76 0 0 25 0 1 0 485757494 122941440 28823 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30015 28823 603 41 0 29974 0
vsize: 120060
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 30762 0 0 0 75933 77 0 0 25 0 1 0 485757494 124522496 29212 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30401 29212 603 41 0 30360 0
vsize: 121604
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 31182 0 0 0 76932 78 0 0 25 0 1 0 485757494 126259200 29632 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30825 29632 603 41 0 30784 0
vsize: 123300
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 31516 0 0 0 77932 79 0 0 25 0 1 0 485757494 127606784 29966 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31154 29966 603 41 0 31113 0
vsize: 124616
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 31910 0 0 0 78930 80 0 0 25 0 1 0 485757494 129183744 30360 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31539 30360 603 41 0 31498 0
vsize: 126156
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 32292 0 0 0 79929 81 0 0 25 0 1 0 485757494 130785280 30742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31930 30742 603 41 0 31889 0
vsize: 127720
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 32592 0 0 0 80929 82 0 0 25 0 1 0 485757494 131989504 31042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32224 31042 603 41 0 32183 0
vsize: 128896
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 32927 0 0 0 81928 83 0 0 25 0 1 0 485757494 133455872 31377 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32582 31377 603 41 0 32541 0
vsize: 130328
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 33250 0 0 0 82928 84 0 0 25 0 1 0 485757494 134660096 31700 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32876 31700 603 41 0 32835 0
vsize: 131504
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 33580 0 0 0 83927 85 0 0 25 0 1 0 485757494 136118272 32030 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33232 32030 603 41 0 33191 0
vsize: 132928
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 33995 0 0 0 84926 86 0 0 25 0 1 0 485757494 137740288 32445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33628 32445 603 41 0 33587 0
vsize: 134512
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 34374 0 0 0 85925 86 0 0 25 0 1 0 485757494 139354112 32824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34022 32824 603 41 0 33981 0
vsize: 136088
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 34795 0 0 0 86924 87 0 0 25 0 1 0 485757494 140972032 33245 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34417 33245 603 41 0 34376 0
vsize: 137668
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 35202 0 0 0 87923 88 0 0 25 0 1 0 485757494 142704640 33652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34840 33652 603 41 0 34799 0
vsize: 139360
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 35595 0 0 0 88922 90 0 0 25 0 1 0 485757494 144306176 34045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35231 34045 603 41 0 35190 0
vsize: 140924
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 35914 0 0 0 89922 90 0 0 25 0 1 0 485757494 145637376 34364 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35556 34364 603 41 0 35515 0
vsize: 142224
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 36295 0 0 0 90922 90 0 0 25 0 1 0 485757494 147099648 34745 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35913 34745 603 41 0 35872 0
vsize: 143652
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 36664 0 0 0 91921 91 0 0 25 0 1 0 485757494 148672512 35114 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36297 35114 603 41 0 36256 0
vsize: 145188
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 37011 0 0 0 92921 92 0 0 25 0 1 0 485757494 150147072 35461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36657 35461 603 41 0 36616 0
vsize: 146628
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 37362 0 0 0 93920 93 0 0 25 0 1 0 485757494 151494656 35812 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36986 35813 603 41 0 36945 0
vsize: 147944
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 37722 0 0 0 94919 94 0 0 25 0 1 0 485757494 152969216 36172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37346 36172 603 41 0 37305 0
vsize: 149384
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 38100 0 0 0 95919 95 0 0 25 0 1 0 485757494 154558464 36550 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37734 36550 603 41 0 37693 0
vsize: 150936
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 38578 0 0 0 96918 96 0 0 25 0 1 0 485757494 156450816 37028 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38196 37028 603 41 0 38155 0
vsize: 152784
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 38841 0 0 0 97917 97 0 0 25 0 1 0 485757494 157540352 37291 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38462 37291 603 41 0 38421 0
vsize: 153848
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 39131 0 0 0 98916 98 0 0 25 0 1 0 485757494 158752768 37581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38758 37581 603 41 0 38717 0
vsize: 155032
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 39340 0 0 0 99916 98 0 0 25 0 1 0 485757494 159555584 37790 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38954 37790 603 41 0 38913 0
vsize: 155816
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 39597 0 0 0 100915 99 0 0 25 0 1 0 485757494 160628736 38047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39216 38047 603 41 0 39175 0
vsize: 156864
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 39903 0 0 0 101915 100 0 0 25 0 1 0 485757494 161845248 38353 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39513 38353 603 41 0 39472 0
vsize: 158052
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 40345 0 0 0 102914 101 0 0 25 0 1 0 485757494 163704832 38795 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39967 38795 603 41 0 39926 0
vsize: 159868
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 40822 0 0 0 103913 102 0 0 25 0 1 0 485757494 165699584 39272 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40454 39272 603 41 0 40413 0
vsize: 161816
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41128 0 0 0 104913 102 0 0 25 0 1 0 485757494 166899712 39578 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40747 39578 603 41 0 40706 0
vsize: 162988
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41479 0 0 0 105911 104 0 0 25 0 1 0 485757494 168366080 39929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41105 39929 603 41 0 41064 0
vsize: 164420
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 106911 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223696 1074744273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 107910 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 108911 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 109911 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 110911 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 111911 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 112911 104 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 113911 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 114912 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 115912 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 116912 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 117912 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 118912 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32084
Raw data (stat): 32084 (minisat+) R 32083 32461 32460 0 -1 0 41743 0 0 0 119913 105 0 0 25 0 1 0 485757494 168923136 40087 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32084
Raw data (stat): 32084 (minisat+) Z 32083 32461 32460 0 -1 12 41746 0 0 0 119913 112 0 0 25 0 1 0 485757494 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: 10
Real time (s): 1200.12
CPU time (s): 1200.26
CPU user time (s): 1199.13
CPU system time (s): 1.12483
CPU usage (%): 100.012
Max. virtual memory (Kb): 164964
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####