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-4.opb
MD5SUM	615f734b8951521e89cf22f42d6d26cc
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.05084
Number of variables	450
Total number of constraints	17831
Number of constraints which are clauses	17831
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 5233

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 22:45:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3701 boxname=wulflinc13 idbench=317 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  615f734b8951521e89cf22f42d6d26cc  /oldhome/oroussel/tmp/wulflinc13/normalized-frb30-15-4.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc13/normalized-frb30-15-4.opb /oldhome/oroussel/tmp/wulflinc13/normalized-frb30-15-4.opb
IDLAUNCH: 3701
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        909224 kB
Buffers:         34408 kB
Cached:          71008 kB
SwapCached:        392 kB
Active:          53432 kB
Inactive:        55264 kB
HighTotal:      131008 kB
HighFree:        56084 kB
LowTotal:       903652 kB
LowFree:        853140 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11088 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:05:11 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3701 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17831 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 |   17831    35662 |    5943       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 883   maxlim: 22   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23854    57192 |    7951       0        0     nan |  0.000 % |
c |       100 |   23854    57192 |    8746     100     1107    11.1 |  0.309 % |
c |       250 |   23854    57192 |    9620     249     3349    13.4 |  0.377 % |
c |       475 |   23785    56955 |   10582     460     6184    13.4 |  0.906 % |
c |       812 |   23678    56586 |   11641     767    11191    14.6 |  1.887 % |
c |      1318 |   23570    56218 |   12805    1250    20016    16.0 |  2.943 % |
c |      2077 |   23498    55972 |   14085    1986    32759    16.5 |  3.623 % |
c |      3217 |   23322    55370 |   15494    3085    57228    18.6 |  5.509 % |
c |      4925 |   22670    53122 |   17043    4574   105133    23.0 | 13.132 % |
c |      7488 |   21863    50323 |   18748    6797   182886    26.9 | 24.083 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7941 |   21831    50210 |    7277    7201   199478    27.7 | 24.083 % |
c |      8041 |   21831    50210 |    8004    7301   202506    27.7 | 24.590 % |
c |      8191 |   21831    50210 |    8805    7451   209350    28.1 | 24.585 % |
c |      8416 |   21831    50210 |    9685    7676   218600    28.5 | 24.585 % |
c |      8753 |   21831    50210 |   10654    8013   232047    29.0 | 24.585 % |
c |      9259 |   21831    50210 |   11719    8519   256237    30.1 | 24.593 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9934 |   21834    50223 |    7278    9194   297761    32.4 | 24.593 % |
c |     10034 |   21834    50223 |    8005    4697   151044    32.2 | 24.649 % |
c |     10184 |   21809    50136 |    8806    4842   153482    31.7 | 25.019 % |
c |     10410 |   21809    50136 |    9687    5068   167587    33.1 | 25.019 % |
c |     10748 |   21809    50136 |   10655    5406   176315    32.6 | 25.019 % |
c |     11254 |   21682    49693 |   11721    5883   197281    33.5 | 27.129 % |
c |     12014 |   21682    49693 |   12893    6643   242491    36.5 | 27.129 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12313 |   21674    49668 |    7224    6927   259249    37.4 | 27.129 % |
c |     12413 |   21674    49668 |    7946    7027   264937    37.7 | 27.259 % |
c |     12564 |   21674    49668 |    8741    7178   267948    37.3 | 27.259 % |
c |     12789 |   21674    49668 |    9615    7403   282949    38.2 | 27.265 % |
c |     13126 |   21674    49668 |   10576    7740   297091    38.4 | 27.259 % |
c |     13632 |   21674    49668 |   11634    8246   337851    41.0 | 27.259 % |
c |     14391 |   21616    49468 |   12797    8932   375679    42.1 | 27.944 % |
c |     15530 |   21589    49375 |   14077   10025   430526    42.9 | 28.169 % |
c |     17239 |   21536    49190 |   15485   11683   489074    41.9 | 28.916 % |
c |     19802 |   21477    48985 |   17033   14205   599849    42.2 | 29.752 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20299 |   21478    48992 |    7159   14702   622530    42.3 | 29.752 % |
c |     20399 |   21478    48992 |    7874    7451   237029    31.8 | 29.797 % |
c |     20549 |   21457    48917 |    8662    7594   240839    31.7 | 30.173 % |
c |     20774 |   21457    48917 |    9528    7819   250360    32.0 | 30.181 % |
c |     21111 |   21448    48886 |   10481    8150   267247    32.8 | 30.248 % |
c |     21617 |   21448    48886 |   11529    8656   304312    35.2 | 30.248 % |
c |     22376 |   21439    48855 |   12682    9407   347992    37.0 | 30.324 % |
c |     23517 |   21410    48758 |   13950   10510   395237    37.6 | 30.708 % |
c |     25226 |   21410    48758 |   15345   12219   472685    38.7 | 30.700 % |
c |     27788 |   21389    48683 |   16880   14777   628663    42.5 | 31.081 % |
c |     31633 |   21380    48652 |   18568    9707   345278    35.6 | 31.160 % |
c |     37401 |   21380    48652 |   20425   15475   555832    35.9 | 31.160 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45935 |   21381    48657 |    7127   13391   428986    32.0 | 31.160 % |
c |     46035 |   21381    48657 |    7839    6796   191387    28.2 | 31.211 % |
c |     46185 |   21349    48547 |    8623    6941   194147    28.0 | 31.579 % |
c |     46410 |   21288    48334 |    9486    7145   198910    27.8 | 32.481 % |
c |     46748 |   21288    48334 |   10434    7483   213833    28.6 | 32.481 % |
c |     47254 |   21265    48253 |   11478    7982   228531    28.6 | 32.857 % |
c |     48013 |   21265    48253 |   12625    8741   265240    30.3 | 32.857 % |
c |     49152 |   21209    48055 |   13888    9869   296892    30.1 | 33.835 % |
c |     50861 |   21209    48055 |   15277   11578   384264    33.2 | 33.841 % |
c |     53423 |   21209    48055 |   16805   14140   475324    33.6 | 33.835 % |
c |     57271 |   21209    48055 |   18485    9140   360810    39.5 | 33.841 % |
c |     63038 |   21209    48055 |   20334   14907   747709    50.2 | 33.835 % |
c |     71687 |   21203    48035 |   22367   12968   578401    44.6 | 33.916 % |
c |     84661 |   21203    48035 |   24604   14443   559663    38.7 | 33.910 % |
c |    104122 |   21203    48035 |   27064   21197  1473396    69.5 | 33.910 % |
c |    133315 |   21157    47871 |   29771   22557   952171    42.2 | 34.742 % |
c |    177104 |   21157    47871 |   32748   18932  1293314    68.3 | 34.742 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225109 |   21158    47878 |    7052   29503  1930374    65.4 | 34.742 % |
c |    225210 |   21158    47878 |    7757    7309   307478    42.1 | 34.792 % |
c |    225360 |   21158    47878 |    8532    7459   308992    41.4 | 34.786 % |
c |    225585 |   21158    47878 |    9386    7684   316050    41.1 | 34.791 % |
c |    225922 |   21158    47878 |   10324    8021   325908    40.6 | 34.786 % |
c |    226428 |   21158    47878 |   11357    8527   334183    39.2 | 34.786 % |
c |    227187 |   21158    47878 |   12493    9286   368508    39.7 | 34.792 % |
c |    228326 |   21158    47878 |   13742   10425   420297    40.3 | 34.786 % |
c |    230034 |   21158    47878 |   15116   12133   496706    40.9 | 34.786 % |
c |    232597 |   21158    47878 |   16628   14696   604958    41.2 | 34.786 % |
c |    236444 |   21158    47878 |   18291    9806   368720    37.6 | 34.787 % |
c |    242210 |   21158    47878 |   20120   15572   503906    32.4 | 34.786 % |
c |    250859 |   21158    47878 |   22132   13824   238689    17.3 | 34.786 % |
c |    263833 |   21158    47878 |   24345   15393   258447    16.8 | 34.793 % |
c |    283296 |   21158    47878 |   26779   22362   358527    16.0 | 34.793 % |
c |    312488 |   21158    47878 |   29457   24043   486256    20.2 | 34.793 % |
c |    356278 |   21158    47878 |   32403   22191   464140    20.9 | 34.793 % |
c |    421962 |   21158    47878 |   35644   18891   340666    18.0 | 34.793 % |
c |    520488 |   21158    47878 |   39208   20791   441679    21.2 | 34.793 % |
c |    668277 |   21158    47878 |   43129   18804   351111    18.7 | 34.793 % |
c |    889960 |   21158    47878 |   47442   41351   864242    20.9 | 34.793 % |
#### 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.91 0.95 0.90 2/54 3363
Raw data (stat): 3363 (runsolver) R 3362 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421434736 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.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 1357 0 0 0 995 3 0 0 25 0 1 0 421434736 7168000 1335 4294967295 134512640 134672761 3221224560 3221223744 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1750 1335 603 41 0 1709 0
vsize: 7000
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 1573 0 0 0 1994 4 0 0 25 0 1 0 421434736 8097792 1551 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1551 603 41 0 1936 0
vsize: 7908
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 1691 0 0 0 2993 4 0 0 25 0 1 0 421434736 8495104 1669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2074 1669 603 41 0 2033 0
vsize: 8296
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 1691 0 0 0 3993 4 0 0 25 0 1 0 421434736 8495104 1669 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2074 1669 603 41 0 2033 0
vsize: 8296
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2003 0 0 0 4993 5 0 0 25 0 1 0 421434736 9830400 1981 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2400 1981 603 41 0 2359 0
vsize: 9600
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2018 0 0 0 5993 5 0 0 25 0 1 0 421434736 9830400 1996 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1996 603 41 0 2359 0
vsize: 9600
[startup+70.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2418 0 0 0 6991 7 0 0 25 0 1 0 421434736 11587584 2396 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2829 2396 603 41 0 2788 0
vsize: 11316
[startup+80.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2607 0 0 0 7990 7 0 0 25 0 1 0 421434736 12255232 2585 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2992 2585 603 41 0 2951 0
vsize: 11968
[startup+90.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2858 0 0 0 8990 8 0 0 25 0 1 0 421434736 13320192 2836 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2836 603 41 0 3211 0
vsize: 13008
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2859 0 0 0 9990 8 0 0 25 0 1 0 421434736 13320192 2837 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2837 603 41 0 3211 0
vsize: 13008
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2859 0 0 0 10990 8 0 0 25 0 1 0 421434736 13320192 2837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2837 603 41 0 3211 0
vsize: 13008
[startup+120.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2862 0 0 0 11990 8 0 0 25 0 1 0 421434736 13320192 2840 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2840 603 41 0 3211 0
vsize: 13008
[startup+130.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 2863 0 0 0 12991 8 0 0 25 0 1 0 421434736 13320192 2841 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2841 603 41 0 3211 0
vsize: 13008
[startup+140.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3156 0 0 0 13990 9 0 0 25 0 1 0 421434736 14528512 3134 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3547 3134 603 41 0 3506 0
vsize: 14188
[startup+150.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3164 0 0 0 14990 9 0 0 25 0 1 0 421434736 14528512 3142 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3547 3142 603 41 0 3506 0
vsize: 14188
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3449 0 0 0 15989 10 0 0 25 0 1 0 421434736 15790080 3427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3427 603 41 0 3814 0
vsize: 15420
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3464 0 0 0 16989 10 0 0 25 0 1 0 421434736 15790080 3442 4294967295 134512640 134672761 3221224560 3221223664 134559802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3442 603 41 0 3814 0
vsize: 15420
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3516 0 0 0 17989 10 0 0 25 0 1 0 421434736 16089088 3494 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3928 3494 603 41 0 3887 0
vsize: 15712
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3811 0 0 0 18988 12 0 0 25 0 1 0 421434736 17428480 3789 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4255 3789 603 41 0 4214 0
vsize: 17020
[startup+200.004 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3814 0 0 0 19989 12 0 0 25 0 1 0 421434736 17428480 3792 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4255 3792 603 41 0 4214 0
vsize: 17020
[startup+210.004 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3823 0 0 0 20989 12 0 0 25 0 1 0 421434736 17428480 3801 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4255 3801 603 41 0 4214 0
vsize: 17020
[startup+220.004 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3950 0 0 0 21988 12 0 0 25 0 1 0 421434736 17965056 3928 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4386 3928 603 41 0 4345 0
vsize: 17544
[startup+230.004 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3953 0 0 0 22989 12 0 0 25 0 1 0 421434736 17965056 3931 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4386 3931 603 41 0 4345 0
vsize: 17544
[startup+240.004 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 23989 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+250.005 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 24989 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+260.005 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 25989 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+270.005 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 26989 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+280.006 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 27989 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+290.006 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 28989 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+300.006 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 29990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+310.006 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 30990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+320.005 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 31990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+330.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 32990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+340.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 33990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+350.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 34990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+360.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 35990 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+370.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 36991 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+380.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 37991 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223744 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+390.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 38991 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+400.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 39991 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+410.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 40991 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+420.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 41992 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+430.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3959 0 0 0 42992 12 0 0 25 0 1 0 421434736 18100224 3937 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3937 603 41 0 4378 0
vsize: 17676
[startup+440.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3962 0 0 0 43992 13 0 0 25 0 1 0 421434736 18100224 3940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3940 603 41 0 4378 0
vsize: 17676
[startup+450.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3962 0 0 0 44992 13 0 0 25 0 1 0 421434736 18100224 3940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3940 603 41 0 4378 0
vsize: 17676
[startup+460.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3962 0 0 0 45992 13 0 0 25 0 1 0 421434736 18100224 3940 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3940 603 41 0 4378 0
vsize: 17676
[startup+470.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3962 0 0 0 46992 13 0 0 25 0 1 0 421434736 18100224 3940 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3940 603 41 0 4378 0
vsize: 17676
[startup+480.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3962 0 0 0 47993 13 0 0 25 0 1 0 421434736 18100224 3940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3940 603 41 0 4378 0
vsize: 17676
[startup+490.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3962 0 0 0 48993 13 0 0 25 0 1 0 421434736 18100224 3940 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3940 603 41 0 4378 0
vsize: 17676
[startup+500.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3964 0 0 0 49993 13 0 0 25 0 1 0 421434736 18100224 3942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3942 603 41 0 4378 0
vsize: 17676
[startup+510.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3964 0 0 0 50993 13 0 0 25 0 1 0 421434736 18100224 3942 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3942 603 41 0 4378 0
vsize: 17676
[startup+520.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3964 0 0 0 51993 13 0 0 25 0 1 0 421434736 18100224 3942 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3942 603 41 0 4378 0
vsize: 17676
[startup+530.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3964 0 0 0 52993 13 0 0 25 0 1 0 421434736 18100224 3942 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3942 603 41 0 4378 0
vsize: 17676
[startup+540.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3965 0 0 0 53994 13 0 0 25 0 1 0 421434736 18100224 3943 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3943 603 41 0 4378 0
vsize: 17676
[startup+550.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3967 0 0 0 54994 13 0 0 25 0 1 0 421434736 18100224 3945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3945 603 41 0 4378 0
vsize: 17676
[startup+560.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3967 0 0 0 55994 13 0 0 25 0 1 0 421434736 18100224 3945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3945 603 41 0 4378 0
vsize: 17676
[startup+570.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3967 0 0 0 56994 13 0 0 25 0 1 0 421434736 18100224 3945 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3945 603 41 0 4378 0
vsize: 17676
[startup+580.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3967 0 0 0 57994 13 0 0 25 0 1 0 421434736 18100224 3945 4294967295 134512640 134672761 3221224560 3221223744 134558977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3945 603 41 0 4378 0
vsize: 17676
[startup+590.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3967 0 0 0 58994 13 0 0 25 0 1 0 421434736 18100224 3945 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3945 603 41 0 4378 0
vsize: 17676
[startup+600.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 59995 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+610.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 60995 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+620.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 61995 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+630.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 62995 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+640.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 63995 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+650.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 64996 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+660.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 65996 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+670.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 66996 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+680.006 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 67996 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+690.005 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3968 0 0 0 68996 13 0 0 25 0 1 0 421434736 18100224 3946 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3946 603 41 0 4378 0
vsize: 17676
[startup+700.005 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3970 0 0 0 69996 13 0 0 25 0 1 0 421434736 18100224 3948 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3948 603 41 0 4378 0
vsize: 17676
[startup+710.006 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 70996 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+720.005 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 71996 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+730.005 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 72997 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+740.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 73997 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223824 134562218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+750.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 74997 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+760.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 75997 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+770.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 76997 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+780.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 77997 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+790.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 78998 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+800.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 79998 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+810.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 80998 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+820.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 81998 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+830.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 82998 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+840.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 83999 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+850.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3973 0 0 0 84999 13 0 0 25 0 1 0 421434736 18100224 3951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3951 603 41 0 4378 0
vsize: 17676
[startup+860.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 85999 13 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+870.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 86999 13 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+880.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 87999 13 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+890.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3363
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 88999 13 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+900.027 s]
Raw data (loadavg): 1.16 1.03 0.93 3/56 3410
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 90001 13 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+910.028 s]
Raw data (loadavg): 1.13 1.03 0.93 2/54 3416
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 90999 15 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+920.028 s]
Raw data (loadavg): 1.11 1.03 0.93 2/54 3416
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 91999 15 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+930.027 s]
Raw data (loadavg): 1.10 1.03 0.93 2/54 3416
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 92999 15 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+940.027 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 3416
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3982 0 0 0 93999 15 0 0 25 0 1 0 421434736 18100224 3960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3960 603 41 0 4378 0
vsize: 17676
[startup+950.028 s]
Raw data (loadavg): 1.07 1.03 0.93 2/54 3416
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3983 0 0 0 94999 15 0 0 25 0 1 0 421434736 18100224 3961 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3961 603 41 0 4378 0
vsize: 17676
[startup+960.027 s]
Raw data (loadavg): 1.06 1.03 0.93 2/54 3416
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 95999 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223744 134559385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+970.027 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 96999 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+980.028 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 98000 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+990.028 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 99000 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+1000.03 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 100000 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+1010.03 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 101000 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+1020.03 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3986 0 0 0 102000 15 0 0 25 0 1 0 421434736 18100224 3964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+1030.03 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 103000 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1040.03 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 104001 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223744 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1050.03 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 105001 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1060.03 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 106001 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1070.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 107001 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 108001 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 109001 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 110002 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 111002 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 112002 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 113002 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 114002 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 115003 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 116003 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 117003 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 118003 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 119003 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3418
Raw data (stat): 3363 (minisat+) R 3362 30701 30700 0 -1 0 3987 0 0 0 120004 15 0 0 25 0 1 0 421434736 18100224 3965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 3965 603 41 0 4378 0
vsize: 17676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 3418
Raw data (stat): 3363 (minisat+) Z 3362 30701 30700 0 -1 12 3990 0 0 0 120004 16 0 0 25 0 1 0 421434736 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.04
CPU time (s): 1200.21
CPU user time (s): 1200.04
CPU system time (s): 0.163975
CPU usage (%): 100.014
Max. virtual memory (Kb): 17676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####