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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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	3684
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.3
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 19174

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 18:08:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16913 boxname=wulflinc2 idbench=1301 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-lp4l.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-lp4l.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-lp4l.opb
IDLAUNCH: 16913
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        902348 kB
Buffers:         21336 kB
Cached:          88152 kB
SwapCached:       3324 kB
Active:          39104 kB
Inactive:        75180 kB
HighTotal:      131008 kB
HighFree:        44072 kB
LowTotal:       903652 kB
LowFree:        858276 kB
SwapTotal:     2097136 kB
SwapFree:      2092928 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            12468 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:28:57 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 16913 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.89 0.93 0.90 2/54 2545
Raw data (stat): 2545 (runsolver) R 2544 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488904865 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 6395 0 0 0 982 16 0 0 25 0 1 0 488904865 27475968 5559 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6708 5559 603 41 0 6667 0
vsize: 26832
[startup+20.0021 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 7032 0 0 0 1980 19 0 0 25 0 1 0 488904865 29343744 6024 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7164 6024 603 41 0 7123 0
vsize: 28656
[startup+30.0028 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 7631 0 0 0 2978 21 0 0 25 0 1 0 488904865 31813632 6623 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7767 6623 603 41 0 7726 0
vsize: 31068
[startup+40.0029 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 8123 0 0 0 3975 23 0 0 25 0 1 0 488904865 33832960 7115 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8260 7115 603 41 0 8219 0
vsize: 33040
[startup+50.0032 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 8524 0 0 0 4974 25 0 0 25 0 1 0 488904865 35454976 7516 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8656 7516 603 41 0 8615 0
vsize: 34624
[startup+60.0029 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 9026 0 0 0 5972 27 0 0 25 0 1 0 488904865 36986880 7907 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9030 7907 603 41 0 8989 0
vsize: 36120
[startup+70.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 9479 0 0 0 6971 28 0 0 25 0 1 0 488904865 38993920 8360 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9520 8360 603 41 0 9479 0
vsize: 38080
[startup+80.0043 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 9948 0 0 0 7969 30 0 0 25 0 1 0 488904865 40878080 8829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9980 8829 603 41 0 9939 0
vsize: 39920
[startup+90.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 10380 0 0 0 8968 32 0 0 25 0 1 0 488904865 42639360 9261 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9261 603 41 0 10369 0
vsize: 41640
[startup+100.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 10937 0 0 0 9966 33 0 0 25 0 1 0 488904865 44920832 9818 4294967295 134512640 134672761 3221224560 3221223744 134559588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10967 9818 603 41 0 10926 0
vsize: 43868
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 11518 0 0 0 10965 34 0 0 25 0 1 0 488904865 46026752 10108 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11237 10108 603 41 0 11196 0
vsize: 44948
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 11880 0 0 0 11964 36 0 0 25 0 1 0 488904865 47505408 10470 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11598 10470 603 41 0 11557 0
vsize: 46392
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 12384 0 0 0 12961 38 0 0 25 0 1 0 488904865 49655808 10974 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12123 10974 603 41 0 12082 0
vsize: 48492
[startup+140.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 12777 0 0 0 13960 40 0 0 25 0 1 0 488904865 51388416 11367 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12546 11367 603 41 0 12505 0
vsize: 50184
[startup+150.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 13265 0 0 0 14958 42 0 0 25 0 1 0 488904865 53272576 11855 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 11855 603 41 0 12965 0
vsize: 52024
[startup+160.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 13728 0 0 0 15957 43 0 0 25 0 1 0 488904865 55279616 12318 4294967295 134512640 134672761 3221224560 3221223664 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13496 12318 603 41 0 13455 0
vsize: 53984
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 14211 0 0 0 16956 45 0 0 25 0 1 0 488904865 57155584 12801 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13954 12801 603 41 0 13913 0
vsize: 55816
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 14790 0 0 0 17954 46 0 0 25 0 1 0 488904865 59584512 13380 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14547 13380 603 41 0 14506 0
vsize: 58188
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 15339 0 0 0 18953 48 0 0 25 0 1 0 488904865 61739008 13929 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15073 13929 603 41 0 15032 0
vsize: 60292
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 15851 0 0 0 19951 50 0 0 25 0 1 0 488904865 63889408 14441 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15598 14441 603 41 0 15557 0
vsize: 62392
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 16230 0 0 0 20950 51 0 0 25 0 1 0 488904865 65372160 14820 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15960 14820 603 41 0 15919 0
vsize: 63840
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 16608 0 0 0 21949 52 0 0 25 0 1 0 488904865 66977792 15198 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16352 15198 603 41 0 16311 0
vsize: 65408
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 17053 0 0 0 22949 52 0 0 25 0 1 0 488904865 68739072 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16782 15643 603 41 0 16741 0
vsize: 67128
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 17594 0 0 0 23947 54 0 0 25 0 1 0 488904865 71016448 16184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17338 16184 603 41 0 17297 0
vsize: 69352
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 18095 0 0 0 24945 56 0 0 25 0 1 0 488904865 73011200 16685 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17825 16685 603 41 0 17784 0
vsize: 71300
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 18567 0 0 0 25944 58 0 0 25 0 1 0 488904865 75026432 17157 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18317 17157 603 41 0 18276 0
vsize: 73268
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 18919 0 0 0 26943 59 0 0 25 0 1 0 488904865 76365824 17509 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18644 17509 603 41 0 18603 0
vsize: 74576
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 19373 0 0 0 27942 60 0 0 25 0 1 0 488904865 78241792 17963 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19102 17963 603 41 0 19061 0
vsize: 76408
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 19794 0 0 0 28940 62 0 0 25 0 1 0 488904865 79978496 18384 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19526 18384 603 41 0 19485 0
vsize: 78104
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 20316 0 0 0 29939 64 0 0 25 0 1 0 488904865 82132992 18906 4294967295 134512640 134672761 3221224560 3221223664 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20052 18906 603 41 0 20011 0
vsize: 80208
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 20795 0 0 0 30937 65 0 0 25 0 1 0 488904865 84000768 19385 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20508 19385 603 41 0 20467 0
vsize: 82032
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 21346 0 0 0 31936 66 0 0 25 0 1 0 488904865 86286336 19936 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21066 19936 603 41 0 21025 0
vsize: 84264
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 21908 0 0 0 32934 68 0 0 25 0 1 0 488904865 88821760 20498 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21685 20498 603 41 0 21644 0
vsize: 86740
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 22377 0 0 0 33933 70 0 0 25 0 1 0 488904865 90832896 20967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22176 20967 603 41 0 22135 0
vsize: 88704
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 22807 0 0 0 34932 71 0 0 25 0 1 0 488904865 92585984 21397 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22604 21397 603 41 0 22563 0
vsize: 90416
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23156 0 0 0 35931 72 0 0 25 0 1 0 488904865 93511680 21648 4294967295 134512640 134672761 3221224560 3221223728 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+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23156 0 0 0 36931 72 0 0 25 0 1 0 488904865 93511680 21648 4294967295 134512640 134672761 3221224560 3221223664 134560218 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23156 0 0 0 37931 73 0 0 25 0 1 0 488904865 93511680 21648 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23156 0 0 0 38931 73 0 0 25 0 1 0 488904865 93511680 21648 4294967295 134512640 134672761 3221224560 3221223732 134556639 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23156 0 0 0 39931 73 0 0 25 0 1 0 488904865 93511680 21648 4294967295 134512640 134672761 3221224560 3221223728 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+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23156 0 0 0 40930 73 0 0 25 0 1 0 488904865 93511680 21648 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21648 603 41 0 22789 0
vsize: 91320
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 41930 74 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 42930 74 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134561005 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 43930 74 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 44930 75 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134560876 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 45929 75 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223696 134560706 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 46929 76 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 47929 76 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 48929 76 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 49929 76 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 50929 77 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 51929 77 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 52929 77 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 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+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 53928 77 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134560867 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 54928 78 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 55928 78 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223664 134560196 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 56928 78 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 57928 79 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223664 134559998 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23199 0 0 0 58927 79 0 0 25 0 1 0 488904865 93511680 21649 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21649 603 41 0 22789 0
vsize: 91320
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23428 0 0 0 59926 80 0 0 25 0 1 0 488904865 94560256 21878 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23086 21878 603 41 0 23045 0
vsize: 92344
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 23839 0 0 0 60925 82 0 0 25 0 1 0 488904865 96165888 22289 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23478 22289 603 41 0 23437 0
vsize: 93912
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 24369 0 0 0 61923 84 0 0 25 0 1 0 488904865 98402304 22819 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24024 22819 603 41 0 23983 0
vsize: 96096
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 24795 0 0 0 62922 85 0 0 25 0 1 0 488904865 100155392 23245 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24452 23245 603 41 0 24411 0
vsize: 97808
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 25407 0 0 0 63920 87 0 0 25 0 1 0 488904865 102567936 23857 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25041 23857 603 41 0 25000 0
vsize: 100164
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 25924 0 0 0 64919 89 0 0 25 0 1 0 488904865 104722432 24374 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25567 24374 603 41 0 25526 0
vsize: 102268
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 26419 0 0 0 65917 91 0 0 25 0 1 0 488904865 106754048 24869 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26063 24869 603 41 0 26022 0
vsize: 104252
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 26777 0 0 0 66916 92 0 0 25 0 1 0 488904865 108228608 25227 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26423 25227 603 41 0 26382 0
vsize: 105692
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 27246 0 0 0 67915 93 0 0 25 0 1 0 488904865 110116864 25696 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26884 25696 603 41 0 26843 0
vsize: 107536
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 27694 0 0 0 68914 94 0 0 25 0 1 0 488904865 111976448 26144 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27338 26144 603 41 0 27297 0
vsize: 109352
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 28099 0 0 0 69912 96 0 0 25 0 1 0 488904865 113635328 26549 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27743 26549 603 41 0 27702 0
vsize: 110972
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 28465 0 0 0 70911 97 0 0 25 0 1 0 488904865 115101696 26915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28101 26915 603 41 0 28060 0
vsize: 112404
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 28830 0 0 0 71910 98 0 0 25 0 1 0 488904865 116690944 27280 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28489 27280 603 41 0 28448 0
vsize: 113956
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 29150 0 0 0 72909 99 0 0 25 0 1 0 488904865 117882880 27600 4294967295 134512640 134672761 3221224560 3221223744 134558909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28780 27600 603 41 0 28739 0
vsize: 115120
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 29470 0 0 0 73908 101 0 0 25 0 1 0 488904865 119214080 27920 4294967295 134512640 134672761 3221224560 3221223744 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29105 27920 603 41 0 29064 0
vsize: 116420
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 29836 0 0 0 74908 102 0 0 25 0 1 0 488904865 120684544 28286 4294967295 134512640 134672761 3221224560 3221223664 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29464 28286 603 41 0 29423 0
vsize: 117856
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 30186 0 0 0 75906 103 0 0 25 0 1 0 488904865 122142720 28636 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29820 28636 603 41 0 29779 0
vsize: 119280
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 30567 0 0 0 76906 104 0 0 25 0 1 0 488904865 123727872 29017 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30207 29017 603 41 0 30166 0
vsize: 120828
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 30922 0 0 0 77905 105 0 0 25 0 1 0 488904865 125181952 29372 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30562 29372 603 41 0 30521 0
vsize: 122248
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 31350 0 0 0 78904 106 0 0 25 0 1 0 488904865 126939136 29800 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30991 29800 603 41 0 30950 0
vsize: 123964
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 31697 0 0 0 79903 107 0 0 25 0 1 0 488904865 128401408 30147 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31348 30147 603 41 0 31307 0
vsize: 125392
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 32083 0 0 0 80902 108 0 0 25 0 1 0 488904865 129978368 30533 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31733 30533 603 41 0 31692 0
vsize: 126932
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 32399 0 0 0 81901 109 0 0 25 0 1 0 488904865 131190784 30849 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32029 30849 603 41 0 31988 0
vsize: 128116
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 32716 0 0 0 82901 109 0 0 25 0 1 0 488904865 132509696 31166 4294967295 134512640 134672761 3221224560 3221223664 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32351 31166 603 41 0 32310 0
vsize: 129404
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 33061 0 0 0 83900 110 0 0 25 0 1 0 488904865 133988352 31511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32712 31511 603 41 0 32671 0
vsize: 130848
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 33326 0 0 0 84899 111 0 0 25 0 1 0 488904865 135061504 31776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32974 31776 603 41 0 32933 0
vsize: 131896
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 33660 0 0 0 85898 113 0 0 25 0 1 0 488904865 136384512 32110 4294967295 134512640 134672761 3221224560 3221223664 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33297 32110 603 41 0 33256 0
vsize: 133188
[startup+870.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 34121 0 0 0 86897 114 0 0 25 0 1 0 488904865 138268672 32571 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33757 32571 603 41 0 33716 0
vsize: 135028
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 34479 0 0 0 87896 116 0 0 25 0 1 0 488904865 139763712 32929 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34122 32929 603 41 0 34081 0
vsize: 136488
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 34906 0 0 0 88894 118 0 0 25 0 1 0 488904865 141516800 33356 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34550 33356 603 41 0 34509 0
vsize: 138200
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 35299 0 0 0 89893 119 0 0 25 0 1 0 488904865 143110144 33749 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34939 33749 603 41 0 34898 0
vsize: 139756
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 35671 0 0 0 90891 121 0 0 25 0 1 0 488904865 144576512 34121 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35297 34121 603 41 0 35256 0
vsize: 141188
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 35974 0 0 0 91890 122 0 0 25 0 1 0 488904865 145895424 34424 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35619 34424 603 41 0 35578 0
vsize: 142476
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 36399 0 0 0 92889 123 0 0 25 0 1 0 488904865 147623936 34849 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36041 34849 603 41 0 36000 0
vsize: 144164
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 36720 0 0 0 93889 124 0 0 25 0 1 0 488904865 148942848 35170 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36363 35170 603 41 0 36322 0
vsize: 145452
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 37086 0 0 0 94887 125 0 0 25 0 1 0 488904865 150421504 35536 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36724 35536 603 41 0 36683 0
vsize: 146896
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 37421 0 0 0 95887 126 0 0 25 0 1 0 488904865 151764992 35871 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37052 35871 603 41 0 37011 0
vsize: 148208
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 37756 0 0 0 96886 127 0 0 25 0 1 0 488904865 153104384 36206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37379 36206 603 41 0 37338 0
vsize: 149516
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 38162 0 0 0 97884 129 0 0 25 0 1 0 488904865 154832896 36612 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37801 36612 603 41 0 37760 0
vsize: 151204
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 38608 0 0 0 98883 130 0 0 25 0 1 0 488904865 156585984 37058 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38229 37058 603 41 0 38188 0
vsize: 152916
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 38866 0 0 0 99883 131 0 0 25 0 1 0 488904865 157675520 37316 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38495 37316 603 41 0 38454 0
vsize: 153980
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 39153 0 0 0 100882 132 0 0 25 0 1 0 488904865 158887936 37603 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38791 37603 603 41 0 38750 0
vsize: 155164
[startup+1020.04 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 39357 0 0 0 101881 133 0 0 25 0 1 0 488904865 159690752 37807 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38987 37807 603 41 0 38946 0
vsize: 155948
[startup+1030.04 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 39607 0 0 0 102880 134 0 0 25 0 1 0 488904865 160628736 38057 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39216 38057 603 41 0 39175 0
vsize: 156864
[startup+1040.04 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 39906 0 0 0 103879 135 0 0 25 0 1 0 488904865 161845248 38356 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39513 38356 603 41 0 39472 0
vsize: 158052
[startup+1050.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 40342 0 0 0 104877 137 0 0 25 0 1 0 488904865 163704832 38792 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39967 38792 603 41 0 39926 0
vsize: 159868
[startup+1060.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 40810 0 0 0 105876 139 0 0 25 0 1 0 488904865 165568512 39260 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40422 39260 603 41 0 40381 0
vsize: 161688
[startup+1070.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41120 0 0 0 106875 140 0 0 25 0 1 0 488904865 166899712 39570 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40747 39570 603 41 0 40706 0
vsize: 162988
[startup+1080.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41465 0 0 0 107874 141 0 0 25 0 1 0 488904865 168230912 39915 4294967295 134512640 134672761 3221224560 3221223744 134559345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41072 39915 603 41 0 41031 0
vsize: 164288
[startup+1090.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 108873 142 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223728 134560980 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.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 109873 142 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223664 134560196 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.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 110873 142 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223720 134560076 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.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 111873 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223728 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+1130.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 112873 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223728 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+1140.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 113873 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1150.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 114873 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223616 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 115873 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223696 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 116874 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 117874 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 118874 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 40087 603 41 0 41200 0
vsize: 164964
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2545
Raw data (stat): 2545 (minisat+) R 2544 20937 20936 0 -1 0 41743 0 0 0 119874 143 0 0 25 0 1 0 488904865 168923136 40087 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 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): 1.00 0.99 0.91 1/54 2545
Raw data (stat): 2545 (minisat+) Z 2544 20937 20936 0 -1 12 41746 0 0 0 119874 150 0 0 25 0 1 0 488904865 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.26
CPU user time (s): 1198.75
CPU system time (s): 1.50877
CPU usage (%): 100.011
Max. virtual memory (Kb): 164964
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####