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/manquinho/routing/normalized-s4-4-3-8pb.opb
MD5SUM	2bf0a3299a380a62e2f4aaf6d6f8fe18
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	36
Optimality of the best value was proved	NO
Number of terms in the objective function	432
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	432
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	432
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	0.903861
Number of variables	432
Total number of constraints	1304
Number of constraints which are clauses	1280
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	18
Trace number 5201

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-13 22:23:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3628 boxname=wulflinc21 idbench=244 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2bf0a3299a380a62e2f4aaf6d6f8fe18  /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-8pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-8pb.opb /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-8pb.opb
IDLAUNCH: 3628
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        907560 kB
Buffers:         26512 kB
Cached:          80792 kB
SwapCached:          0 kB
Active:          33908 kB
Inactive:        76244 kB
HighTotal:      131008 kB
HighFree:        46620 kB
LowTotal:       903652 kB
LowFree:        860940 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11276 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:44:00 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 3628 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1304 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1242]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1232]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1199]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1171]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1161]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1147]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1121]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1099]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1089]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1052]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1030]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1024]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1018]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1008]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 998]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 948]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 946]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 932]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 906]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 884]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 874]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 826]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 816]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 806]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 802]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 758]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 733]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 723]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 713]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 663]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 661]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 643]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 622]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 554]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 520]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 518]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 492]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 474]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 448]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 430]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 408]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 382]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 376]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 366]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 356]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 307]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 305]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 253]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 235]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 182]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 172]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 112]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  94]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  36]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  34]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  22]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  21]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  20]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  19]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  18]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  17]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  16]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  15]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  14]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  13]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  12]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  11]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[  10]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   9]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   8]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   7]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   6]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   5]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   4]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   3]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   2]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   1]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ---[   0]---> Adder-cost: 32   maxlim: 14   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6248    21336 |    2082       0        0     nan |  0.000 % |
c |       102 |    6224    21268 |    2290      98      260     2.7 | 20.900 % |
c |       252 |    6218    21251 |    2519     247      793     3.2 | 20.966 % |
c |       477 |    6191    21169 |    2771     466     2078     4.5 | 21.230 % |
c |       815 |    6155    21056 |    3048     797     4423     5.5 | 21.561 % |
c |      1324 |    6098    20867 |    3353    1286     8956     7.0 | 22.024 % |
c |      2084 |    6044    20700 |    3688    2035    17504     8.6 | 22.553 % |
c |      3223 |    6020    20621 |    4057    3160    37060    11.7 | 22.751 % |
c |      4931 |    6020    20621 |    4462    2619    40359    15.4 | 22.751 % |
c |      7494 |    5945    20375 |    4909    2676    38762    14.5 | 23.413 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 856   maxlim: 372   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10165 |   11879    41559 |    3959    5340   103577    19.4 | 23.413 % |
c |     10265 |   11870    41528 |    4354    2768    41101    14.8 | 15.297 % |
c |     10416 |   11870    41528 |    4790    2919    43435    14.9 | 15.297 % |
c |     10643 |   11870    41528 |    5269    3146    47881    15.2 | 15.297 % |
c |     10981 |   11870    41528 |    5796    3484    55156    15.8 | 15.297 % |
c |     11487 |   11864    41511 |    6376    3989    65441    16.4 | 15.339 % |
c |     12248 |   11864    41511 |    7013    4750    80945    17.0 | 15.339 % |
c |     13388 |   11864    41511 |    7714    5890    97303    16.5 | 15.339 % |
c |     15097 |   11857    41488 |    8486    7595   128247    16.9 | 15.381 % |
c |     17660 |   11848    41457 |    9335    5664    94355    16.7 | 15.424 % |
c |     21505 |   11822    41370 |   10268    9498   174324    18.4 | 15.592 % |
c |     27272 |   11810    41330 |   11295    9925   205569    20.7 | 15.676 % |
c |     35922 |   11801    41299 |   12425    6537   155034    23.7 | 15.719 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 374   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40513 |   11799    41302 |    3933   11126   405510    36.4 | 15.719 % |
c |     40615 |   11799    41302 |    4326    2884   103078    35.7 | 15.832 % |
c |     40766 |   11799    41302 |    4758    3035   104104    34.3 | 15.832 % |
c |     40991 |   11799    41302 |    5234    3260   105910    32.5 | 15.832 % |
c |     41329 |   11799    41302 |    5758    3598   110233    30.6 | 15.832 % |
c |     41837 |   11799    41302 |    6334    4106   121179    29.5 | 15.832 % |
c |     42597 |   11799    41302 |    6967    4866   131118    26.9 | 15.832 % |
c |     43736 |   11799    41302 |    7664    6005   157447    26.2 | 15.832 % |
c |     45445 |   11799    41302 |    8430    7714   205789    26.7 | 15.832 % |
c |     48007 |   11787    41262 |    9273    5714   120096    21.0 | 15.916 % |
c |     51852 |   11781    41242 |   10201    9557   232419    24.3 | 15.958 % |
c ==============================================================================
c [1mFound solution: 56[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 376   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54838 |   11785    41263 |    3928    6881   202920    29.5 | 15.958 % |
c |     54938 |   11785    41263 |    4320    3541    80236    22.7 | 16.029 % |
c |     55088 |   11785    41263 |    4752    3691    81403    22.1 | 16.029 % |
c |     55313 |   11785    41263 |    5228    3916    83607    21.4 | 16.029 % |
c |     55651 |   11785    41263 |    5750    4254    90436    21.3 | 16.029 % |
c |     56161 |   11785    41263 |    6326    4764    99120    20.8 | 16.029 % |
c |     56921 |   11785    41263 |    6958    5524   120276    21.8 | 16.029 % |
c |     58061 |   11785    41263 |    7654    6664   136535    20.5 | 16.029 % |
c |     59769 |   11785    41263 |    8420    4292    62731    14.6 | 16.029 % |
c |     62333 |   11785    41263 |    9262    6856   136788    20.0 | 16.029 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 378   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64137 |   11787    41280 |    3929    8660   184816    21.3 | 16.029 % |
c |     64238 |   11787    41280 |    4321    2266    29388    13.0 | 16.099 % |
c |     64388 |   11787    41280 |    4754    2416    31105    12.9 | 16.099 % |
c |     64614 |   11787    41280 |    5229    2642    36257    13.7 | 16.099 % |
c |     64951 |   11787    41280 |    5752    2978    43655    14.7 | 16.141 % |
c |     65458 |   11781    41260 |    6327    3483    56325    16.2 | 16.142 % |
c |     66219 |   11781    41260 |    6960    4244    75790    17.9 | 16.141 % |
c |     67358 |   11781    41260 |    7656    5383   100920    18.7 | 16.141 % |
c |     69066 |   11781    41260 |    8422    7091   139978    19.7 | 16.141 % |
c |     71628 |   11781    41260 |    9264    5232    89264    17.1 | 16.141 % |
c |     75477 |   11781    41260 |   10190    9081   163774    18.0 | 16.141 % |
c |     81243 |   11781    41260 |   11209    9538   168507    17.7 | 16.141 % |
c |     89892 |   11772    41229 |   12330    6436   114318    17.8 | 16.183 % |
c |    102866 |   11772    41229 |   13563   12435   839417    67.5 | 16.183 % |
c |    122328 |   11772    41229 |   14920    9937   703372    70.8 | 16.183 % |
c |    151522 |   11772    41229 |   16412    8317   157540    18.9 | 16.183 % |
c |    195311 |   11772    41229 |   18053   17315   863963    49.9 | 16.183 % |
c |    260997 |   11772    41229 |   19859   16862  1111175    65.9 | 16.183 % |
c |    359523 |   11760    41192 |   21844   12598   556186    44.1 | 16.267 % |
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    399975 |   11763    41210 |    3921   19200   975098    50.8 | 16.267 % |
c |    400076 |   11763    41210 |    4313    2501    48073    19.2 | 16.331 % |
c |    400226 |   11763    41210 |    4744    2651    49947    18.8 | 16.331 % |
c |    400452 |   11763    41210 |    5218    2877    54414    18.9 | 16.331 % |
c |    400789 |   11763    41210 |    5740    3214    61128    19.0 | 16.331 % |
c |    401296 |   11763    41210 |    6314    3721    73142    19.7 | 16.331 % |
c |    402056 |   11763    41210 |    6946    4481    90945    20.3 | 16.331 % |
c |    403196 |   11763    41210 |    7640    5621   118009    21.0 | 16.331 % |
c |    404906 |   11763    41210 |    8405    7331   152983    20.9 | 16.331 % |
c |    407470 |   11763    41210 |    9245    5474    92370    16.9 | 16.331 % |
c |    411316 |   11763    41210 |   10170    9320   154126    16.5 | 16.331 % |
c |    417082 |   11763    41210 |   11187    9786   184165    18.8 | 16.331 % |
c |    425734 |   11763    41210 |   12305    6645   258511    38.9 | 16.331 % |
c |    438708 |   11763    41210 |   13536    6601   193641    29.3 | 16.331 % |
c |    458170 |   11763    41210 |   14889   11657   645891    55.4 | 16.331 % |
c |    487363 |   11757    41190 |   16378    9729   430429    44.2 | 16.373 % |
c |    531152 |   11751    41170 |   18016   10491   616824    58.8 | 16.415 % |
c |    596838 |   11751    41170 |   19818   10646   435259    40.9 | 16.415 % |
c |    695367 |   11751    41170 |   21800   16485   706345    42.8 | 16.415 % |
c |    843157 |   11751    41170 |   23980   17995   899821    50.0 | 16.415 % |
c |   1064840 |   11751    41170 |   26378   17291   815213    47.1 | 16.415 % |
#### 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.84 0.95 0.90 2/55 2134
Raw data (stat): 2134 (runsolver) D 2133 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 356788547 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 1001 0 0 0 996 3 0 0 25 0 1 0 356788547 5742592 979 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1402 979 603 41 0 1361 0
vsize: 5608
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.95 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 1162 0 0 0 1995 4 0 0 25 0 1 0 356788547 6414336 1140 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1566 1140 603 41 0 1525 0
vsize: 6264
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.95 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 1440 0 0 0 2994 5 0 0 25 0 1 0 356788547 7491584 1418 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1829 1418 603 41 0 1788 0
vsize: 7316
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.95 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 1855 0 0 0 3993 6 0 0 25 0 1 0 356788547 9228288 1833 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1833 603 41 0 2212 0
vsize: 9012
[startup+50.003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2192 0 0 0 4992 7 0 0 25 0 1 0 356788547 10567680 2170 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2170 603 41 0 2539 0
vsize: 10320
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2193 0 0 0 5992 7 0 0 25 0 1 0 356788547 10567680 2171 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2171 603 41 0 2539 0
vsize: 10320
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2212 0 0 0 6992 8 0 0 25 0 1 0 356788547 10784768 2190 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2190 603 41 0 2592 0
vsize: 10532
[startup+80.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2212 0 0 0 7992 8 0 0 25 0 1 0 356788547 10784768 2190 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2190 603 41 0 2592 0
vsize: 10532
[startup+90.0047 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2212 0 0 0 8992 8 0 0 25 0 1 0 356788547 10784768 2190 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2190 603 41 0 2592 0
vsize: 10532
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2212 0 0 0 9992 8 0 0 25 0 1 0 356788547 10784768 2190 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2190 603 41 0 2592 0
vsize: 10532
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2323 0 0 0 10991 9 0 0 25 0 1 0 356788547 11190272 2301 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2301 603 41 0 2691 0
vsize: 10928
[startup+120.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2332 0 0 0 11991 9 0 0 25 0 1 0 356788547 11190272 2310 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2310 603 41 0 2691 0
vsize: 10928
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2363 0 0 0 12991 9 0 0 25 0 1 0 356788547 11325440 2341 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2765 2341 603 41 0 2724 0
vsize: 11060
[startup+140.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2380 0 0 0 13991 10 0 0 25 0 1 0 356788547 11460608 2358 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2358 603 41 0 2757 0
vsize: 11192
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2411 0 0 0 14991 10 0 0 25 0 1 0 356788547 11591680 2389 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2830 2389 603 41 0 2789 0
vsize: 11320
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2797 0 0 0 15989 11 0 0 25 0 1 0 356788547 13213696 2775 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3226 2775 603 41 0 3185 0
vsize: 12904
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2823 0 0 0 16990 11 0 0 25 0 1 0 356788547 13213696 2801 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3226 2801 603 41 0 3185 0
vsize: 12904
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2823 0 0 0 17990 11 0 0 25 0 1 0 356788547 13213696 2801 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3226 2801 603 41 0 3185 0
vsize: 12904
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2829 0 0 0 18990 11 0 0 25 0 1 0 356788547 13352960 2807 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2807 603 41 0 3219 0
vsize: 13040
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2829 0 0 0 19990 12 0 0 25 0 1 0 356788547 13352960 2807 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2807 603 41 0 3219 0
vsize: 13040
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2829 0 0 0 20990 12 0 0 25 0 1 0 356788547 13352960 2807 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2807 603 41 0 3219 0
vsize: 13040
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2851 0 0 0 21989 12 0 0 25 0 1 0 356788547 13352960 2829 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2829 603 41 0 3219 0
vsize: 13040
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2854 0 0 0 22990 12 0 0 25 0 1 0 356788547 13352960 2832 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2832 603 41 0 3219 0
vsize: 13040
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2854 0 0 0 23990 12 0 0 25 0 1 0 356788547 13352960 2832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2832 603 41 0 3219 0
vsize: 13040
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2863 0 0 0 24990 13 0 0 25 0 1 0 356788547 13492224 2841 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3294 2841 603 41 0 3253 0
vsize: 13176
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2875 0 0 0 25989 13 0 0 25 0 1 0 356788547 13492224 2853 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3294 2853 603 41 0 3253 0
vsize: 13176
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2893 0 0 0 26989 13 0 0 25 0 1 0 356788547 13639680 2871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3330 2871 603 41 0 3289 0
vsize: 13320
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2899 0 0 0 27989 13 0 0 25 0 1 0 356788547 13639680 2877 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3330 2877 603 41 0 3289 0
vsize: 13320
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2922 0 0 0 28989 14 0 0 25 0 1 0 356788547 13799424 2900 4294967295 134512640 134672761 3221224560 3221223744 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3369 2900 603 41 0 3328 0
vsize: 13476
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2924 0 0 0 29989 14 0 0 25 0 1 0 356788547 13799424 2902 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3369 2902 603 41 0 3328 0
vsize: 13476
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2930 0 0 0 30989 14 0 0 25 0 1 0 356788547 13799424 2908 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3369 2908 603 41 0 3328 0
vsize: 13476
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2956 0 0 0 31989 14 0 0 25 0 1 0 356788547 13946880 2934 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3405 2934 603 41 0 3364 0
vsize: 13620
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 32989 14 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 33989 14 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 34989 14 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 35989 14 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 36989 15 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 37989 15 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 38989 15 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 39989 15 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223744 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2975 0 0 0 40989 15 0 0 25 0 1 0 356788547 13946880 2953 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2953 603 41 0 3364 0
vsize: 13620
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2981 0 0 0 41989 15 0 0 25 0 1 0 356788547 13946880 2959 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2959 603 41 0 3364 0
vsize: 13620
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2982 0 0 0 42989 15 0 0 25 0 1 0 356788547 13946880 2960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2960 603 41 0 3364 0
vsize: 13620
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2987 0 0 0 43989 16 0 0 25 0 1 0 356788547 14110720 2965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3445 2965 603 41 0 3404 0
vsize: 13780
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2995 0 0 0 44989 16 0 0 25 0 1 0 356788547 14110720 2973 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3445 2973 603 41 0 3404 0
vsize: 13780
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 2995 0 0 0 45989 16 0 0 25 0 1 0 356788547 14110720 2973 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3445 2973 603 41 0 3404 0
vsize: 13780
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3007 0 0 0 46989 16 0 0 25 0 1 0 356788547 14110720 2985 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3445 2985 603 41 0 3404 0
vsize: 13780
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3170 0 0 0 47989 17 0 0 25 0 1 0 356788547 14786560 3148 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3610 3148 603 41 0 3569 0
vsize: 14440
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3213 0 0 0 48988 17 0 0 25 0 1 0 356788547 15085568 3191 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3191 603 41 0 3642 0
vsize: 14732
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3218 0 0 0 49988 17 0 0 25 0 1 0 356788547 15085568 3196 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3196 603 41 0 3642 0
vsize: 14732
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3228 0 0 0 50988 17 0 0 25 0 1 0 356788547 15085568 3206 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3206 603 41 0 3642 0
vsize: 14732
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3243 0 0 0 51988 18 0 0 25 0 1 0 356788547 15249408 3221 4294967295 134512640 134672761 3221224560 3221223744 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3221 603 41 0 3682 0
vsize: 14892
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3249 0 0 0 52988 18 0 0 25 0 1 0 356788547 15249408 3227 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3227 603 41 0 3682 0
vsize: 14892
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3250 0 0 0 53989 18 0 0 25 0 1 0 356788547 15249408 3228 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3228 603 41 0 3682 0
vsize: 14892
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3267 0 0 0 54988 18 0 0 25 0 1 0 356788547 15249408 3245 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3245 603 41 0 3682 0
vsize: 14892
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3273 0 0 0 55988 18 0 0 25 0 1 0 356788547 15413248 3251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3251 603 41 0 3722 0
vsize: 15052
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3273 0 0 0 56988 18 0 0 25 0 1 0 356788547 15413248 3251 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3251 603 41 0 3722 0
vsize: 15052
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3280 0 0 0 57988 18 0 0 25 0 1 0 356788547 15413248 3258 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3258 603 41 0 3722 0
vsize: 15052
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3330 0 0 0 58988 19 0 0 25 0 1 0 356788547 15544320 3308 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3795 3308 603 41 0 3754 0
vsize: 15180
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3342 0 0 0 59988 19 0 0 25 0 1 0 356788547 15679488 3320 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3828 3320 603 41 0 3787 0
vsize: 15312
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3353 0 0 0 60988 19 0 0 25 0 1 0 356788547 15679488 3331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3828 3331 603 41 0 3787 0
vsize: 15312
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3364 0 0 0 61988 19 0 0 25 0 1 0 356788547 15843328 3342 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3868 3342 603 41 0 3827 0
vsize: 15472
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3387 0 0 0 62988 19 0 0 25 0 1 0 356788547 15843328 3365 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3868 3365 603 41 0 3827 0
vsize: 15472
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3402 0 0 0 63988 19 0 0 25 0 1 0 356788547 15990784 3380 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3904 3380 603 41 0 3863 0
vsize: 15616
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3404 0 0 0 64988 20 0 0 25 0 1 0 356788547 15990784 3382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3904 3382 603 41 0 3863 0
vsize: 15616
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3415 0 0 0 65988 20 0 0 25 0 1 0 356788547 15990784 3393 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3904 3393 603 41 0 3863 0
vsize: 15616
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3445 0 0 0 66988 20 0 0 25 0 1 0 356788547 16138240 3423 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3423 603 41 0 3899 0
vsize: 15760
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3446 0 0 0 67988 20 0 0 25 0 1 0 356788547 16138240 3424 4294967295 134512640 134672761 3221224560 3221223656 1075347118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3424 603 41 0 3899 0
vsize: 15760
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3450 0 0 0 68988 20 0 0 25 0 1 0 356788547 16285696 3428 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3976 3428 603 41 0 3935 0
vsize: 15904
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3464 0 0 0 69988 21 0 0 25 0 1 0 356788547 16285696 3442 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3976 3442 603 41 0 3935 0
vsize: 15904
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3465 0 0 0 70988 21 0 0 25 0 1 0 356788547 16285696 3443 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3976 3443 603 41 0 3935 0
vsize: 15904
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3475 0 0 0 71988 21 0 0 25 0 1 0 356788547 16285696 3453 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3976 3453 603 41 0 3935 0
vsize: 15904
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3491 0 0 0 72988 21 0 0 25 0 1 0 356788547 16433152 3469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4012 3469 603 41 0 3971 0
vsize: 16048
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3496 0 0 0 73988 21 0 0 25 0 1 0 356788547 16433152 3474 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4012 3474 603 41 0 3971 0
vsize: 16048
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3507 0 0 0 74988 21 0 0 25 0 1 0 356788547 16433152 3485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4012 3485 603 41 0 3971 0
vsize: 16048
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3518 0 0 0 75988 21 0 0 25 0 1 0 356788547 16580608 3496 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4048 3496 603 41 0 4007 0
vsize: 16192
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3597 0 0 0 76988 22 0 0 25 0 1 0 356788547 16846848 3575 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3575 603 41 0 4072 0
vsize: 16452
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3666 0 0 0 77988 22 0 0 25 0 1 0 356788547 17113088 3644 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4178 3644 603 41 0 4137 0
vsize: 16712
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3690 0 0 0 78988 22 0 0 25 0 1 0 356788547 17248256 3668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4211 3668 603 41 0 4170 0
vsize: 16844
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3698 0 0 0 79988 22 0 0 25 0 1 0 356788547 17248256 3676 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4211 3676 603 41 0 4170 0
vsize: 16844
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3710 0 0 0 80988 22 0 0 25 0 1 0 356788547 17391616 3688 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4246 3688 603 41 0 4205 0
vsize: 16984
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3724 0 0 0 81988 22 0 0 25 0 1 0 356788547 17391616 3702 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4246 3702 603 41 0 4205 0
vsize: 16984
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3729 0 0 0 82988 22 0 0 25 0 1 0 356788547 17391616 3707 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4246 3707 603 41 0 4205 0
vsize: 16984
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3730 0 0 0 83988 22 0 0 25 0 1 0 356788547 17391616 3708 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4246 3708 603 41 0 4205 0
vsize: 16984
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3746 0 0 0 84988 23 0 0 25 0 1 0 356788547 17588224 3724 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3724 603 41 0 4253 0
vsize: 17176
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3746 0 0 0 85988 23 0 0 25 0 1 0 356788547 17588224 3724 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3724 603 41 0 4253 0
vsize: 17176
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3757 0 0 0 86988 23 0 0 25 0 1 0 356788547 17588224 3735 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3735 603 41 0 4253 0
vsize: 17176
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3757 0 0 0 87988 23 0 0 25 0 1 0 356788547 17588224 3735 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3735 603 41 0 4253 0
vsize: 17176
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3763 0 0 0 88988 23 0 0 25 0 1 0 356788547 17588224 3741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3741 603 41 0 4253 0
vsize: 17176
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3763 0 0 0 89988 23 0 0 25 0 1 0 356788547 17588224 3741 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3741 603 41 0 4253 0
vsize: 17176
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3763 0 0 0 90988 24 0 0 25 0 1 0 356788547 17588224 3741 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3741 603 41 0 4253 0
vsize: 17176
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3771 0 0 0 91988 24 0 0 25 0 1 0 356788547 17588224 3749 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4294 3749 603 41 0 4253 0
vsize: 17176
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3780 0 0 0 92988 24 0 0 25 0 1 0 356788547 17752064 3758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3758 603 41 0 4293 0
vsize: 17336
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3783 0 0 0 93988 24 0 0 25 0 1 0 356788547 17752064 3761 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3761 603 41 0 4293 0
vsize: 17336
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3791 0 0 0 94988 24 0 0 25 0 1 0 356788547 17752064 3769 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3769 603 41 0 4293 0
vsize: 17336
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3791 0 0 0 95988 24 0 0 25 0 1 0 356788547 17752064 3769 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4334 3769 603 41 0 4293 0
vsize: 17336
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3808 0 0 0 96988 25 0 0 25 0 1 0 356788547 17915904 3786 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3786 603 41 0 4333 0
vsize: 17496
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3808 0 0 0 97988 25 0 0 25 0 1 0 356788547 17915904 3786 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3786 603 41 0 4333 0
vsize: 17496
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3817 0 0 0 98987 25 0 0 25 0 1 0 356788547 17915904 3795 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3795 603 41 0 4333 0
vsize: 17496
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3827 0 0 0 99987 25 0 0 25 0 1 0 356788547 17915904 3805 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3805 603 41 0 4333 0
vsize: 17496
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3831 0 0 0 100987 26 0 0 25 0 1 0 356788547 17915904 3809 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3809 603 41 0 4333 0
vsize: 17496
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3834 0 0 0 101987 26 0 0 25 0 1 0 356788547 17915904 3812 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3812 603 41 0 4333 0
vsize: 17496
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3845 0 0 0 102987 26 0 0 25 0 1 0 356788547 18112512 3823 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4422 3823 603 41 0 4381 0
vsize: 17688
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3846 0 0 0 103987 26 0 0 25 0 1 0 356788547 18112512 3824 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4422 3824 603 41 0 4381 0
vsize: 17688
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3846 0 0 0 104987 26 0 0 25 0 1 0 356788547 18112512 3824 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4422 3824 603 41 0 4381 0
vsize: 17688
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3846 0 0 0 105987 27 0 0 25 0 1 0 356788547 18112512 3824 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4422 3824 603 41 0 4381 0
vsize: 17688
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3951 0 0 0 106986 27 0 0 25 0 1 0 356788547 18513920 3929 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4520 3929 603 41 0 4479 0
vsize: 18080
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3958 0 0 0 107986 27 0 0 25 0 1 0 356788547 18513920 3936 4294967295 134512640 134672761 3221224560 3221223712 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4520 3936 603 41 0 4479 0
vsize: 18080
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3974 0 0 0 108986 28 0 0 25 0 1 0 356788547 18653184 3952 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3952 603 41 0 4513 0
vsize: 18216
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3974 0 0 0 109986 28 0 0 25 0 1 0 356788547 18653184 3952 4294967295 134512640 134672761 3221224560 3221223664 134555084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3952 603 41 0 4513 0
vsize: 18216
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3974 0 0 0 110986 28 0 0 25 0 1 0 356788547 18653184 3952 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3952 603 41 0 4513 0
vsize: 18216
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3974 0 0 0 111986 28 0 0 25 0 1 0 356788547 18653184 3952 4294967295 134512640 134672761 3221224560 3221223664 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3952 603 41 0 4513 0
vsize: 18216
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3974 0 0 0 112986 28 0 0 25 0 1 0 356788547 18653184 3952 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3952 603 41 0 4513 0
vsize: 18216
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3980 0 0 0 113986 29 0 0 25 0 1 0 356788547 18653184 3958 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3958 603 41 0 4513 0
vsize: 18216
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 3996 0 0 0 114986 29 0 0 25 0 1 0 356788547 18653184 3974 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3974 603 41 0 4513 0
vsize: 18216
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 4009 0 0 0 115986 29 0 0 25 0 1 0 356788547 18825216 3987 4294967295 134512640 134672761 3221224560 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4596 3987 603 41 0 4555 0
vsize: 18384
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 4056 0 0 0 116986 29 0 0 25 0 1 0 356788547 18956288 4034 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4628 4034 603 41 0 4587 0
vsize: 18512
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 4061 0 0 0 117985 30 0 0 25 0 1 0 356788547 18956288 4039 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4628 4039 603 41 0 4587 0
vsize: 18512
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 4067 0 0 0 118985 30 0 0 25 0 1 0 356788547 19107840 4045 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4665 4045 603 41 0 4624 0
vsize: 18660
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2134
Raw data (stat): 2134 (minisat+) R 2133 30927 30926 0 -1 0 4067 0 0 0 119985 30 0 0 25 0 1 0 356788547 19107840 4045 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4665 4045 603 41 0 4624 0
vsize: 18660
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 2134
Raw data (stat): 2134 (minisat+) Z 2133 30927 30926 0 -1 12 4070 0 0 0 119985 31 0 0 25 0 1 0 356788547 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.17
CPU user time (s): 1199.86
CPU system time (s): 0.314952
CPU usage (%): 100.011
Max. virtual memory (Kb): 18660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####