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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-3.opb
MD5SUM	063fe125a766c5e46d0ecbf211fd8049
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	450
Total number of constraints	17809
Number of constraints which are clauses	17809
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5609

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 00:49:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4076 boxname=wulflinc5 idbench=316 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  063fe125a766c5e46d0ecbf211fd8049  /oldhome/oroussel/tmp/wulflinc5/normalized-frb30-15-3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-frb30-15-3.opb /oldhome/oroussel/tmp/wulflinc5/normalized-frb30-15-3.opb
IDLAUNCH: 4076
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        899320 kB
Buffers:         34068 kB
Cached:          79668 kB
SwapCached:       2272 kB
Active:          54300 kB
Inactive:        64608 kB
HighTotal:      131008 kB
HighFree:        47404 kB
LowTotal:       903652 kB
LowFree:        851916 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10944 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:09:35 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4076 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17809 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17809    35618 |    5342       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   17809    35618 |    7123       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.615906 s)
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   34945    75925 |   10483       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11801          
c   -- var.elim.:  2000/11801          
c   -- var.elim.:  3000/11801          
c   -- var.elim.:  4000/11801          
c   -- var.elim.:  5000/11801          
c   -- var.elim.:  6000/11801          
c   -- var.elim.:  7000/11801          
c   -- var.elim.:  8000/11801          
c   -- var.elim.:  9000/11801          
c   -- var.elim.:  10000/11801          
c   -- var.elim.:  11000/11801          
c   -- var.elim.:  11801/11801          
c   -- var.elim.:  1000/6021          
c   -- var.elim.:  2000/6021          
c   -- var.elim.:  3000/6021          
c   -- var.elim.:  4000/6021          
c   -- var.elim.:  5000/6021          
c   -- var.elim.:  6000/6021          
c   -- var.elim.:  6021/6021          
c   -- var.elim.:  101/101          
c   -- subsuming                       
c   -- var.elim.:  1000/2300          
c   -- var.elim.:  2000/2300          
c   -- var.elim.:  2300/2300          
c   -- var.elim.:  260/260          
c |         0 |   22798    70566 |      --       0       --      -- |     --   | -12147/-5358
c |         0 |   22798    70566 |    9119       0        0     nan |  0.000 % |
c |       100 |   22798    70566 |   10031     100    16034   160.3 | 52.479 % |
c |       250 |   22798    70566 |   11034     250    26991   108.0 | 52.478 % |
c |       476 |   22798    70566 |   12137     476    55457   116.5 | 52.478 % |
c |       813 |   22798    70566 |   13351     813    96223   118.4 | 52.478 % |
c |      1321 |   22710    69875 |   14629    1314   166546   126.7 | 53.179 % |
c |      2081 |   22710    69875 |   16092    2074   287570   138.7 | 53.180 % |
c |      3220 |   22638    69331 |   17646    3199   463439   144.9 | 53.714 % |
c |      4928 |   22421    67670 |   19224    4872   744941   152.9 | 55.381 % |
c |      7490 |   22361    67220 |   21090    7424  1342646   180.9 | 55.882 % |
c ==============================================================================
c (current CPU-time: 19.645 s)
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8277 |   24229    72294 |    7268    8203  1507513   183.8 | 55.882 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4385          
c   -- var.elim.:  2000/4385          
c   -- var.elim.:  3000/4385          
c   -- var.elim.:  4000/4385          
c   -- var.elim.:  4385/4385          
c   -- var.elim.:  1000/1481          
c   -- var.elim.:  1481/1481          
c |      8277 |   22377    70042 |      --    8203       --      -- |     --   | -1852/-2251
c |      8277 |   22377    70042 |    8950    8203  1507513   183.8 | 55.882 % |
c |      8377 |   22359    69907 |    9837    8302  1519986   183.1 | 61.647 % |
c |      8528 |   22359    69907 |   10821    8453  1546505   183.0 | 61.648 % |
c |      8754 |   22359    69907 |   11903    8679  1586174   182.8 | 61.648 % |
c |      9093 |   22359    69907 |   13094    9018  1659203   184.0 | 61.648 % |
c |      9600 |   22333    69717 |   14387    9500  1755017   184.7 | 61.823 % |
c |     10360 |   22333    69717 |   15825   10260  1914776   186.6 | 61.822 % |
c |     11500 |   22281    69290 |   17367   11389  2144818   188.3 | 62.201 % |
c |     13208 |   22213    68723 |   19046   13083  2471636   188.9 | 62.697 % |
c |     15770 |   22049    67382 |   20796   15592  2986181   191.5 | 63.893 % |
c |     19614 |   21982    66844 |   22806   19377  3871116   199.8 | 64.359 % |
c ==============================================================================
c (current CPU-time: 51.7431 s)
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22170 |   22389    66850 |    6716   21862  4372729   200.0 | 64.359 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2901          
c   -- var.elim.:  2000/2901          
c   -- var.elim.:  2901/2901          
c   -- var.elim.:  651/651          
c |     22170 |   21739    63263 |      --   21862       --      -- |     --   | -632/-1322
c |     22170 |   21739    63263 |    8695   18148  2669782   147.1 | 64.359 % |
c |     22271 |   21739    63263 |    9565   12200  1691363   138.6 | 66.344 % |
c |     22422 |   21719    63120 |   10511   12350  1718128   139.1 | 66.489 % |
c |     22647 |   21699    62988 |   11552   12569  1758047   139.9 | 66.633 % |
c |     22984 |   21673    62791 |   12692   12905  1812213   140.4 | 66.792 % |
c |     23491 |   21673    62791 |   13961   13412  1910997   142.5 | 66.793 % |
c |     24250 |   21651    62637 |   15342   14161  2057622   145.3 | 66.938 % |
c |     25389 |   21627    62469 |   16857   15297  2257038   147.5 | 67.112 % |
c |     27097 |   21607    62314 |   18526   16988  2592653   152.6 | 67.256 % |
c |     29659 |   21587    62168 |   20360   19542  3142554   160.8 | 67.387 % |
c |     33506 |   21514    61599 |   22320   23361  3980713   170.4 | 67.908 % |
c |     39272 |   21374    60535 |   24393   16789  2757376   164.2 | 68.894 % |
c |     47922 |   21209    59402 |   26625   25404  4498877   177.1 | 70.068 % |
c ==============================================================================
c (current CPU-time: 124.531 s)
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     54274 |   22855    63552 |    6856   31748  5902818   185.9 | 70.068 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3658          
c   -- var.elim.:  2000/3658          
c   -- var.elim.:  3000/3658          
c   -- var.elim.:  3658/3658          
c   -- var.elim.:  1000/1071          
c   -- var.elim.:  1071/1071          
c   -- var.elim.:  32/32          
c |     54274 |   21234    61705 |      --   31748       --      -- |     --   | -1611/-1826
c |     54274 |   21234    61705 |    8493   31748  5902818   185.9 | 70.068 % |
c |     54374 |   21234    61705 |    9342   11109  1618100   145.7 | 72.495 % |
c |     54524 |   21234    61705 |   10277   11259  1641226   145.8 | 72.495 % |
c |     54750 |   21234    61705 |   11304   11485  1680481   146.3 | 72.495 % |
c |     55088 |   21234    61705 |   12435   11823  1751581   148.2 | 72.495 % |
c |     55594 |   21234    61705 |   13679   12329  1879867   152.5 | 72.495 % |
c |     56353 |   21181    61322 |   15009   13082  1985890   151.8 | 72.826 % |
c |     57492 |   21181    61322 |   16510   14221  2283743   160.6 | 72.827 % |
c |     59200 |   21181    61322 |   18161   15929  2607693   163.7 | 72.827 % |
c |     61762 |   21181    61322 |   19977   18491  3145684   170.1 | 72.827 % |
c |     65609 |   21073    60441 |   21863   22316  3992009   178.9 | 73.531 % |
c |     71375 |   20992    59890 |   23957   16278  2606210   160.1 | 74.010 % |
c |     80025 |   20879    59020 |   26210   24891  4428226   177.9 | 74.714 % |
c |     92999 |   20648    57296 |   28512   22465  3678224   163.7 | 76.204 % |
c |    112460 |   20361    55095 |   30928   23502  3713461   158.0 | 78.065 % |
c |    141652 |   20146    53439 |   33661   31381  5425835   172.9 | 79.434 % |
c |    185442 |   20067    52827 |   36882   26810  4605000   171.8 | 79.939 % |
c ==============================================================================
c (current CPU-time: 577.473 s)
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    238074 |   19895    51413 |    5968   25730  4135969   160.7 | 79.939 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1435          
c   -- var.elim.:  1435/1435          
c   -- var.elim.:  297/297          
c   -- var.elim.:  564/564          
c   -- var.elim.:  169/169          
c |    238074 |   19828    50356 |      --   25730       --      -- |     --   | -53/-905
c |    238074 |   19828    50356 |    7931   14356  1022166    71.2 | 79.939 % |
c |    238176 |   19828    50356 |    8724    9673   663621    68.6 | 81.497 % |
c |    238326 |   19828    50356 |    9596    9823   683756    69.6 | 81.497 % |
c |    238551 |   19828    50356 |   10556   10048   713558    71.0 | 81.497 % |
c |    238888 |   19828    50356 |   11612   10385   760736    73.3 | 81.497 % |
c |    239394 |   19828    50356 |   12773   10891   850832    78.1 | 81.497 % |
c |    240154 |   19828    50356 |   14050   11651   946253    81.2 | 81.497 % |
c |    241293 |   19828    50356 |   15455   12790  1142867    89.4 | 81.497 % |
c |    243001 |   19828    50356 |   17001   14498  1392357    96.0 | 81.497 % |
c |    245563 |   19826    50334 |   18699   17056  1820001   106.7 | 81.510 % |
c |    249407 |   19826    50334 |   20569   20900  2411049   115.4 | 81.510 % |
c |    255176 |   19826    50334 |   22626   26669  3317426   124.4 | 81.511 % |
c |    263825 |   19794    50108 |   24848   21821  2917104   133.7 | 81.697 % |
c ==============================================================================
c (current CPU-time: 647.312 s)
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    274502 |   20280    50946 |    6083   17101  2200333   128.7 | 81.697 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1376          
c   -- var.elim.:  1376/1376          
c   -- var.elim.:  465/465          
c   -- var.elim.:  1/1          
c |    274502 |   19741    49989 |      --   17101       --      -- |     --   | -538/-954
c |    274502 |   19741    49989 |    7896   12549  1095233    87.3 | 81.697 % |
c |    274602 |   19741    49989 |    8686   12649  1107591    87.6 | 82.917 % |
c |    274753 |   19741    49989 |    9554   12800  1124815    87.9 | 82.917 % |
c |    274978 |   19741    49989 |   10510   13025  1151086    88.4 | 82.916 % |
c |    275315 |   19741    49989 |   11561   13362  1191903    89.2 | 82.917 % |
c |    275821 |   19741    49989 |   12717   13868  1260468    90.9 | 82.916 % |
c |    276581 |   19741    49989 |   13988   14628  1361264    93.1 | 82.916 % |
c |    277720 |   19717    49823 |   15369   15763  1522777    96.6 | 83.044 % |
c |    279428 |   19692    49658 |   16884   17469  1832480   104.9 | 83.198 % |
c |    281991 |   19692    49658 |   18573   20032  2205567   110.1 | 83.197 % |
c |    285835 |   19652    49375 |   20388   23861  2715005   113.8 | 83.453 % |
c |    291601 |   19652    49375 |   22427   18455  2220465   120.3 | 83.453 % |
c |    300251 |   19590    48899 |   24592   27058  3479653   128.6 | 83.810 % |
c |    313225 |   19541    48565 |   26984   24510  3060637   124.9 | 84.117 % |
c |    332686 |   19363    47334 |   29412   26204  3203002   122.2 | 85.202 % |
c |    361881 |   19258    46575 |   32178   35512  3754970   105.7 | 85.827 % |
c |    405670 |   19133    45757 |   35166   33760  3674126   108.8 | 86.568 % |
c |    471354 |   19050    45242 |   38515   19558  1869360    95.6 | 87.066 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C450 -C449 -C448 -C447 C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 28114
Raw data (stat): 28114 (runsolver) R 28113 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422177925 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 2468 0 0 0 989 9 0 0 25 0 1 0 422177925 12181504 2391 4294967295 134512640 134672761 3221224560 3221223104 134621083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2974 2391 603 41 0 2933 0
vsize: 11896
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 4356 0 0 0 1984 14 0 0 25 0 1 0 422177925 18464768 3923 4294967295 134512640 134672761 3221224560 3221223104 134621041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4508 3923 603 41 0 4467 0
vsize: 18032
[startup+30.0024 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 5329 0 0 0 2979 19 0 0 25 0 1 0 422177925 21962752 4826 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4826 603 41 0 5321 0
vsize: 21448
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 6343 0 0 0 3977 21 0 0 25 0 1 0 422177925 26185728 5840 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6393 5840 603 41 0 6352 0
vsize: 25572
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 7206 0 0 0 4974 24 0 0 25 0 1 0 422177925 29581312 6703 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7222 6703 603 41 0 7181 0
vsize: 28888
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 7846 0 0 0 5970 28 0 0 25 0 1 0 422177925 31522816 7171 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7696 7171 603 41 0 7655 0
vsize: 30784
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 7846 0 0 0 6970 28 0 0 25 0 1 0 422177925 31522816 7171 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7696 7171 603 41 0 7655 0
vsize: 30784
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 7850 0 0 0 7970 28 0 0 25 0 1 0 422177925 31522816 7175 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7696 7175 603 41 0 7655 0
vsize: 30784
[startup+90.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 8393 0 0 0 8969 30 0 0 25 0 1 0 422177925 33677312 7717 4294967295 134512640 134672761 3221224560 3221223600 134614325 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8222 7717 603 41 0 8181 0
vsize: 32888
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 8393 0 0 0 9969 30 0 0 25 0 1 0 422177925 33677312 7717 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8222 7717 603 41 0 8181 0
vsize: 32888
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 8393 0 0 0 10969 30 0 0 25 0 1 0 422177925 33677312 7717 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8222 7717 603 41 0 8181 0
vsize: 32888
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 8763 0 0 0 11969 31 0 0 25 0 1 0 422177925 35241984 8087 4294967295 134512640 134672761 3221224560 3221223744 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8604 8087 603 41 0 8563 0
vsize: 34416
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 12963 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 13963 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 14963 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 15964 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 16964 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 17964 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9817 0 0 0 18964 35 0 0 25 0 1 0 422177925 39460864 8961 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8961 603 41 0 9593 0
vsize: 38536
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9818 0 0 0 19964 35 0 0 25 0 1 0 422177925 39460864 8962 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8962 603 41 0 9593 0
vsize: 38536
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9850 0 0 0 20964 36 0 0 25 0 1 0 422177925 39587840 8994 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9665 8994 603 41 0 9624 0
vsize: 38660
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9850 0 0 0 21965 36 0 0 25 0 1 0 422177925 39587840 8994 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9665 8994 603 41 0 9624 0
vsize: 38660
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9850 0 0 0 22965 36 0 0 25 0 1 0 422177925 39587840 8994 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9665 8994 603 41 0 9624 0
vsize: 38660
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 9850 0 0 0 23965 36 0 0 25 0 1 0 422177925 39587840 8994 4294967295 134512640 134672761 3221224560 3221223664 134603769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9665 8994 603 41 0 9624 0
vsize: 38660
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10069 0 0 0 24964 36 0 0 25 0 1 0 422177925 40628224 9213 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9919 9213 603 41 0 9878 0
vsize: 39676
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10509 0 0 0 25963 38 0 0 25 0 1 0 422177925 42385408 9648 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9648 603 41 0 10307 0
vsize: 41392
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10509 0 0 0 26963 38 0 0 25 0 1 0 422177925 42385408 9648 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9648 603 41 0 10307 0
vsize: 41392
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10509 0 0 0 27963 38 0 0 25 0 1 0 422177925 42385408 9648 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9648 603 41 0 10307 0
vsize: 41392
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10509 0 0 0 28964 38 0 0 25 0 1 0 422177925 42385408 9648 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9648 603 41 0 10307 0
vsize: 41392
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10509 0 0 0 29964 38 0 0 25 0 1 0 422177925 42385408 9648 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9648 603 41 0 10307 0
vsize: 41392
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10629 0 0 0 30964 38 0 0 25 0 1 0 422177925 42840064 9761 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10459 9761 603 41 0 10418 0
vsize: 41836
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10629 0 0 0 31964 38 0 0 25 0 1 0 422177925 42840064 9761 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10459 9761 603 41 0 10418 0
vsize: 41836
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10629 0 0 0 32964 38 0 0 25 0 1 0 422177925 42840064 9761 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10459 9761 603 41 0 10418 0
vsize: 41836
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10629 0 0 0 33964 38 0 0 25 0 1 0 422177925 42840064 9761 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10459 9761 603 41 0 10418 0
vsize: 41836
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10629 0 0 0 34964 38 0 0 25 0 1 0 422177925 42840064 9761 4294967295 134512640 134672761 3221224560 3221223600 134613761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10459 9761 603 41 0 10418 0
vsize: 41836
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 10787 0 0 0 35964 39 0 0 25 0 1 0 422177925 43495424 9919 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10619 9919 603 41 0 10578 0
vsize: 42476
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11316 0 0 0 36963 40 0 0 25 0 1 0 422177925 45608960 10438 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11135 10438 603 41 0 11094 0
vsize: 44540
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11316 0 0 0 37963 40 0 0 25 0 1 0 422177925 45608960 10438 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11135 10438 603 41 0 11094 0
vsize: 44540
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11316 0 0 0 38963 40 0 0 25 0 1 0 422177925 45608960 10438 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11135 10438 603 41 0 11094 0
vsize: 44540
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11317 0 0 0 39964 40 0 0 25 0 1 0 422177925 45608960 10439 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11135 10439 603 41 0 11094 0
vsize: 44540
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11317 0 0 0 40964 40 0 0 25 0 1 0 422177925 45608960 10439 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11135 10439 603 41 0 11094 0
vsize: 44540
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11317 0 0 0 41964 40 0 0 25 0 1 0 422177925 45608960 10439 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11135 10439 603 41 0 11094 0
vsize: 44540
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11357 0 0 0 42964 40 0 0 25 0 1 0 422177925 45600768 10437 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11133 10437 603 41 0 11092 0
vsize: 44532
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11357 0 0 0 43964 40 0 0 25 0 1 0 422177925 45600768 10437 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11133 10437 603 41 0 11092 0
vsize: 44532
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11357 0 0 0 44964 40 0 0 25 0 1 0 422177925 45600768 10437 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11133 10437 603 41 0 11092 0
vsize: 44532
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11357 0 0 0 45965 40 0 0 25 0 1 0 422177925 45600768 10437 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11133 10437 603 41 0 11092 0
vsize: 44532
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11357 0 0 0 46965 40 0 0 25 0 1 0 422177925 45600768 10437 4294967295 134512640 134672761 3221224560 3221223600 134612873 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11133 10437 603 41 0 11092 0
vsize: 44532
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 11357 0 0 0 47965 40 0 0 25 0 1 0 422177925 45600768 10437 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11133 10437 603 41 0 11092 0
vsize: 44532
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 48963 42 0 0 25 0 1 0 422177925 48586752 11147 4294967295 134512640 134672761 3221224560 3221223424 134645421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11862 11147 603 41 0 11821 0
vsize: 47448
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 49963 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 50964 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 51964 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 52964 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 53964 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 54964 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12067 0 0 0 55965 42 0 0 25 0 1 0 422177925 48324608 11104 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11104 603 41 0 11757 0
vsize: 47192
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12110 0 0 0 56965 42 0 0 25 0 1 0 422177925 48320512 11103 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11797 11103 603 41 0 11756 0
vsize: 47188
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12649 0 0 0 57962 45 0 0 25 0 1 0 422177925 49623040 11350 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12115 11350 603 41 0 12074 0
vsize: 48460
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12649 0 0 0 58961 45 0 0 25 0 1 0 422177925 49623040 11350 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11350 603 41 0 12074 0
vsize: 48460
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12649 0 0 0 59962 45 0 0 25 0 1 0 422177925 49623040 11350 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11350 603 41 0 12074 0
vsize: 48460
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12649 0 0 0 60962 45 0 0 25 0 1 0 422177925 49623040 11350 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11350 603 41 0 12074 0
vsize: 48460
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12650 0 0 0 61962 45 0 0 25 0 1 0 422177925 49623040 11351 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11351 603 41 0 12074 0
vsize: 48460
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28114
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12650 0 0 0 62962 45 0 0 25 0 1 0 422177925 49623040 11351 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11351 603 41 0 12074 0
vsize: 48460
[startup+640.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 12650 0 0 0 63961 46 0 0 25 0 1 0 422177925 49623040 11351 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11351 603 41 0 12074 0
vsize: 48460
[startup+650.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 64957 49 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+660.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 65957 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+670.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 66956 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+680.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 67956 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+690.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 68957 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+700.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28167
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 69957 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+710.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 70957 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+720.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 71957 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+730.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 72957 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+740.024 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13115 0 0 0 73958 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+750.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 74958 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+760.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 75958 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+770.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 76958 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 77958 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 78958 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+800.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 79959 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+810.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 80959 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 81959 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13149 0 0 0 82959 50 0 0 25 0 1 0 422177925 48582656 11179 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11179 603 41 0 11820 0
vsize: 47444
[startup+840.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 83959 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+850.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 84959 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+860.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 85960 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+870.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 86960 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+880.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 87960 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+890.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 88960 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+900.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 89960 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+910.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 90961 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+920.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 91961 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+930.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 92961 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+940.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 93961 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+950.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 94961 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+960.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28169
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 95962 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+970.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 96962 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+980.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 97962 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+990.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 98962 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 99962 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 100963 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 101963 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 102963 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 103963 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 104964 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 105964 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 106964 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 107964 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 108964 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 109964 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 110965 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13150 0 0 0 111965 50 0 0 25 0 1 0 422177925 48582656 11180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11180 603 41 0 11820 0
vsize: 47444
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 112965 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 113965 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 114965 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 115966 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 116966 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 117966 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 118966 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28171
Raw data (stat): 28114 (minisat+) R 28113 24215 24214 0 -1 0 13152 0 0 0 119966 50 0 0 25 0 1 0 422177925 48582656 11182 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11182 603 41 0 11820 0
vsize: 47444
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28171
Raw data (stat): 28114 (minisat+) Z 28113 24215 24214 0 -1 12 13153 0 0 0 119966 53 0 0 25 0 1 0 422177925 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.06
CPU time (s): 1200.2
CPU user time (s): 1199.67
CPU system time (s): 0.532918
CPU usage (%): 100.011
Max. virtual memory (Kb): 48460
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####