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 5236

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 22:47:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3704 boxname=wulflinc6 idbench=320 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  409f1cf0658f035df65cb61f3e4f598e  /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-2.opb /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-2.opb
IDLAUNCH: 3704
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        912168 kB
Buffers:         34900 kB
Cached:          65476 kB
SwapCached:       2644 kB
Active:          51848 kB
Inactive:        54024 kB
HighTotal:      131008 kB
HighFree:        61656 kB
LowTotal:       903652 kB
LowFree:        850512 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11072 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:07:56 (client local time) WITH STATUS 10 IN 1200.36 SECONDS
stats: 3704 7 1200.36 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]---> Adder-cost: 1165   maxlim: 24   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35809    84165 |   11936       0        0     nan |  0.000 % |
c |       100 |   35809    84165 |   13129     100      974     9.7 |  0.176 % |
c |       250 |   35791    84103 |   14442     246     3050    12.4 |  0.286 % |
c |       475 |   35791    84103 |   15886     471     6682    14.2 |  0.286 % |
c |       812 |   35773    84041 |   17475     804    11516    14.3 |  0.406 % |
c |      1318 |   35755    83979 |   19223    1304    17697    13.6 |  0.515 % |
c |      2077 |   35693    83765 |   21145    2045    31729    15.5 |  0.977 % |
c |      3216 |   35459    82963 |   23259    3123    57427    18.4 |  2.582 % |
c |      4924 |   34404    79336 |   25585    4526    88382    19.5 | 11.396 % |
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 |      5079 |   34405    79342 |   11468    4681    91494    19.5 | 11.396 % |
c |      5179 |   34399    79322 |   12614    4778    94078    19.7 | 11.503 % |
c |      5329 |   34399    79322 |   13876    4927    95992    19.5 | 11.556 % |
c |      5554 |   34278    78905 |   15263    5094   101108    19.8 | 12.644 % |
c |      5891 |   34109    78324 |   16790    5396   110166    20.4 | 14.250 % |
c |      6397 |   33983    77892 |   18469    5846   124249    21.3 | 15.503 % |
c |      7156 |   33850    77433 |   20316    6539   147616    22.6 | 16.883 % |
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 |      7591 |   33855    77456 |   11285    6974   163836    23.5 | 16.883 % |
c |      7691 |   33855    77456 |   12413    7074   168986    23.9 | 16.924 % |
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 |      7822 |   33856    77461 |   11285    7205   174078    24.2 | 16.924 % |
c |      7923 |   33856    77461 |   12413    7306   179257    24.5 | 16.978 % |
c |      8073 |   33856    77461 |   13654    7456   180958    24.3 | 16.972 % |
c |      8298 |   33856    77461 |   15020    7681   193472    25.2 | 16.978 % |
c |      8635 |   33808    77293 |   16522    8004   206424    25.8 | 17.429 % |
c |      9141 |   33808    77293 |   18174    8510   230249    27.1 | 17.432 % |
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 |      9282 |   33811    77306 |   11270    8651   236014    27.3 | 17.432 % |
c |      9383 |   33811    77306 |   12397    8752   241823    27.6 | 17.482 % |
c |      9533 |   33659    76772 |   13636    8822   247663    28.1 | 19.252 % |
c |      9758 |   33597    76560 |   15000    9023   254748    28.2 | 19.935 % |
c |     10095 |   33583    76512 |   16500    9351   267118    28.6 | 20.103 % |
c |     10602 |   33583    76512 |   18150    9858   287524    29.2 | 20.103 % |
c |     11361 |   33526    76315 |   19965   10595   321122    30.3 | 20.674 % |
c |     12501 |   33526    76315 |   21962   11735   404109    34.4 | 20.674 % |
c |     14209 |   33506    76245 |   24158   13413   492398    36.7 | 20.845 % |
c |     16773 |   33468    76113 |   26574   15883   670898    42.2 | 21.135 % |
c |     20617 |   33468    76113 |   29231   19727   959332    48.6 | 21.131 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23283 |   33446    76038 |   11148   22388  1140695    51.0 | 21.131 % |
c |     23384 |   33446    76038 |   12262   11295   615175    54.5 | 21.461 % |
c |     23534 |   33435    75999 |   13489   11441   622583    54.4 | 21.580 % |
c |     23760 |   33435    75999 |   14837   11667   630720    54.1 | 21.575 % |
c |     24097 |   33418    75940 |   16321   12001   658195    54.8 | 21.752 % |
c |     24604 |   33386    75828 |   17953   12504   681010    54.5 | 22.094 % |
c |     25363 |   33386    75828 |   19749   13263   725400    54.7 | 22.089 % |
c |     26502 |   33377    75797 |   21724   14375   797754    55.5 | 22.146 % |
c |     28210 |   33358    75730 |   23896   16079   894593    55.6 | 22.374 % |
c |     30772 |   33324    75612 |   26286   18633  1074823    57.7 | 22.717 % |
c |     34616 |   33324    75612 |   28915   22477  1303929    58.0 | 22.717 % |
c |     40383 |   33316    75582 |   31806   28240  1926038    68.2 | 22.780 % |
c |     49032 |   33232    75294 |   34987   18454  1331047    72.1 | 23.459 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56987 |   33198    75184 |   11066   26398  1902604    72.1 | 23.459 % |
c |     57087 |   33198    75184 |   12172    6701   378605    56.5 | 23.849 % |
c |     57238 |   33198    75184 |   13389    6852   382911    55.9 | 23.845 % |
c |     57463 |   33198    75184 |   14728    7077   398010    56.2 | 23.849 % |
c |     57800 |   33184    75136 |   16201    7406   409635    55.3 | 24.016 % |
c |     58306 |   33123    74925 |   17821    7903   434191    54.9 | 24.644 % |
c |     59065 |   33123    74925 |   19604    8662   482006    55.6 | 24.644 % |
c |     60204 |   33123    74925 |   21564    9801   548443    56.0 | 24.644 % |
c |     61912 |   33123    74925 |   23720   11509   657450    57.1 | 24.644 % |
c |     64474 |   33103    74855 |   26093   14061   884144    62.9 | 24.815 % |
c |     68321 |   33071    74745 |   28702   17871  1236641    69.2 | 25.100 % |
c |     74087 |   33071    74745 |   31572   23637  1597238    67.6 | 25.100 % |
c |     82736 |   33071    74745 |   34729   32286  2174640    67.4 | 25.104 % |
c |     95712 |   33071    74745 |   38202   23957  1579174    65.9 | 25.100 % |
c |    115176 |   33035    74623 |   42023   18151  1279250    70.5 | 25.385 % |
c |    144368 |   33035    74623 |   46225   18836  1425015    75.7 | 25.391 % |
c |    188157 |   33035    74623 |   50847   30548  3014314    98.7 | 25.391 % |
c |    253841 |   32987    74459 |   55932   23034  2881737   125.1 | 25.731 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    323621 |   32978    74407 |   10992   50384  4649046    92.3 | 25.731 % |
c |    323723 |   32978    74407 |   12091    7545   342663    45.4 | 25.789 % |
c |    323873 |   32963    74356 |   13300    7690   346540    45.1 | 25.903 % |
c |    324098 |   32963    74356 |   14630    7915   355701    44.9 | 25.903 % |
c |    324435 |   32963    74356 |   16093    8252   370934    45.0 | 25.898 % |
c |    324941 |   32963    74356 |   17702    8758   393337    44.9 | 25.898 % |
c |    325703 |   32963    74356 |   19472    9520   430862    45.3 | 25.901 % |
c |    326844 |   32963    74356 |   21420   10661   488593    45.8 | 25.899 % |
c |    328554 |   32944    74289 |   23562   12367   603948    48.8 | 26.127 % |
c |    331116 |   32944    74289 |   25918   14929   718978    48.2 | 26.127 % |
c |    334960 |   32944    74289 |   28510   18773  1095607    58.4 | 26.127 % |
c |    340726 |   32944    74289 |   31361   24539  1510691    61.6 | 26.131 % |
c |    349375 |   32944    74289 |   34497   14991   967952    64.6 | 26.131 % |
c |    362349 |   32917    74196 |   37947   27945  2147749    76.9 | 26.416 % |
c |    381810 |   32899    74134 |   41742   23026  1834531    79.7 | 26.526 % |
c |    411002 |   32899    74134 |   45916   24289  2514985   103.5 | 26.530 % |
c |    454791 |   32879    74064 |   50507   35871  2527636    70.5 | 26.697 % |
c |    520475 |   32879    74064 |   55558   28494  2704239    94.9 | 26.697 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    607593 |   32949    74282 |   10983   35851  2036984    56.8 | 26.697 % |
c |    607695 |   32913    74164 |   12081    8974   295474    32.9 | 27.268 % |
c |    607845 |   32913    74164 |   13289    9124   300705    33.0 | 27.268 % |
c |    608071 |   32905    74136 |   14618    9348   312113    33.4 | 27.380 % |
c |    608408 |   32905    74136 |   16080    9685   328242    33.9 | 27.380 % |
c |    608915 |   32905    74136 |   17688   10192   346039    34.0 | 27.380 % |
c |    609676 |   32905    74136 |   19457   10953   389941    35.6 | 27.385 % |
c |    610816 |   32905    74136 |   21402   12093   448152    37.1 | 27.380 % |
c |    612524 |   32905    74136 |   23543   13801   526560    38.2 | 27.380 % |
c |    615086 |   32905    74136 |   25897   16363   714691    43.7 | 27.384 % |
c |    618933 |   32905    74136 |   28487   20210   921399    45.6 | 27.380 % |
c |    624702 |   32905    74136 |   31335   25979  1166363    44.9 | 27.385 % |
c |    633351 |   32905    74136 |   34469   17501   644463    36.8 | 27.380 % |
c |    646325 |   32905    74136 |   37916   30475  1329319    43.6 | 27.385 % |
c |    665786 |   32905    74136 |   41707   25556  1464943    57.3 | 27.380 % |
c |    694979 |   32905    74136 |   45878   26966  1172313    43.5 | 27.385 % |
c |    738768 |   32905    74136 |   50466   40111  1612964    40.2 | 27.385 % |
#### 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.93 0.96 0.91 2/54 32692
Raw data (stat): 32692 (runsolver) R 32691 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421447051 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 1532 0 0 0 993 5 0 0 25 0 1 0 421447051 7827456 1510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1911 1510 603 41 0 1870 0
vsize: 7644
[startup+20.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 2206 0 0 0 1990 7 0 0 25 0 1 0 421447051 10571776 2184 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2581 2184 603 41 0 2540 0
vsize: 10324
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 2832 0 0 0 2988 9 0 0 25 0 1 0 421447051 13127680 2810 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3205 2810 603 41 0 3164 0
vsize: 12820
[startup+39.9997 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3479 0 0 0 3986 11 0 0 25 0 1 0 421447051 15933440 3457 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3890 3457 603 41 0 3849 0
vsize: 15560
[startup+50.0001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3479 0 0 0 4986 11 0 0 25 0 1 0 421447051 15933440 3457 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3890 3457 603 41 0 3849 0
vsize: 15560
[startup+60.0001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3479 0 0 0 5986 12 0 0 25 0 1 0 421447051 15933440 3457 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3890 3457 603 41 0 3849 0
vsize: 15560
[startup+70.0001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3479 0 0 0 6986 12 0 0 25 0 1 0 421447051 15933440 3457 4294967295 134512640 134672761 3221224560 3221223744 134559390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3890 3457 603 41 0 3849 0
vsize: 15560
[startup+80.0005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3549 0 0 0 7986 12 0 0 25 0 1 0 421447051 16207872 3527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3957 3527 603 41 0 3916 0
vsize: 15828
[startup+90.0004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3719 0 0 0 8986 13 0 0 25 0 1 0 421447051 16871424 3697 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4119 3697 603 41 0 4078 0
vsize: 16476
[startup+99.9996 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3719 0 0 0 9986 13 0 0 25 0 1 0 421447051 16871424 3697 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4119 3697 603 41 0 4078 0
vsize: 16476
[startup+110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 3765 0 0 0 10987 13 0 0 25 0 1 0 421447051 17002496 3743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4151 3743 603 41 0 4110 0
vsize: 16604
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 4140 0 0 0 11985 14 0 0 25 0 1 0 421447051 18624512 4118 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4547 4118 603 41 0 4506 0
vsize: 18188
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 4140 0 0 0 12986 14 0 0 25 0 1 0 421447051 18624512 4118 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4547 4118 603 41 0 4506 0
vsize: 18188
[startup+139.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 4140 0 0 0 13986 14 0 0 25 0 1 0 421447051 18624512 4118 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4547 4118 603 41 0 4506 0
vsize: 18188
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 4205 0 0 0 14986 14 0 0 25 0 1 0 421447051 18894848 4183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4613 4183 603 41 0 4572 0
vsize: 18452
[startup+159.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 4717 0 0 0 15985 16 0 0 25 0 1 0 421447051 21028864 4695 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4695 603 41 0 5093 0
vsize: 20536
[startup+169.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5013 0 0 0 16985 16 0 0 25 0 1 0 421447051 22224896 4991 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5426 4991 603 41 0 5385 0
vsize: 21704
[startup+179.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5013 0 0 0 17985 16 0 0 25 0 1 0 421447051 22224896 4991 4294967295 134512640 134672761 3221224560 3221223744 134559588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5426 4991 603 41 0 5385 0
vsize: 21704
[startup+189.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5013 0 0 0 18985 16 0 0 25 0 1 0 421447051 22224896 4991 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5426 4991 603 41 0 5385 0
vsize: 21704
[startup+199.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5013 0 0 0 19985 17 0 0 25 0 1 0 421447051 22224896 4991 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5426 4991 603 41 0 5385 0
vsize: 21704
[startup+209.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5067 0 0 0 20986 17 0 0 25 0 1 0 421447051 22355968 5045 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5458 5045 603 41 0 5417 0
vsize: 21832
[startup+219.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5468 0 0 0 21984 18 0 0 25 0 1 0 421447051 24084480 5446 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5880 5446 603 41 0 5839 0
vsize: 23520
[startup+229.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5852 0 0 0 22983 19 0 0 25 0 1 0 421447051 25542656 5830 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6236 5830 603 41 0 6195 0
vsize: 24944
[startup+239.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5852 0 0 0 23984 19 0 0 25 0 1 0 421447051 25542656 5830 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6236 5830 603 41 0 6195 0
vsize: 24944
[startup+249.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5854 0 0 0 24984 19 0 0 25 0 1 0 421447051 25542656 5832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6236 5832 603 41 0 6195 0
vsize: 24944
[startup+259.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5866 0 0 0 25984 19 0 0 25 0 1 0 421447051 25718784 5844 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6279 5844 603 41 0 6238 0
vsize: 25116
[startup+269.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5876 0 0 0 26985 19 0 0 25 0 1 0 421447051 25718784 5854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6279 5854 603 41 0 6238 0
vsize: 25116
[startup+279.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 5877 0 0 0 27985 19 0 0 25 0 1 0 421447051 25718784 5855 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6279 5855 603 41 0 6238 0
vsize: 25116
[startup+289.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6182 0 0 0 28985 20 0 0 25 0 1 0 421447051 26918912 6160 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6572 6160 603 41 0 6531 0
vsize: 26288
[startup+299.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6601 0 0 0 29984 21 0 0 25 0 1 0 421447051 28667904 6579 4294967295 134512640 134672761 3221224560 3221223664 134555114 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6999 6579 603 41 0 6958 0
vsize: 27996
[startup+309.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6623 0 0 0 30984 21 0 0 25 0 1 0 421447051 28803072 6601 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7032 6601 603 41 0 6991 0
vsize: 28128
[startup+319.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6623 0 0 0 31985 21 0 0 25 0 1 0 421447051 28803072 6601 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7032 6601 603 41 0 6991 0
vsize: 28128
[startup+329.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6624 0 0 0 32985 21 0 0 25 0 1 0 421447051 28803072 6602 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7032 6602 603 41 0 6991 0
vsize: 28128
[startup+339.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6624 0 0 0 33985 21 0 0 25 0 1 0 421447051 28803072 6602 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7032 6602 603 41 0 6991 0
vsize: 28128
[startup+349.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6624 0 0 0 34986 21 0 0 25 0 1 0 421447051 28803072 6602 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7032 6602 603 41 0 6991 0
vsize: 28128
[startup+359.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6624 0 0 0 35986 21 0 0 25 0 1 0 421447051 28803072 6602 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7032 6602 603 41 0 6991 0
vsize: 28128
[startup+369.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 6799 0 0 0 36986 21 0 0 25 0 1 0 421447051 29458432 6777 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7192 6777 603 41 0 7151 0
vsize: 28768
[startup+379.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7257 0 0 0 37984 23 0 0 25 0 1 0 421447051 31313920 7235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7645 7235 603 41 0 7604 0
vsize: 30580
[startup+389.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7537 0 0 0 38983 25 0 0 25 0 1 0 421447051 32509952 7515 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7937 7515 603 41 0 7896 0
vsize: 31748
[startup+399.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7538 0 0 0 39983 25 0 0 25 0 1 0 421447051 32509952 7516 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7937 7516 603 41 0 7896 0
vsize: 31748
[startup+409.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7538 0 0 0 40983 25 0 0 25 0 1 0 421447051 32509952 7516 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7937 7516 603 41 0 7896 0
vsize: 31748
[startup+419.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7538 0 0 0 41983 25 0 0 25 0 1 0 421447051 32509952 7516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7937 7516 603 41 0 7896 0
vsize: 31748
[startup+429.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7538 0 0 0 42983 25 0 0 25 0 1 0 421447051 32509952 7516 4294967295 134512640 134672761 3221224560 3221223664 134555314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7937 7516 603 41 0 7896 0
vsize: 31748
[startup+439.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7538 0 0 0 43984 25 0 0 25 0 1 0 421447051 32509952 7516 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7937 7516 603 41 0 7896 0
vsize: 31748
[startup+449.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7538 0 0 0 44984 25 0 0 25 0 1 0 421447051 32509952 7516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7937 7516 603 41 0 7896 0
vsize: 31748
[startup+459.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 7676 0 0 0 45984 26 0 0 25 0 1 0 421447051 33046528 7654 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8068 7654 603 41 0 8027 0
vsize: 32272
[startup+469.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8023 0 0 0 46984 26 0 0 25 0 1 0 421447051 34504704 8001 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8001 603 41 0 8383 0
vsize: 33696
[startup+479.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8023 0 0 0 47984 26 0 0 25 0 1 0 421447051 34504704 8001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8001 603 41 0 8383 0
vsize: 33696
[startup+489.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8023 0 0 0 48984 26 0 0 25 0 1 0 421447051 34504704 8001 4294967295 134512640 134672761 3221224560 3221223516 1075349791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8001 603 41 0 8383 0
vsize: 33696
[startup+499.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 49985 26 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+509.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 50985 26 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+519.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 51985 26 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+529.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 52986 26 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+539.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 53986 26 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+549.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 54986 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+559.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 55986 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+569.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 56987 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 57987 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+589.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 58987 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+599.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 59988 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+609.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 60988 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223632 134553539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+619.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 61988 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223664 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+629.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 62989 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+639.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8024 0 0 0 63989 27 0 0 25 0 1 0 421447051 34504704 8002 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8002 603 41 0 8383 0
vsize: 33696
[startup+649.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 64990 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+659.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 65990 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+669.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 66990 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+679.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 67991 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+689.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 68991 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 69991 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 70992 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32692
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 71992 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+730.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32693
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 72993 27 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+740.003 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 73977 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+750.003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 74977 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+760.003 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 75977 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+770.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 76978 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+780.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 77978 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+790.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 78978 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+800.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32745
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 79979 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+810.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 80979 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+820.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 81979 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+830.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 82980 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+840.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 83980 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+850.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 84980 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+860.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 85981 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+870.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 86980 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223744 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+880.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 87980 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+890.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 88981 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+900.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 89981 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+910.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 90981 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+920.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 91982 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+930.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 92982 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+940.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 93982 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+950.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 94983 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+960.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 95983 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+970.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 96983 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223652 1075351196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+980.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 97984 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+990.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 98984 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 99984 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 100984 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 101985 42 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 102985 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32747
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 103985 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 104986 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 105986 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 106986 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 107987 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 108987 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 109987 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 110988 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 111988 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 112988 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 113989 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 114989 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 115989 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 116990 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 117990 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 118991 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32749
Raw data (stat): 32692 (minisat+) R 32691 29653 29652 0 -1 0 8025 0 0 0 119991 43 0 0 25 0 1 0 421447051 34504704 8003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 8003 603 41 0 8383 0
vsize: 33696
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32749
Raw data (stat): 32692 (minisat+) Z 32691 29653 29652 0 -1 12 8028 0 0 0 119991 44 0 0 25 0 1 0 421447051 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.36
CPU user time (s): 1199.91
CPU system time (s): 0.447931
CPU usage (%): 100.028
Max. virtual memory (Kb): 33696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####