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/frb35-17-opb/normalized-frb35-17-2.opb
MD5SUM	409f1cf0658f035df65cb61f3e4f598e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27847
Number of constraints which are clauses	27847
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 6364

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 04:36:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4832 boxname=wulflinc18 idbench=320 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  409f1cf0658f035df65cb61f3e4f598e  /oldhome/oroussel/tmp/wulflinc18/normalized-frb35-17-2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc18/normalized-frb35-17-2.opb /oldhome/oroussel/tmp/wulflinc18/normalized-frb35-17-2.opb
IDLAUNCH: 4832
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 3
cpu MHz		: 451.177
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:        852336 kB
Buffers:         35432 kB
Cached:         110720 kB
SwapCached:        320 kB
Active:          57328 kB
Inactive:        92036 kB
HighTotal:      131008 kB
HighFree:        16352 kB
LowTotal:       903652 kB
LowFree:        835984 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27484 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:56:40 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4832 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27847 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27847    55694 |    9282       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   84628   188638 |   28209       0        0     nan |  0.000 % |
c |       100 |   84444   188223 |   31029      96      452     4.7 |  0.290 % |
c |       251 |   84001   187212 |   34132     220     1258     5.7 |  0.967 % |
c |       476 |   83068   185082 |   37546     404     2390     5.9 |  2.400 % |
c |       813 |   80860   180022 |   41300     615     4114     6.7 |  5.865 % |
c |      1320 |   77698   172767 |   45430     987     8355     8.5 | 10.886 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1559 |   74530   165517 |   24843    1075     9021     8.4 | 10.886 % |
c |      1659 |   73103   162237 |   27327    1148     9606     8.4 | 18.545 % |
c |      1809 |   71040   157490 |   30060    1246    10152     8.1 | 21.861 % |
c |      2034 |   68158   150827 |   33066    1399    11739     8.4 | 26.524 % |
c |      2371 |   65545   144751 |   36372    1621    13830     8.5 | 30.960 % |
c |      2878 |   61881   136246 |   40009    1929    17565     9.1 | 37.023 % |
c |      3637 |   55463   121143 |   44010    2295    22189     9.7 | 48.187 % |
c |      4776 |   50023   108445 |   48411    2916    28881     9.9 | 57.633 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6482 |   43321    92667 |   14440    3573    39241    11.0 | 57.633 % |
c |      6583 |   43111    92177 |   15884    3644    39638    10.9 | 69.860 % |
c |      6733 |   42532    90835 |   17472    3710    40223    10.8 | 70.836 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6895 |   42532    90878 |   14177    3827    42272    11.0 | 70.836 % |
c |      6996 |   42193    90081 |   15594    3895    43600    11.2 | 71.626 % |
c |      7146 |   41319    88026 |   17154    3795    44159    11.6 | 73.189 % |
c |      7372 |   40767    86731 |   18869    3861    45816    11.9 | 74.207 % |
c |      7710 |   40460    86007 |   20756    4122    48753    11.8 | 74.768 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8153 |   39658    84107 |   13219    4387    54130    12.3 | 74.768 % |
c |      8253 |   39583    83926 |   14540    4462    55589    12.5 | 76.292 % |
c |      8403 |   39495    83720 |   15994    4570    57315    12.5 | 76.441 % |
c |      8628 |   39094    82780 |   17594    4707    61853    13.1 | 77.145 % |
c |      8966 |   39094    82780 |   19353    5045    81072    16.1 | 77.145 % |
c |      9472 |   39094    82780 |   21289    5551   118559    21.4 | 77.145 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9628 |   39087    82783 |   13029    5694   122256    21.5 | 77.145 % |
c |      9732 |   39083    82774 |   14331    5797   124470    21.5 | 77.208 % |
c |      9882 |   38783    82066 |   15765    5776   124873    21.6 | 77.752 % |
c |     10107 |   38672    81804 |   17341    5939   129404    21.8 | 77.962 % |
c |     10445 |   37790    79744 |   19075    6096   139593    22.9 | 79.502 % |
c |     10951 |   37778    79716 |   20983    6591   149536    22.7 | 79.523 % |
c |     11710 |   37510    79087 |   23081    7250   187948    25.9 | 80.005 % |
c |     12849 |   37510    79087 |   25389    8389   258784    30.8 | 80.005 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13574 |   37370    78732 |   12456    8920   275430    30.9 | 80.005 % |
c |     13674 |   37179    78285 |   13701    8910   277405    31.1 | 80.582 % |
c |     13824 |   36942    77728 |   15071    9029   281743    31.2 | 81.013 % |
c |     14049 |   36942    77728 |   16578    9254   292618    31.6 | 81.013 % |
c |     14386 |   36942    77728 |   18236    9591   305256    31.8 | 81.013 % |
c |     14892 |   36942    77728 |   20060   10097   331111    32.8 | 81.013 % |
c |     15652 |   36908    77648 |   22066   10820   377201    34.9 | 81.075 % |
c |     16791 |   36884    77592 |   24273   11937   419789    35.2 | 81.116 % |
c |     18500 |   36458    76606 |   26700   13555   541917    40.0 | 81.835 % |
c |     21062 |   36328    76300 |   29370   15989   717134    44.9 | 82.076 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23326 |   36235    76090 |   12078   18118   912263    50.4 | 82.076 % |
c |     23426 |   36213    76038 |   13285   18214   915958    50.3 | 82.397 % |
c |     23576 |   36213    76038 |   14614   18364   921187    50.2 | 82.397 % |
c |     23801 |   36213    76038 |   16075   18589   937589    50.4 | 82.397 % |
c |     24138 |   36213    76038 |   17683   18926   954445    50.4 | 82.397 % |
c |     24644 |   35989    75504 |   19451   19057   966198    50.7 | 82.832 % |
c |     25404 |   35724    74885 |   21396   19667   999821    50.8 | 83.302 % |
c |     26543 |   35724    74885 |   23536   20806  1067168    51.3 | 83.302 % |
c |     28253 |   35718    74871 |   25890   22514  1134216    50.4 | 83.312 % |
c |     30816 |   35566    74522 |   28479   25057  1276055    50.9 | 83.573 % |
c |     34660 |   35566    74522 |   31327   28901  1538588    53.2 | 83.573 % |
c |     40428 |   35479    74320 |   34459   34597  2024073    58.5 | 83.721 % |
c |     49077 |   35463    74283 |   37905   43243  2652281    61.3 | 83.747 % |
c |     62051 |   35447    74246 |   41696   17869   834446    46.7 | 83.772 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68739 |   35322    73938 |   11774   24553  1305275    53.2 | 83.772 % |
c |     68839 |   35322    73938 |   12951   24653  1312835    53.3 | 83.973 % |
c |     68990 |   35322    73938 |   14246   24804  1322597    53.3 | 83.973 % |
c |     69216 |   35322    73938 |   15671   25030  1334526    53.3 | 83.973 % |
c |     69553 |   35103    73419 |   17238   25345  1356708    53.5 | 84.397 % |
c |     70059 |   35103    73419 |   18962   25851  1380829    53.4 | 84.397 % |
c |     70819 |   35103    73419 |   20858   26611  1423778    53.5 | 84.397 % |
c |     71958 |   35103    73419 |   22944   27750  1495152    53.9 | 84.397 % |
c |     73666 |   35022    73227 |   25238   29454  1575645    53.5 | 84.556 % |
c |     76228 |   34931    73015 |   27762   31979  1743428    54.5 | 84.714 % |
c |     80072 |   34931    73015 |   30538   35823  1896931    53.0 | 84.714 % |
c |     85838 |   34931    73015 |   33592   41589  2211192    53.2 | 84.714 % |
c |     94487 |   34931    73015 |   36951   50238  2609302    51.9 | 84.714 % |
c |    107461 |   34917    72982 |   40647   25744  1008187    39.2 | 84.740 % |
c |    126922 |   34855    72831 |   44711   45195  2030066    44.9 | 84.878 % |
c |    156114 |   34855    72831 |   49182   29328  1001207    34.1 | 84.878 % |
c |    199903 |   34821    72751 |   54101   26896   953722    35.5 | 84.939 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    263484 |   34859    72844 |   11619   40799  1765560    43.3 | 84.939 % |
c |    263586 |   34859    72844 |   12780   20502   690290    33.7 | 84.898 % |
c |    263736 |   34859    72844 |   14058   20652   695577    33.7 | 84.898 % |
c |    263961 |   34859    72844 |   15464   20877   703048    33.7 | 84.898 % |
c |    264298 |   34859    72844 |   17011   21214   716417    33.8 | 84.898 % |
c |    264805 |   34859    72844 |   18712   21721   737150    33.9 | 84.898 % |
c |    265564 |   34849    72821 |   20583   22478   769955    34.3 | 84.913 % |
c |    266703 |   34849    72821 |   22642   23617   808362    34.2 | 84.913 % |
c |    268412 |   34849    72821 |   24906   25326   859361    33.9 | 84.913 % |
c |    270974 |   34849    72821 |   27396   27888   944617    33.9 | 84.913 % |
c |    274818 |   34849    72821 |   30136   31732  1052381    33.2 | 84.913 % |
c |    280584 |   34843    72807 |   33150   37497  1280986    34.2 | 84.923 % |
c |    289233 |   34843    72807 |   36465   46146  1695653    36.7 | 84.923 % |
c |    302208 |   34827    72770 |   40111   23547   710922    30.2 | 84.949 % |
c |    321669 |   34803    72713 |   44123   43004  1471405    34.2 | 84.995 % |
c |    350861 |   34803    72713 |   48535   27777   902333    32.5 | 84.995 % |
c |    394651 |   34631    72306 |   53388   24199   745111    30.8 | 85.326 % |
c |    460335 |   34615    72269 |   58727   37021  1921413    51.9 | 85.352 % |
c |    558861 |   34484    71966 |   64600   21205   569160    26.8 | 85.561 % |
#### 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.90 0.92 0.90 2/55 30181
Raw data (stat): 30181 (runsolver) R 30180 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481753986 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.92 0.93 0.90 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 2419 0 0 0 992 6 0 0 25 0 1 0 481753986 12259328 2390 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2390 603 41 0 2952 0
vsize: 11972
[startup+20.002 s]
Raw data (loadavg): 0.93 0.93 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 2419 0 0 0 1991 7 0 0 25 0 1 0 481753986 12259328 2390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2390 603 41 0 2952 0
vsize: 11972
[startup+30.0025 s]
Raw data (loadavg): 0.94 0.93 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 2864 0 0 0 2989 9 0 0 25 0 1 0 481753986 14135296 2835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3451 2835 603 41 0 3410 0
vsize: 13804
[startup+40.0024 s]
Raw data (loadavg): 0.95 0.93 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 3447 0 0 0 3987 12 0 0 25 0 1 0 481753986 16523264 3418 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4034 3418 603 41 0 3993 0
vsize: 16136
[startup+50.0067 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 3918 0 0 0 4985 14 0 0 25 0 1 0 481753986 18395136 3889 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4491 3889 603 41 0 4450 0
vsize: 17964
[startup+60.0073 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 4426 0 0 0 5982 16 0 0 25 0 1 0 481753986 20533248 4397 4294967295 134512640 134672761 3221224560 3221223744 134558909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4397 603 41 0 4972 0
vsize: 20052
[startup+70.0072 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 4863 0 0 0 6981 18 0 0 25 0 1 0 481753986 22380544 4834 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5464 4834 603 41 0 5423 0
vsize: 21856
[startup+80.0085 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 5233 0 0 0 7979 20 0 0 25 0 1 0 481753986 23969792 5204 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5852 5204 603 41 0 5811 0
vsize: 23408
[startup+90.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 5614 0 0 0 8977 22 0 0 25 0 1 0 481753986 25423872 5585 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6207 5585 603 41 0 6166 0
vsize: 24828
[startup+100.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 5923 0 0 0 9976 23 0 0 25 0 1 0 481753986 26755072 5894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6532 5894 603 41 0 6491 0
vsize: 26128
[startup+110.01 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6173 0 0 0 10976 24 0 0 25 0 1 0 481753986 27676672 6144 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6757 6144 603 41 0 6716 0
vsize: 27028
[startup+120.011 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 11976 24 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+130.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 12976 24 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+140.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 13976 24 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+150.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 14976 25 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+160.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 15975 25 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+170.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 16975 25 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+180.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 17975 25 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223664 134560523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+190.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 18975 25 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+200.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 19975 26 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+210.016 s]
Raw data (loadavg): 1.07 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 20975 26 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+220.016 s]
Raw data (loadavg): 1.06 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 21975 26 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+230.017 s]
Raw data (loadavg): 1.05 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 22974 27 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+240.017 s]
Raw data (loadavg): 1.04 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6193 0 0 0 23974 27 0 0 25 0 1 0 481753986 27836416 6164 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6164 603 41 0 6755 0
vsize: 27184
[startup+250.018 s]
Raw data (loadavg): 1.04 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6197 0 0 0 24974 28 0 0 25 0 1 0 481753986 27836416 6168 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6168 603 41 0 6755 0
vsize: 27184
[startup+260.019 s]
Raw data (loadavg): 1.03 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 25974 28 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+270.019 s]
Raw data (loadavg): 1.03 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 26974 28 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+280.018 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 27974 28 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+290.023 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 28974 29 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+300.024 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 30183
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 29974 29 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+310.025 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 30973 29 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+320.024 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 31973 30 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+330.025 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 32973 30 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+340.025 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 33973 30 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+350.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6202 0 0 0 34973 31 0 0 25 0 1 0 481753986 27836416 6173 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6796 6173 603 41 0 6755 0
vsize: 27184
[startup+360.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6206 0 0 0 35973 31 0 0 25 0 1 0 481753986 28098560 6177 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6860 6177 603 41 0 6819 0
vsize: 27440
[startup+370.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6206 0 0 0 36972 31 0 0 25 0 1 0 481753986 28098560 6177 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6860 6177 603 41 0 6819 0
vsize: 27440
[startup+380.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6206 0 0 0 37972 32 0 0 25 0 1 0 481753986 28098560 6177 4294967295 134512640 134672761 3221224560 3221223728 134561086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6860 6177 603 41 0 6819 0
vsize: 27440
[startup+390.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6206 0 0 0 38972 32 0 0 25 0 1 0 481753986 28098560 6177 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6860 6177 603 41 0 6819 0
vsize: 27440
[startup+400.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6206 0 0 0 39972 32 0 0 25 0 1 0 481753986 28098560 6177 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6860 6177 603 41 0 6819 0
vsize: 27440
[startup+410.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6213 0 0 0 40972 33 0 0 25 0 1 0 481753986 28241920 6184 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6895 6184 603 41 0 6854 0
vsize: 27580
[startup+420.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6213 0 0 0 41972 33 0 0 25 0 1 0 481753986 28241920 6184 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6895 6184 603 41 0 6854 0
vsize: 27580
[startup+430.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6232 0 0 0 42972 33 0 0 25 0 1 0 481753986 28241920 6203 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6895 6203 603 41 0 6854 0
vsize: 27580
[startup+440.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6234 0 0 0 43973 33 0 0 25 0 1 0 481753986 28241920 6205 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6895 6205 603 41 0 6854 0
vsize: 27580
[startup+450.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6234 0 0 0 44973 33 0 0 25 0 1 0 481753986 28241920 6205 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6895 6205 603 41 0 6854 0
vsize: 27580
[startup+460.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6337 0 0 0 45972 33 0 0 25 0 1 0 481753986 28745728 6308 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7018 6308 603 41 0 6977 0
vsize: 28072
[startup+470.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6578 0 0 0 46971 35 0 0 25 0 1 0 481753986 29675520 6549 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7245 6549 603 41 0 7204 0
vsize: 28980
[startup+480.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6661 0 0 0 47971 35 0 0 25 0 1 0 481753986 30081024 6632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7344 6632 603 41 0 7303 0
vsize: 29376
[startup+490.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6661 0 0 0 48971 35 0 0 25 0 1 0 481753986 30081024 6632 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7344 6632 603 41 0 7303 0
vsize: 29376
[startup+500.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6665 0 0 0 49972 35 0 0 25 0 1 0 481753986 30081024 6636 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7344 6636 603 41 0 7303 0
vsize: 29376
[startup+510.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6672 0 0 0 50972 35 0 0 25 0 1 0 481753986 30081024 6643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7344 6643 603 41 0 7303 0
vsize: 29376
[startup+520.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6681 0 0 0 51971 35 0 0 25 0 1 0 481753986 30191616 6652 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6652 603 41 0 7330 0
vsize: 29484
[startup+530.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6681 0 0 0 52971 35 0 0 25 0 1 0 481753986 30191616 6652 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6652 603 41 0 7330 0
vsize: 29484
[startup+540.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6681 0 0 0 53971 35 0 0 25 0 1 0 481753986 30191616 6652 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6652 603 41 0 7330 0
vsize: 29484
[startup+550.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6687 0 0 0 54972 35 0 0 25 0 1 0 481753986 30191616 6658 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6658 603 41 0 7330 0
vsize: 29484
[startup+560.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 55972 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+570.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 56972 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+580.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 57972 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223664 134555379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+590.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 58972 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+600.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30185
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 59972 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+610.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 60973 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+620.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 61973 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+630.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6692 0 0 0 62973 36 0 0 25 0 1 0 481753986 30191616 6663 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6663 603 41 0 7330 0
vsize: 29484
[startup+640.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6705 0 0 0 63973 36 0 0 25 0 1 0 481753986 30355456 6676 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6676 603 41 0 7370 0
vsize: 29644
[startup+650.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6705 0 0 0 64973 36 0 0 25 0 1 0 481753986 30355456 6676 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6676 603 41 0 7370 0
vsize: 29644
[startup+660.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 65973 36 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+670.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 66973 36 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+680.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 67973 36 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+690.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 68973 36 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+700.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 69973 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+710.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 70974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+720.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 71974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+730.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 72974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+740.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 73974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+750.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 74974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+760.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 75974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+770.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 76974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+780.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 77974 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+790.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 78975 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+800.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 79975 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+810.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 80975 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+820.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 6706 0 0 0 81975 37 0 0 25 0 1 0 481753986 30355456 6677 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6677 603 41 0 7370 0
vsize: 29644
[startup+830.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 7085 0 0 0 82973 39 0 0 25 0 1 0 481753986 31825920 7056 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7770 7056 603 41 0 7729 0
vsize: 31080
[startup+840.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 7348 0 0 0 83972 40 0 0 25 0 1 0 481753986 32890880 7319 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8030 7319 603 41 0 7989 0
vsize: 32120
[startup+850.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 7563 0 0 0 84972 41 0 0 25 0 1 0 481753986 33820672 7534 4294967295 134512640 134672761 3221224560 3221223480 1075351196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8257 7534 603 41 0 8216 0
vsize: 33028
[startup+860.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 7791 0 0 0 85971 42 0 0 25 0 1 0 481753986 34750464 7762 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8484 7762 603 41 0 8443 0
vsize: 33936
[startup+870.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 7995 0 0 0 86971 43 0 0 25 0 1 0 481753986 35553280 7966 4294967295 134512640 134672761 3221224560 3221223728 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8680 7966 603 41 0 8639 0
vsize: 34720
[startup+880.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 87971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223616 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+890.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 88971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+900.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30187
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 89971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+910.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 90971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+920.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 91971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+930.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 92971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+940.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 93971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+950.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 94971 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+960.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 95972 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223744 134559583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+970.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8006 0 0 0 96972 43 0 0 25 0 1 0 481753986 35688448 7977 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7977 603 41 0 8672 0
vsize: 34852
[startup+980.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8024 0 0 0 97972 44 0 0 25 0 1 0 481753986 35688448 7995 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7995 603 41 0 8672 0
vsize: 34852
[startup+990.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8028 0 0 0 98972 44 0 0 25 0 1 0 481753986 35688448 7999 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 7999 603 41 0 8672 0
vsize: 34852
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 99972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 100972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 101972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 102972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 103972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 104972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 105972 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 106973 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 107973 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 108973 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 109973 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 110973 44 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 111973 45 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 112973 45 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 113973 45 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 114973 45 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8030 0 0 0 115973 45 0 0 25 0 1 0 481753986 35688448 8001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8713 8001 603 41 0 8672 0
vsize: 34852
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8039 0 0 0 116973 45 0 0 25 0 1 0 481753986 35880960 8010 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8760 8010 603 41 0 8719 0
vsize: 35040
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8040 0 0 0 117973 45 0 0 25 0 1 0 481753986 35880960 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8760 8011 603 41 0 8719 0
vsize: 35040
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8040 0 0 0 118973 45 0 0 25 0 1 0 481753986 35880960 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8760 8011 603 41 0 8719 0
vsize: 35040
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 30189
Raw data (stat): 30181 (minisat+) R 30180 20024 20023 0 -1 0 8064 0 0 0 119973 45 0 0 25 0 1 0 481753986 35880960 8035 4294967295 134512640 134672761 3221224560 3221223744 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8760 8035 603 41 0 8719 0
vsize: 35040
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.97 0.91 1/55 30189
Raw data (stat): 30181 (minisat+) Z 30180 20024 20023 0 -1 12 8067 0 0 0 119974 47 0 0 25 0 1 0 481753986 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.09
CPU time (s): 1200.22
CPU user time (s): 1199.74
CPU system time (s): 0.473927
CPU usage (%): 100.011
Max. virtual memory (Kb): 35040
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####