PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888496 kB
Buffers:         36600 kB
Cached:          89044 kB
SwapCached:        564 kB
Active:          54940 kB
Inactive:        74168 kB
HighTotal:      131008 kB
HighFree:        38024 kB
LowTotal:       903652 kB
LowFree:        850472 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11420 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:53:41 (client local time) WITH STATUS 10 IN 1209.96 SECONDS
stats: 4829 7 1209.96 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17831 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17831    35662 |    5943       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   52019   115771 |   17339       0        0     nan |  0.000 % |
c |       100 |   51519   114636 |   19072      83      569     6.9 |  1.596 % |
c |       250 |   50271   111802 |   20980     194     1293     6.7 |  4.362 % |
c |       475 |   48358   107437 |   23078     369     3275     8.9 |  9.245 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       773 |   46950   104312 |   15650     607     5979     9.9 |  9.245 % |
c |       873 |   45521   101018 |   17215     668     6806    10.2 | 17.705 % |
c |      1025 |   44598    98886 |   18936     796     8486    10.7 | 20.161 % |
c |      1250 |   43104    95436 |   20830     966     9892    10.2 | 24.158 % |
c |      1587 |   40405    89151 |   22913    1175    13250    11.3 | 31.685 % |
c |      2093 |   36538    80178 |   25204    1515    18247    12.0 | 41.888 % |
c |      2852 |   33640    73384 |   27724    2064    24505    11.9 | 50.178 % |
c |      3991 |   30079    65045 |   30497    2904    38939    13.4 | 60.474 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4098 |   29253    63066 |    9751    2891    38642    13.4 | 60.474 % |
c |      4198 |   29028    62535 |   10726    2980    40140    13.5 | 63.520 % |
c |      4348 |   28037    60215 |   11798    2983    41845    14.0 | 66.382 % |
c |      4573 |   27892    59877 |   12978    3165    44262    14.0 | 66.772 % |
c |      4910 |   27892    59877 |   14276    3502    53627    15.3 | 66.771 % |
c |      5416 |   27793    59647 |   15704    3969    66696    16.8 | 67.051 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5746 |   27665    59362 |    9221    4250    76780    18.1 | 67.051 % |
c |      5847 |   27659    59348 |   10143    4346    78774    18.1 | 67.599 % |
c |      5998 |   27586    59178 |   11157    4484    81221    18.1 | 67.810 % |
c |      6223 |   27570    59140 |   12273    4705    89755    19.1 | 67.861 % |
c |      6560 |   27308    58522 |   13500    4945   103445    20.9 | 68.613 % |
c |      7066 |   27019    57835 |   14850    5349   115694    21.6 | 69.491 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7303 |   26724    57117 |    8908    5505   125234    22.7 | 69.491 % |
c |      7403 |   26586    56791 |    9798    5593   129533    23.2 | 70.687 % |
c |      7555 |   26586    56791 |   10778    5745   136110    23.7 | 70.687 % |
c |      7781 |   26582    56782 |   11856    5968   146214    24.5 | 70.695 % |
c |      8118 |   25801    54946 |   13042    5969   150835    25.3 | 72.993 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8536 |   25888    55171 |    8629    6387   174079    27.3 | 72.993 % |
c |      8636 |   25819    55007 |    9491    6471   176118    27.2 | 73.206 % |
c |      8786 |   25698    54726 |   10441    6479   179794    27.8 | 73.533 % |
c |      9011 |   25226    53608 |   11485    6591   183992    27.9 | 74.975 % |
c |      9348 |   25216    53585 |   12633    6920   196171    28.3 | 75.000 % |
c |      9854 |   25216    53585 |   13897    7426   225313    30.3 | 75.000 % |
c |     10614 |   25206    53562 |   15286    8179   258486    31.6 | 75.025 % |
c |     11754 |   24582    52100 |   16815    8924   296829    33.3 | 76.878 % |
c |     13465 |   24011    50754 |   18497   10225   377735    36.9 | 78.571 % |
c |     16027 |   23884    50455 |   20346   12688   534488    42.1 | 78.949 % |
c |     19871 |   23838    50347 |   22381   16443   704895    42.9 | 79.083 % |
c |     25637 |   23621    49836 |   24619   22126   972380    43.9 | 79.737 % |
c |     34288 |   23318    49115 |   27081   30477  1323824    43.4 | 80.710 % |
c |     47262 |   23276    49017 |   29789   21542   792092    36.8 | 80.827 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56388 |   23254    48945 |    7751   30665  1113463    36.3 | 80.827 % |
c |     56489 |   23254    48945 |    8526   15162   455183    30.0 | 80.889 % |
c |     56639 |   23254    48945 |    9378   15312   459283    30.0 | 80.889 % |
c |     56864 |   23254    48945 |   10316   15537   466427    30.0 | 80.889 % |
c |     57201 |   23254    48945 |   11348   15874   479204    30.2 | 80.889 % |
c |     57707 |   23248    48931 |   12483   16376   493517    30.1 | 80.906 % |
c |     58466 |   23248    48931 |   13731   17135   518587    30.3 | 80.906 % |
c |     59605 |   23201    48821 |   15104   18267   551224    30.2 | 81.048 % |
c |     61313 |   23201    48821 |   16614   19975   593871    29.7 | 81.048 % |
c |     63875 |   23201    48821 |   18276   22537   667223    29.6 | 81.048 % |
c |     67720 |   23027    48410 |   20104   26334   871844    33.1 | 81.593 % |
c |     73486 |   23027    48410 |   22114   16850   569285    33.8 | 81.593 % |
c |     82135 |   22975    48287 |   24325   25485   894618    35.1 | 81.752 % |
c |     95109 |   22969    48273 |   26758   19203   511484    26.6 | 81.769 % |
c |    114570 |   22969    48273 |   29434   18246   466877    25.6 | 81.769 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12846     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137455 |   43385    96013 |   14461   24890   966876    38.8 | 81.769 % |
c |    137555 |   43385    96013 |   15907   12545   412381    32.9 | 53.716 % |
c |    137705 |   43385    96013 |   17497   12695   419114    33.0 | 53.716 % |
c |    137930 |   43385    96013 |   19247   12920   427539    33.1 | 53.716 % |
c |    138267 |   43385    96013 |   21172   13257   443447    33.5 | 53.716 % |
c |    138775 |   43385    96013 |   23289   13765   459548    33.4 | 53.716 % |
c |    139534 |   43330    95885 |   25618   14518   489011    33.7 | 53.814 % |
c |    140673 |   43330    95885 |   28180   15657   526636    33.6 | 53.814 % |
c |    142381 |   43303    95825 |   30998   17364   586979    33.8 | 53.850 % |
c |    144943 |   43207    95608 |   34098   19918   687613    34.5 | 53.989 % |
c |    148787 |   43207    95608 |   37508   23762   815394    34.3 | 53.989 % |
c |    154554 |   43150    95472 |   41258   29517  1001742    33.9 | 54.103 % |
c |    163203 |   43103    95366 |   45384   38165  1250686    32.8 | 54.170 % |
c |    176177 |   42479    93940 |   49923   51122  1703422    33.3 | 55.138 % |
c |    195639 |   42432    93838 |   54915   25328   652896    25.8 | 55.216 % |
c |    224831 |   42209    93338 |   60407   54502  1893898    34.7 | 55.566 % |
c |    268623 |   41957    92767 |   66447   43906  1668331    38.0 | 55.989 % |
c |    334307 |   41744    92285 |   73092   52501  1525564    29.1 | 56.314 % |
c |    432833 |   41261    91190 |   80401   83434  2599920    31.2 | 57.066 % |
#### 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.88 0.97 0.91 2/54 4306
Raw data (stat): 4306 (runsolver) R 4305 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423521486 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.90 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 1627 0 0 0 995 3 0 0 25 0 1 0 423521486 8572928 1605 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2093 1605 603 41 0 2052 0
vsize: 8372
[startup+20.0016 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 2168 0 0 0 1993 5 0 0 25 0 1 0 423521486 10809344 2146 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2639 2146 603 41 0 2598 0
vsize: 10556
[startup+30.0028 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 2633 0 0 0 2990 7 0 0 25 0 1 0 423521486 12795904 2611 4294967295 134512640 134672761 3221224560 3221223744 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3124 2611 603 41 0 3083 0
vsize: 12496
[startup+40.0026 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 2966 0 0 0 3989 8 0 0 25 0 1 0 423521486 14143488 2944 4294967295 134512640 134672761 3221224560 3221223800 134558237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2944 603 41 0 3412 0
vsize: 13812
[startup+50.0029 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3336 0 0 0 4987 10 0 0 25 0 1 0 423521486 15736832 3314 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3842 3314 603 41 0 3801 0
vsize: 15368
[startup+60.0031 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3567 0 0 0 5986 11 0 0 25 0 1 0 423521486 16674816 3545 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3545 603 41 0 4030 0
vsize: 16284
[startup+70.0049 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3567 0 0 0 6986 11 0 0 25 0 1 0 423521486 16674816 3545 4294967295 134512640 134672761 3221224560 3221223744 134559321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3545 603 41 0 4030 0
vsize: 16284
[startup+80.0052 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3572 0 0 0 7985 12 0 0 25 0 1 0 423521486 16674816 3550 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3550 603 41 0 4030 0
vsize: 16284
[startup+90.0054 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3573 0 0 0 8985 12 0 0 25 0 1 0 423521486 16674816 3551 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3551 603 41 0 4030 0
vsize: 16284
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 9985 12 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3552 603 41 0 4030 0
vsize: 16284
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 10984 13 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3552 603 41 0 4030 0
vsize: 16284
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 11984 13 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3552 603 41 0 4030 0
vsize: 16284
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 12983 14 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3552 603 41 0 4030 0
vsize: 16284
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3580 0 0 0 13983 14 0 0 25 0 1 0 423521486 16674816 3558 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3558 603 41 0 4030 0
vsize: 16284
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3589 0 0 0 14983 14 0 0 25 0 1 0 423521486 16674816 3567 4294967295 134512640 134672761 3221224560 3221223664 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4071 3567 603 41 0 4030 0
vsize: 16284
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3593 0 0 0 15982 15 0 0 25 0 1 0 423521486 16838656 3571 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4111 3571 603 41 0 4070 0
vsize: 16444
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3594 0 0 0 16981 15 0 0 25 0 1 0 423521486 16838656 3572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4111 3572 603 41 0 4070 0
vsize: 16444
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3594 0 0 0 17981 15 0 0 25 0 1 0 423521486 16838656 3572 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4111 3572 603 41 0 4070 0
vsize: 16444
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3594 0 0 0 18981 16 0 0 25 0 1 0 423521486 16838656 3572 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4111 3572 603 41 0 4070 0
vsize: 16444
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 19980 16 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3834 603 41 0 4377 0
vsize: 17672
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 20980 16 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3834 603 41 0 4377 0
vsize: 17672
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 21980 17 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3834 603 41 0 4377 0
vsize: 17672
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 22979 17 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3834 603 41 0 4377 0
vsize: 17672
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 23979 17 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3834 603 41 0 4377 0
vsize: 17672
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3864 0 0 0 24978 18 0 0 25 0 1 0 423521486 18227200 3839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4450 3839 603 41 0 4409 0
vsize: 17800
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4000 0 0 0 25977 18 0 0 25 0 1 0 423521486 18755584 3975 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4579 3975 603 41 0 4538 0
vsize: 18316
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4154 0 0 0 26977 19 0 0 25 0 1 0 423521486 19288064 4129 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4709 4129 603 41 0 4668 0
vsize: 18836
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4305 0 0 0 27976 20 0 0 25 0 1 0 423521486 19951616 4280 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4871 4280 603 41 0 4830 0
vsize: 19484
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4434 0 0 0 28975 21 0 0 25 0 1 0 423521486 20484096 4409 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5001 4409 603 41 0 4960 0
vsize: 20004
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4557 0 0 0 29974 21 0 0 25 0 1 0 423521486 21008384 4532 4294967295 134512640 134672761 3221224560 3221223696 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5129 4532 603 41 0 5088 0
vsize: 20516
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4664 0 0 0 30974 22 0 0 25 0 1 0 423521486 21405696 4639 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5226 4639 603 41 0 5185 0
vsize: 20904
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4774 0 0 0 31973 23 0 0 25 0 1 0 423521486 21803008 4749 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5323 4749 603 41 0 5282 0
vsize: 21292
[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4880 0 0 0 32972 24 0 0 25 0 1 0 423521486 22204416 4855 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5421 4855 603 41 0 5380 0
vsize: 21684
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4941 0 0 0 33971 24 0 0 25 0 1 0 423521486 22466560 4916 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5485 4916 603 41 0 5444 0
vsize: 21940
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4946 0 0 0 34971 25 0 0 25 0 1 0 423521486 22466560 4921 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5485 4921 603 41 0 5444 0
vsize: 21940
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4953 0 0 0 35970 25 0 0 25 0 1 0 423521486 22630400 4928 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4928 603 41 0 5484 0
vsize: 22100
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4953 0 0 0 36970 26 0 0 25 0 1 0 423521486 22630400 4928 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4928 603 41 0 5484 0
vsize: 22100
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4953 0 0 0 37970 26 0 0 25 0 1 0 423521486 22630400 4928 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4928 603 41 0 5484 0
vsize: 22100
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4969 0 0 0 38969 26 0 0 25 0 1 0 423521486 22630400 4944 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4944 603 41 0 5484 0
vsize: 22100
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4970 0 0 0 39969 27 0 0 25 0 1 0 423521486 22630400 4945 4294967295 134512640 134672761 3221224560 3221223560 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4945 603 41 0 5484 0
vsize: 22100
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4972 0 0 0 40968 27 0 0 25 0 1 0 423521486 22630400 4947 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4947 603 41 0 5484 0
vsize: 22100
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4972 0 0 0 41968 27 0 0 25 0 1 0 423521486 22630400 4947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4947 603 41 0 5484 0
vsize: 22100
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4972 0 0 0 42968 28 0 0 25 0 1 0 423521486 22630400 4947 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 4947 603 41 0 5484 0
vsize: 22100
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5105 0 0 0 43967 28 0 0 25 0 1 0 423521486 23158784 5080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5654 5080 603 41 0 5613 0
vsize: 22616
[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5237 0 0 0 44966 29 0 0 25 0 1 0 423521486 23949312 5212 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5847 5212 603 41 0 5806 0
vsize: 23388
[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5351 0 0 0 45965 30 0 0 25 0 1 0 423521486 24481792 5326 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5977 5326 603 41 0 5936 0
vsize: 23908
[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5463 0 0 0 46965 30 0 0 25 0 1 0 423521486 24875008 5438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6073 5438 603 41 0 6032 0
vsize: 24292
[startup+480.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 47965 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223360 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 48964 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 49964 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 50964 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 51963 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+530.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 52963 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 53962 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 54963 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5523 603 41 0 6129 0
vsize: 24680
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5552 0 0 0 55962 33 0 0 25 0 1 0 423521486 25272320 5527 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5527 603 41 0 6129 0
vsize: 24680
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5552 0 0 0 56962 33 0 0 25 0 1 0 423521486 25272320 5527 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5527 603 41 0 6129 0
vsize: 24680
[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5556 0 0 0 57961 33 0 0 25 0 1 0 423521486 25272320 5531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5531 603 41 0 6129 0
vsize: 24680
[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5561 0 0 0 58961 33 0 0 25 0 1 0 423521486 25272320 5536 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5536 603 41 0 6129 0
vsize: 24680
[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5561 0 0 0 59961 34 0 0 25 0 1 0 423521486 25272320 5536 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6170 5536 603 41 0 6129 0
vsize: 24680
[startup+610.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5575 0 0 0 60961 34 0 0 25 0 1 0 423521486 25427968 5550 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6208 5550 603 41 0 6167 0
vsize: 24832
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5657 0 0 0 61960 34 0 0 25 0 1 0 423521486 25694208 5632 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6273 5632 603 41 0 6232 0
vsize: 25092
[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5762 0 0 0 62960 35 0 0 25 0 1 0 423521486 26087424 5737 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6369 5737 603 41 0 6328 0
vsize: 25476
[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5869 0 0 0 63959 36 0 0 25 0 1 0 423521486 26628096 5844 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6501 5844 603 41 0 6460 0
vsize: 26004
[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5970 0 0 0 64958 36 0 0 25 0 1 0 423521486 27021312 5945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5945 603 41 0 6556 0
vsize: 26388
[startup+660.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5980 0 0 0 65957 37 0 0 25 0 1 0 423521486 27021312 5955 4294967295 134512640 134672761 3221224560 3221223744 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5955 603 41 0 6556 0
vsize: 26388
[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5980 0 0 0 66957 37 0 0 25 0 1 0 423521486 27021312 5955 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5955 603 41 0 6556 0
vsize: 26388
[startup+680.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5981 0 0 0 67957 38 0 0 25 0 1 0 423521486 27021312 5956 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5956 603 41 0 6556 0
vsize: 26388
[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5981 0 0 0 68956 38 0 0 25 0 1 0 423521486 27021312 5956 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5956 603 41 0 6556 0
vsize: 26388
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5991 0 0 0 69956 38 0 0 25 0 1 0 423521486 27021312 5966 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5966 603 41 0 6556 0
vsize: 26388
[startup+710.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5992 0 0 0 70956 38 0 0 25 0 1 0 423521486 27021312 5967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5967 603 41 0 6556 0
vsize: 26388
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5992 0 0 0 71956 38 0 0 25 0 1 0 423521486 27021312 5967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5967 603 41 0 6556 0
vsize: 26388
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5993 0 0 0 72956 38 0 0 25 0 1 0 423521486 27021312 5968 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5968 603 41 0 6556 0
vsize: 26388
[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6004 0 0 0 73955 39 0 0 25 0 1 0 423521486 27181056 5979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 5979 603 41 0 6595 0
vsize: 26544
[startup+750.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6005 0 0 0 74955 39 0 0 25 0 1 0 423521486 27181056 5980 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 5980 603 41 0 6595 0
vsize: 26544
[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6017 0 0 0 75954 39 0 0 25 0 1 0 423521486 27181056 5992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 5992 603 41 0 6595 0
vsize: 26544
[startup+770.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6017 0 0 0 76954 39 0 0 25 0 1 0 423521486 27181056 5992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 5992 603 41 0 6595 0
vsize: 26544
[startup+780.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6029 0 0 0 77954 40 0 0 25 0 1 0 423521486 27344896 6004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6004 603 41 0 6635 0
vsize: 26704
[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6030 0 0 0 78954 40 0 0 25 0 1 0 423521486 27344896 6005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6005 603 41 0 6635 0
vsize: 26704
[startup+800.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6032 0 0 0 79954 40 0 0 25 0 1 0 423521486 27344896 6007 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6007 603 41 0 6635 0
vsize: 26704
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6034 0 0 0 80953 40 0 0 25 0 1 0 423521486 27344896 6009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6009 603 41 0 6635 0
vsize: 26704
[startup+820.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6037 0 0 0 81953 40 0 0 25 0 1 0 423521486 27344896 6012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6012 603 41 0 6635 0
vsize: 26704
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6041 0 0 0 82953 41 0 0 25 0 1 0 423521486 27344896 6016 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6016 603 41 0 6635 0
vsize: 26704
[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6043 0 0 0 83953 41 0 0 25 0 1 0 423521486 27344896 6018 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6018 603 41 0 6635 0
vsize: 26704
[startup+850.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 84952 41 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+860.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 85952 42 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+870.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 86952 42 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+880.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 87952 42 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+890.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 88951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223696 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+900.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 89951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+910.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 90951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+920.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 91951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+930.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 92950 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223664 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+940.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 93950 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+950.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 94950 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+960.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 95949 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+970.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 96949 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+980.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 97949 45 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+990.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 98948 45 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6019 603 41 0 6635 0
vsize: 26704
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6054 0 0 0 99948 45 0 0 25 0 1 0 423521486 27344896 6029 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6029 603 41 0 6635 0
vsize: 26704
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6054 0 0 0 100948 46 0 0 25 0 1 0 423521486 27344896 6029 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6029 603 41 0 6635 0
vsize: 26704
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6056 0 0 0 101948 46 0 0 25 0 1 0 423521486 27344896 6031 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6031 603 41 0 6635 0
vsize: 26704
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6057 0 0 0 102947 46 0 0 25 0 1 0 423521486 27344896 6032 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6032 603 41 0 6635 0
vsize: 26704
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6155 0 0 0 103946 47 0 0 25 0 1 0 423521486 27738112 6130 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6772 6130 603 41 0 6731 0
vsize: 27088
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6276 0 0 0 104946 47 0 0 25 0 1 0 423521486 28270592 6251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6251 603 41 0 6861 0
vsize: 27608
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6282 0 0 0 105946 47 0 0 25 0 1 0 423521486 28270592 6257 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6257 603 41 0 6861 0
vsize: 27608
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6285 0 0 0 106946 47 0 0 25 0 1 0 423521486 28270592 6260 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6260 603 41 0 6861 0
vsize: 27608
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6288 0 0 0 107945 48 0 0 25 0 1 0 423521486 28270592 6263 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6263 603 41 0 6861 0
vsize: 27608
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6288 0 0 0 108944 49 0 0 25 0 1 0 423521486 28270592 6263 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6263 603 41 0 6861 0
vsize: 27608
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6294 0 0 0 109944 49 0 0 25 0 1 0 423521486 28270592 6269 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6269 603 41 0 6861 0
vsize: 27608
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6294 0 0 0 110945 49 0 0 25 0 1 0 423521486 28270592 6269 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6269 603 41 0 6861 0
vsize: 27608
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6295 0 0 0 111944 50 0 0 25 0 1 0 423521486 28270592 6270 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6270 603 41 0 6861 0
vsize: 27608
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6299 0 0 0 112944 50 0 0 25 0 1 0 423521486 28270592 6274 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6274 603 41 0 6861 0
vsize: 27608
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6305 0 0 0 113944 51 0 0 25 0 1 0 423521486 28430336 6280 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6280 603 41 0 6900 0
vsize: 27764
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6311 0 0 0 114943 51 0 0 25 0 1 0 423521486 28430336 6286 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6286 603 41 0 6900 0
vsize: 27764
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6311 0 0 0 115943 51 0 0 25 0 1 0 423521486 28430336 6286 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6286 603 41 0 6900 0
vsize: 27764
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6317 0 0 0 116943 51 0 0 25 0 1 0 423521486 28430336 6292 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6292 603 41 0 6900 0
vsize: 27764
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6322 0 0 0 117942 52 0 0 25 0 1 0 423521486 28430336 6297 4294967295 134512640 134672761 3221224560 3221223712 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6297 603 41 0 6900 0
vsize: 27764
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6327 0 0 0 118942 52 0 0 25 0 1 0 423521486 28430336 6302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6302 603 41 0 6900 0
vsize: 27764
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6332 0 0 0 119942 52 0 0 25 0 1 0 423521486 28594176 6307 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6981 6307 603 41 0 6940 0
vsize: 27924
[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4306
Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6346 0 0 0 120941 53 0 0 25 0 1 0 423521486 28594176 6321 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6981 6321 603 41 0 6940 0
vsize: 27924
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4306
Raw data (stat): 4306 (minisat+) Z 4305 30854 30853 0 -1 12 6349 0 0 0 120941 54 0 0 25 0 1 0 423521486 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): 1210.09
CPU time (s): 1209.96
CPU user time (s): 1209.42
CPU system time (s): 0.544917
CPU usage (%): 99.9893
Max. virtual memory (Kb): 27924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####