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/submitted/een/normalized-lseu.opb
MD5SUM	a578bf261896413ca78de4dc6db2447f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1120
Optimality of the best value was proved	NO
Number of terms in the objective function	85
Biggest coefficient in the objective function	517
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	15494
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1656
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	15494
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02184
Number of variables	89
Total number of constraints	28
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	2
Maximum length of a constraint	47
Trace number 6974

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 20:45:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5028 boxname=wulflinc23 idbench=387 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a578bf261896413ca78de4dc6db2447f  /oldhome/oroussel/tmp/wulflinc23/normalized-lseu.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-lseu.opb /oldhome/oroussel/tmp/wulflinc23/normalized-lseu.opb
IDLAUNCH: 5028
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        867368 kB
Buffers:         35364 kB
Cached:          89088 kB
SwapCached:        192 kB
Active:          62912 kB
Inactive:        64584 kB
HighTotal:      131008 kB
HighFree:        37996 kB
LowTotal:       903652 kB
LowFree:        829372 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34184 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:05:27 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 5028 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): .....s
c ---[  26]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  25]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  14]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  13]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  12]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   9]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[   8]---> Adder-cost: 37   maxlim: 99   bits: 8/7
c ---[   7]---> Adder-cost: 44   maxlim: 125   bits: 8/7
c ---[   6]---> Adder-cost: 122   maxlim: 179   bits: 9/8
c ---[   4]---> Adder-cost: 184   maxlim: 205   bits: 9/8
c ---[   3]---> Adder-cost: 175   maxlim: 331   bits: 10/9
c ---[   1]---> Adder-cost: 276   maxlim: 540   bits: 11/10
c ---[   0]---> Adder-cost: 79   maxlim: 66   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6073    21615 |    2024       0        0     nan |  0.000 % |
c |       102 |    6030    21468 |    2226      98      640     6.5 |  7.216 % |
c ==============================================================================
c [1mFound solution: 3011[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 596   maxlim: 12483   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       188 |   10093    35910 |    3364     184     1957    10.6 |  7.216 % |
c |       288 |   10054    35777 |    3700     281     2808    10.0 |  5.172 % |
c |       439 |   10054    35777 |    4070     432     9286    21.5 |  5.172 % |
c |       664 |   10033    35702 |    4477     654    11206    17.1 |  5.232 % |
c |      1001 |    9964    35478 |    4925     979    15407    15.7 |  5.648 % |
c |      1507 |    9964    35478 |    5417    1485    28059    18.9 |  5.648 % |
c ==============================================================================
c [1mFound solution: 2309[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13185   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1534 |    9976    35533 |    3325    1512    28519    18.9 |  5.648 % |
c ==============================================================================
c [1mFound solution: 2207[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13287   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1557 |    9981    35564 |    3327    1535    28967    18.9 |  5.648 % |
c |      1658 |    9969    35525 |    3659    1635    30567    18.7 |  6.095 % |
c |      1808 |    9933    35399 |    4025    1780    33706    18.9 |  6.272 % |
c |      2036 |    9933    35399 |    4428    2008    41590    20.7 |  6.272 % |
c |      2373 |    9933    35399 |    4871    2345    61525    26.2 |  6.272 % |
c |      2879 |    9896    35277 |    5358    2843    71094    25.0 |  6.568 % |
c |      3642 |    9896    35277 |    5893    3606   100482    27.9 |  6.568 % |
c ==============================================================================
c [1mFound solution: 1247[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14247   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3705 |    9893    35282 |    3297    3668   101724    27.7 |  6.568 % |
c |      3806 |    9884    35251 |    3626    1934    44069    22.8 |  7.067 % |
c |      3956 |    9884    35251 |    3989    2084    48097    23.1 |  7.067 % |
c |      4181 |    9884    35251 |    4388    2309    53409    23.1 |  7.067 % |
c |      4519 |    9884    35251 |    4827    2647    64104    24.2 |  7.067 % |
c |      5026 |    9875    35220 |    5309    3147    79874    25.4 |  7.126 % |
c |      5786 |    9875    35220 |    5840    3907   115559    29.6 |  7.126 % |
c |      6925 |    9875    35220 |    6424    5046   166590    33.0 |  7.126 % |
c |      8634 |    9875    35220 |    7067    6755   249858    37.0 |  7.126 % |
c |     11196 |    9851    35138 |    7774    5550   213889    38.5 |  7.362 % |
c |     15043 |    9851    35138 |    8551    5263   207158    39.4 |  7.362 % |
c |     20810 |    9851    35138 |    9406    6568   279286    42.5 |  7.362 % |
c |     29459 |    9851    35138 |   10347    5303   229207    43.2 |  7.362 % |
c |     42434 |    9845    35118 |   11382    7586   298956    39.4 |  7.421 % |
c |     61896 |    9830    35065 |   12520    9340   337411    36.1 |  7.479 % |
c ==============================================================================
c [1mFound solution: 1238[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14256   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67401 |    9836    35099 |    3278    8255   375581    45.5 |  7.479 % |
c |     67502 |    9836    35099 |    3605    2165    52567    24.3 |  7.584 % |
c |     67652 |    9836    35099 |    3966    2315    58839    25.4 |  7.584 % |
c |     67877 |    9836    35099 |    4363    2540    67588    26.6 |  7.584 % |
c |     68214 |    9836    35099 |    4799    2877    80158    27.9 |  7.584 % |
c |     68722 |    9836    35099 |    5279    3385   100539    29.7 |  7.584 % |
c |     69481 |    9836    35099 |    5807    4144   130588    31.5 |  7.584 % |
c |     70622 |    9836    35099 |    6387    5285   182181    34.5 |  7.584 % |
c |     72333 |    9836    35099 |    7026    3629   111653    30.8 |  7.584 % |
c |     74895 |    9836    35099 |    7729    6191   252707    40.8 |  7.584 % |
c |     78739 |    9836    35099 |    8502    5889   238538    40.5 |  7.584 % |
c ==============================================================================
c [1mFound solution: 1169[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14325   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79042 |    9847    35166 |    3282    6192   253187    40.9 |  7.584 % |
c |     79142 |    9847    35166 |    3610    3196   105723    33.1 |  7.846 % |
c |     79294 |    9847    35166 |    3971    3348   108648    32.5 |  7.845 % |
c |     79520 |    9847    35166 |    4368    3574   113311    31.7 |  7.845 % |
c |     79857 |    9826    35095 |    4805    3908   125571    32.1 |  8.021 % |
c |     80365 |    9826    35095 |    5285    4416   148900    33.7 |  8.021 % |
c |     81124 |    9826    35095 |    5814    5175   184471    35.6 |  8.021 % |
c |     82264 |    9826    35095 |    6395    3216   105393    32.8 |  8.021 % |
c |     83973 |    9826    35095 |    7035    4925   177713    36.1 |  8.021 % |
c |     86538 |    9826    35095 |    7738    3820   132809    34.8 |  8.021 % |
c |     90387 |    9826    35095 |    8512    7669   323103    42.1 |  8.021 % |
c |     96154 |    9826    35095 |    9363    4515   166312    36.8 |  8.021 % |
c |    104803 |    9826    35095 |   10300    8279   353832    42.7 |  8.021 % |
c |    117778 |    9826    35095 |   11330   10569   456633    43.2 |  8.021 % |
c |    137239 |    9797    34996 |   12463    6722   251529    37.4 |  8.255 % |
c |    166434 |    9797    34996 |   13709   10358   435281    42.0 |  8.255 % |
c ==============================================================================
c [1mFound solution: 1153[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14341   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    208156 |    9767    34806 |    3255    9192   381097    41.5 |  8.255 % |
c |    208256 |    9767    34806 |    3580    2398    64757    27.0 |  8.640 % |
c |    208407 |    9767    34806 |    3938    2549    71185    27.9 |  8.640 % |
c |    208632 |    9767    34806 |    4332    2774    77018    27.8 |  8.640 % |
c |    208969 |    9767    34806 |    4765    3111    88902    28.6 |  8.640 % |
c |    209475 |    9767    34806 |    5242    3617   109712    30.3 |  8.640 % |
c |    210235 |    9767    34806 |    5766    4377   139690    31.9 |  8.640 % |
c |    211374 |    9767    34806 |    6343    5516   183651    33.3 |  8.640 % |
c |    213085 |    9767    34806 |    6977    3798   122296    32.2 |  8.640 % |
c |    215647 |    9767    34806 |    7675    6360   234426    36.9 |  8.640 % |
c |    219493 |    9767    34806 |    8442    6174   223054    36.1 |  8.640 % |
c |    225260 |    9767    34806 |    9286    7511   292353    38.9 |  8.640 % |
c |    233909 |    9767    34806 |   10215    6457   214838    33.3 |  8.640 % |
c |    246883 |    9767    34806 |   11237    8814   373462    42.4 |  8.640 % |
c |    266347 |    9767    34806 |   12360   10834   404302    37.3 |  8.640 % |
c |    295539 |    9767    34806 |   13596    8180   326664    39.9 |  8.640 % |
c |    339328 |    9767    34806 |   14956   10035   355391    35.4 |  8.640 % |
c ==============================================================================
c [1mFound solution: 1149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14345   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    382192 |    9771    34832 |    3257   14455   569460    39.4 |  8.640 % |
c |    382293 |    9771    34832 |    3582    1908    33350    17.5 |  8.746 % |
c |    382443 |    9771    34832 |    3940    2058    37382    18.2 |  8.746 % |
c |    382668 |    9771    34832 |    4335    2283    47363    20.7 |  8.746 % |
c |    383009 |    9771    34832 |    4768    2624    61094    23.3 |  8.746 % |
c |    383518 |    9771    34832 |    5245    3133    81874    26.1 |  8.746 % |
c |    384279 |    9771    34832 |    5769    3894   108552    27.9 |  8.746 % |
c |    385421 |    9771    34832 |    6346    5036   158825    31.5 |  8.746 % |
c |    387129 |    9771    34832 |    6981    3421   103589    30.3 |  8.746 % |
c |    389694 |    9771    34832 |    7679    5986   224174    37.4 |  8.746 % |
c |    393538 |    9771    34832 |    8447    5794   183943    31.7 |  8.746 % |
c |    399305 |    9771    34832 |    9292    7170   272931    38.1 |  8.746 % |
c |    407954 |    9771    34832 |   10221    6155   229284    37.3 |  8.746 % |
c |    420928 |    9771    34832 |   11244    8326   342197    41.1 |  8.747 % |
c |    440389 |    9771    34832 |   12368   10312   345478    33.5 |  8.746 % |
c |    469583 |    9771    34832 |   13605    7517   290343    38.6 |  8.746 % |
c |    513372 |    9771    34832 |   14965    9307   307826    33.1 |  8.746 % |
c |    579057 |    9771    34832 |   16462   13795   489919    35.5 |  8.746 % |
c |    677583 |    9771    34832 |   18108   11054   483773    43.8 |  8.746 % |
c ==============================================================================
c [1mFound solution: 1148[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14346   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    685157 |    9776    34860 |    3258    9371   350038    37.4 |  8.746 % |
c |    685257 |    9776    34860 |    3583    2443    59326    24.3 |  8.800 % |
c |    685408 |    9776    34860 |    3942    2594    65884    25.4 |  8.800 % |
c |    685633 |    9776    34860 |    4336    2819    74074    26.3 |  8.800 % |
c |    685970 |    9776    34860 |    4770    3156    88055    27.9 |  8.800 % |
c |    686478 |    9776    34860 |    5247    3664   104632    28.6 |  8.800 % |
c |    687241 |    9776    34860 |    5771    4427   131990    29.8 |  8.800 % |
c |    688380 |    9776    34860 |    6348    5566   179255    32.2 |  8.800 % |
c |    690088 |    9776    34860 |    6983    3906   116010    29.7 |  8.800 % |
c |    692651 |    9776    34860 |    7682    6469   220117    34.0 |  8.800 % |
c |    696496 |    9776    34860 |    8450    6228   232719    37.4 |  8.800 % |
c |    702264 |    9776    34860 |    9295    7551   267685    35.5 |  8.800 % |
c |    710913 |    9776    34860 |   10224    6597   220688    33.5 |  8.800 % |
c |    723887 |    9776    34860 |   11247    8918   331808    37.2 |  8.800 % |
c |    743348 |    9776    34860 |   12372   10871   380532    35.0 |  8.800 % |
c |    772540 |    9776    34860 |   13609    7938   323434    40.7 |  8.800 % |
c |    816329 |    9776    34860 |   14970    9607   385995    40.2 |  8.800 % |
c |    882013 |    9767    34829 |   16467   13408   559128    41.7 |  8.858 % |
c ==============================================================================
c [1mFound solution: 1145[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14349   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    914030 |    9769    34850 |    3256   11679   442723    37.9 |  8.858 % |
c |    914131 |    9769    34850 |    3581    3021    73038    24.2 |  8.964 % |
c |    914283 |    9769    34850 |    3939    3173    78959    24.9 |  8.964 % |
c |    914510 |    9769    34850 |    4333    3400    88396    26.0 |  8.964 % |
c |    914847 |    9769    34850 |    4767    3737   101811    27.2 |  8.964 % |
c |    915353 |    9769    34850 |    5243    4243   121394    28.6 |  8.964 % |
c |    916113 |    9769    34850 |    5768    5003   150782    30.1 |  8.964 % |
c |    917252 |    9769    34850 |    6345    3090    74750    24.2 |  8.964 % |
c |    918961 |    9769    34850 |    6979    4799   140614    29.3 |  8.964 % |
c |    921523 |    9769    34850 |    7677    7361   248672    33.8 |  8.964 % |
c |    925367 |    9769    34850 |    8445    7069   272434    38.5 |  8.964 % |
c |    931135 |    9769    34850 |    9289    8348   341038    40.9 |  8.964 % |
c |    939784 |    9769    34850 |   10218    7340   275344    37.5 |  8.964 % |
c |    952760 |    9769    34850 |   11240    9772   373955    38.3 |  8.964 % |
c |    972222 |    9769    34850 |   12364   11632   495444    42.6 |  8.964 % |
c |   1001414 |    9769    34850 |   13601    8855   305916    34.5 |  8.964 % |
c |   1045203 |    9769    34850 |   14961   10486   392735    37.5 |  8.964 % |
c |   1110890 |    9769    34850 |   16457   14823   483383    32.6 |  8.964 % |
c |   1209417 |    9760    34819 |   18103   12268   554476    45.2 |  9.022 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.68 2/54 13012
Raw data (stat): 13012 (runsolver) R 13011 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487573994 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.0006 s]
Raw data (loadavg): 0.87 0.94 0.69 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 956 0 0 0 996 2 0 0 25 0 1 0 487573994 5591040 934 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1365 934 603 41 0 1324 0
vsize: 5460
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.69 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1158 0 0 0 1995 2 0 0 25 0 1 0 487573994 6385664 1136 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1559 1136 603 41 0 1518 0
vsize: 6236
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.94 0.69 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1219 0 0 0 2995 3 0 0 25 0 1 0 487573994 6660096 1197 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1626 1197 603 41 0 1585 0
vsize: 6504
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.69 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1265 0 0 0 3994 3 0 0 25 0 1 0 487573994 6795264 1243 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1659 1243 603 41 0 1618 0
vsize: 6636
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.70 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1300 0 0 0 4993 4 0 0 25 0 1 0 487573994 6930432 1278 4294967295 134512640 134672761 3221224576 3221223744 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1692 1278 603 41 0 1651 0
vsize: 6768
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.94 0.70 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1375 0 0 0 5992 4 0 0 25 0 1 0 487573994 7204864 1353 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1759 1353 603 41 0 1718 0
vsize: 7036
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.95 0.70 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1375 0 0 0 6992 4 0 0 25 0 1 0 487573994 7204864 1353 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1759 1353 603 41 0 1718 0
vsize: 7036
[startup+80.0022 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1375 0 0 0 7992 4 0 0 25 0 1 0 487573994 7204864 1353 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1759 1353 603 41 0 1718 0
vsize: 7036
[startup+90.0018 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1375 0 0 0 8992 4 0 0 25 0 1 0 487573994 7204864 1353 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1759 1353 603 41 0 1718 0
vsize: 7036
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.71 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1381 0 0 0 9992 4 0 0 25 0 1 0 487573994 7352320 1359 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1795 1359 603 41 0 1754 0
vsize: 7180
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.71 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1403 0 0 0 10992 5 0 0 25 0 1 0 487573994 7352320 1381 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1795 1381 603 41 0 1754 0
vsize: 7180
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1425 0 0 0 11992 5 0 0 25 0 1 0 487573994 7499776 1403 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1403 603 41 0 1790 0
vsize: 7324
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1463 0 0 0 12992 5 0 0 25 0 1 0 487573994 7647232 1441 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1867 1441 603 41 0 1826 0
vsize: 7468
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1517 0 0 0 13992 5 0 0 25 0 1 0 487573994 7917568 1495 4294967295 134512640 134672761 3221224576 3221223672 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1933 1495 603 41 0 1892 0
vsize: 7732
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1648 0 0 0 14991 6 0 0 25 0 1 0 487573994 8458240 1626 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2065 1626 603 41 0 2024 0
vsize: 8260
[startup+160.002 s]
Raw data (loadavg): 0.99 0.95 0.73 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1714 0 0 0 15991 6 0 0 25 0 1 0 487573994 8724480 1692 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2130 1692 603 41 0 2089 0
vsize: 8520
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1730 0 0 0 16991 6 0 0 25 0 1 0 487573994 8880128 1708 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1708 603 41 0 2127 0
vsize: 8672
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 17991 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223576 1075349768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 18992 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 19992 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 20992 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 21992 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 22992 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 23993 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 24993 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223680 134560322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+260.003 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 25993 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 26993 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223732 134565154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 27993 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1731 0 0 0 28993 6 0 0 25 0 1 0 487573994 8880128 1709 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1709 603 41 0 2127 0
vsize: 8672
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1753 0 0 0 29993 6 0 0 25 0 1 0 487573994 8880128 1731 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2168 1731 603 41 0 2127 0
vsize: 8672
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1786 0 0 0 30993 7 0 0 25 0 1 0 487573994 9011200 1764 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2200 1764 603 41 0 2159 0
vsize: 8800
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1794 0 0 0 31994 7 0 0 25 0 1 0 487573994 9154560 1772 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1772 603 41 0 2194 0
vsize: 8940
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1795 0 0 0 32993 7 0 0 25 0 1 0 487573994 9154560 1773 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2235 1773 603 41 0 2194 0
vsize: 8940
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1795 0 0 0 33993 7 0 0 25 0 1 0 487573994 9154560 1773 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1773 603 41 0 2194 0
vsize: 8940
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1795 0 0 0 34993 7 0 0 25 0 1 0 487573994 9154560 1773 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1773 603 41 0 2194 0
vsize: 8940
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1795 0 0 0 35993 7 0 0 25 0 1 0 487573994 9154560 1773 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1773 603 41 0 2194 0
vsize: 8940
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 36993 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 37993 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 38993 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 39994 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 40994 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 41994 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1796 0 0 0 42994 7 0 0 25 0 1 0 487573994 9154560 1774 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1774 603 41 0 2194 0
vsize: 8940
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1801 0 0 0 43994 7 0 0 25 0 1 0 487573994 9154560 1779 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1779 603 41 0 2194 0
vsize: 8940
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1801 0 0 0 44994 8 0 0 25 0 1 0 487573994 9154560 1779 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1779 603 41 0 2194 0
vsize: 8940
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1827 0 0 0 45995 8 0 0 25 0 1 0 487573994 9297920 1805 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2270 1805 603 41 0 2229 0
vsize: 9080
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1827 0 0 0 46995 8 0 0 25 0 1 0 487573994 9297920 1805 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2270 1805 603 41 0 2229 0
vsize: 9080
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1847 0 0 0 47995 8 0 0 25 0 1 0 487573994 9297920 1825 4294967295 134512640 134672761 3221224576 3221223496 1075352052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2270 1825 603 41 0 2229 0
vsize: 9080
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1847 0 0 0 48995 8 0 0 25 0 1 0 487573994 9297920 1825 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2270 1825 603 41 0 2229 0
vsize: 9080
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1868 0 0 0 49995 8 0 0 25 0 1 0 487573994 9428992 1846 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1846 603 41 0 2261 0
vsize: 9208
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1906 0 0 0 50995 8 0 0 25 0 1 0 487573994 9564160 1884 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2335 1884 603 41 0 2294 0
vsize: 9340
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1927 0 0 0 51995 8 0 0 25 0 1 0 487573994 9785344 1905 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2389 1905 603 41 0 2348 0
vsize: 9556
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1958 0 0 0 52995 8 0 0 25 0 1 0 487573994 9928704 1936 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2424 1936 603 41 0 2383 0
vsize: 9696
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1965 0 0 0 53995 8 0 0 25 0 1 0 487573994 9928704 1943 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2424 1943 603 41 0 2383 0
vsize: 9696
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1967 0 0 0 54995 8 0 0 25 0 1 0 487573994 9928704 1945 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2424 1945 603 41 0 2383 0
vsize: 9696
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1973 0 0 0 55996 8 0 0 25 0 1 0 487573994 9928704 1951 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2424 1951 603 41 0 2383 0
vsize: 9696
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1975 0 0 0 56996 8 0 0 25 0 1 0 487573994 9928704 1953 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2424 1953 603 41 0 2383 0
vsize: 9696
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 1981 0 0 0 57996 8 0 0 25 0 1 0 487573994 9928704 1959 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2424 1959 603 41 0 2383 0
vsize: 9696
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2087 0 0 0 58996 9 0 0 25 0 1 0 487573994 10334208 2065 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2523 2065 603 41 0 2482 0
vsize: 10092
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2103 0 0 0 59996 9 0 0 25 0 1 0 487573994 10493952 2081 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2562 2081 603 41 0 2521 0
vsize: 10248
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2110 0 0 0 60996 9 0 0 25 0 1 0 487573994 10493952 2088 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2562 2088 603 41 0 2521 0
vsize: 10248
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2110 0 0 0 61996 9 0 0 25 0 1 0 487573994 10493952 2088 4294967295 134512640 134672761 3221224576 3221223760 134559594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2562 2088 603 41 0 2521 0
vsize: 10248
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2110 0 0 0 62996 9 0 0 25 0 1 0 487573994 10493952 2088 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2562 2088 603 41 0 2521 0
vsize: 10248
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2173 0 0 0 63996 10 0 0 25 0 1 0 487573994 10760192 2151 4294967295 134512640 134672761 3221224576 3221223680 134555076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2627 2151 603 41 0 2586 0
vsize: 10508
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2173 0 0 0 64995 10 0 0 25 0 1 0 487573994 10760192 2151 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2627 2151 603 41 0 2586 0
vsize: 10508
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2173 0 0 0 65995 10 0 0 25 0 1 0 487573994 10760192 2151 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2151 603 41 0 2586 0
vsize: 10508
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2173 0 0 0 66995 10 0 0 25 0 1 0 487573994 10760192 2151 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2151 603 41 0 2586 0
vsize: 10508
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2173 0 0 0 67995 10 0 0 25 0 1 0 487573994 10760192 2151 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2151 603 41 0 2586 0
vsize: 10508
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 68995 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 69995 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 70995 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223760 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 71995 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 72996 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 73996 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 74996 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 75996 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 76996 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 77997 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2174 0 0 0 78997 10 0 0 25 0 1 0 487573994 10760192 2152 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2152 603 41 0 2586 0
vsize: 10508
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2175 0 0 0 79997 10 0 0 25 0 1 0 487573994 10760192 2153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2153 603 41 0 2586 0
vsize: 10508
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 80997 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+820.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 81997 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+830.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 82998 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223764 1075347030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 83998 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 84998 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 85998 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+870.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 86998 10 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.84 3/56 13044
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 87997 14 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13065
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 88994 14 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13065
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 89994 14 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13065
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 90994 15 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13065
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 91994 15 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223712 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13065
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 92994 15 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13065
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 93994 16 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223740 134565156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 94994 16 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 95994 16 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2176 0 0 0 96993 17 0 0 25 0 1 0 487573994 10760192 2154 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2154 603 41 0 2586 0
vsize: 10508
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2177 0 0 0 97993 17 0 0 25 0 1 0 487573994 10760192 2155 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2155 603 41 0 2586 0
vsize: 10508
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2180 0 0 0 98993 17 0 0 25 0 1 0 487573994 10760192 2158 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2158 603 41 0 2586 0
vsize: 10508
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2180 0 0 0 99993 17 0 0 25 0 1 0 487573994 10760192 2158 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2158 603 41 0 2586 0
vsize: 10508
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2189 0 0 0 100993 18 0 0 25 0 1 0 487573994 10760192 2167 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2167 603 41 0 2586 0
vsize: 10508
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2189 0 0 0 101993 18 0 0 25 0 1 0 487573994 10760192 2167 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2167 603 41 0 2586 0
vsize: 10508
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2189 0 0 0 102993 19 0 0 25 0 1 0 487573994 10760192 2167 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2167 603 41 0 2586 0
vsize: 10508
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2196 0 0 0 103992 19 0 0 25 0 1 0 487573994 10895360 2174 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2660 2174 603 41 0 2619 0
vsize: 10640
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2196 0 0 0 104992 19 0 0 25 0 1 0 487573994 10895360 2174 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2660 2174 603 41 0 2619 0
vsize: 10640
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2196 0 0 0 105992 19 0 0 25 0 1 0 487573994 10895360 2174 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2660 2174 603 41 0 2619 0
vsize: 10640
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2196 0 0 0 106992 20 0 0 25 0 1 0 487573994 10895360 2174 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2660 2174 603 41 0 2619 0
vsize: 10640
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2240 0 0 0 107992 20 0 0 25 0 1 0 487573994 11026432 2218 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2692 2218 603 41 0 2651 0
vsize: 10768
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2241 0 0 0 108992 21 0 0 25 0 1 0 487573994 11026432 2219 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2692 2219 603 41 0 2651 0
vsize: 10768
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2241 0 0 0 109991 21 0 0 25 0 1 0 487573994 11026432 2219 4294967295 134512640 134672761 3221224576 3221223776 134557814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2692 2219 603 41 0 2651 0
vsize: 10768
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2271 0 0 0 110991 22 0 0 25 0 1 0 487573994 11161600 2249 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2725 2249 603 41 0 2684 0
vsize: 10900
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2324 0 0 0 111991 22 0 0 25 0 1 0 487573994 11292672 2302 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2757 2302 603 41 0 2716 0
vsize: 11028
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2338 0 0 0 112991 22 0 0 25 0 1 0 487573994 11431936 2316 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2316 603 41 0 2750 0
vsize: 11164
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2343 0 0 0 113991 23 0 0 25 0 1 0 487573994 11431936 2321 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2321 603 41 0 2750 0
vsize: 11164
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2348 0 0 0 114991 23 0 0 25 0 1 0 487573994 11431936 2326 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2326 603 41 0 2750 0
vsize: 11164
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2350 0 0 0 115990 23 0 0 25 0 1 0 487573994 11431936 2328 4294967295 134512640 134672761 3221224576 3221223728 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2328 603 41 0 2750 0
vsize: 11164
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2352 0 0 0 116990 24 0 0 25 0 1 0 487573994 11431936 2330 4294967295 134512640 134672761 3221224576 3221223712 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2330 603 41 0 2750 0
vsize: 11164
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13067
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2352 0 0 0 117990 25 0 0 25 0 1 0 487573994 11431936 2330 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2330 603 41 0 2750 0
vsize: 11164
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13069
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2357 0 0 0 118989 25 0 0 25 0 1 0 487573994 11571200 2335 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2825 2335 603 41 0 2784 0
vsize: 11300
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 13069
Raw data (stat): 13012 (minisat+) R 13011 3260 3259 0 -1 0 2359 0 0 0 119989 25 0 0 25 0 1 0 487573994 11571200 2337 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2825 2337 603 41 0 2784 0
vsize: 11300
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.88 1/54 13069
Raw data (stat): 13012 (minisat+) Z 13011 3260 3259 0 -1 12 2362 0 0 0 119989 26 0 0 25 0 1 0 487573994 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.05
CPU time (s): 1200.16
CPU user time (s): 1199.9
CPU system time (s): 0.26296
CPU usage (%): 100.01
Max. virtual memory (Kb): 11300
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####