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/primes-dimacs-cnf/normalized-ii32e1.opb
MD5SUM	33d46caaa6c22613488909eddb5a530f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	162
Optimality of the best value was proved	NO
Number of terms in the objective function	444
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	444
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	444
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.02184
Number of variables	444
Total number of constraints	1408
Number of constraints which are clauses	1408
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	32
Trace number 5495

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 00:10:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3918 boxname=wulflinc15 idbench=158 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  33d46caaa6c22613488909eddb5a530f  /oldhome/oroussel/tmp/wulflinc15/normalized-ii32e1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-ii32e1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-ii32e1.opb
IDLAUNCH: 3918
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        903880 kB
Buffers:         35360 kB
Cached:          74016 kB
SwapCached:       2144 kB
Active:          63248 kB
Inactive:        51140 kB
HighTotal:      131008 kB
HighFree:        53172 kB
LowTotal:       903652 kB
LowFree:        850708 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10844 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:30:52 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3918 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1408 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    1408     6426 |     422       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  444/444          
c |         0 |    1408     6426 |     563       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.075988 s)
c ==============================================================================
c [1mFound solution: 205[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16702     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   21363    53097 |    6408       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13380          
c   -- var.elim.:  2000/13380          
c   -- var.elim.:  3000/13380          
c   -- var.elim.:  4000/13380          
c   -- var.elim.:  5000/13380          
c   -- var.elim.:  6000/13380          
c   -- var.elim.:  7000/13380          
c   -- var.elim.:  8000/13380          
c   -- var.elim.:  9000/13380          
c   -- var.elim.:  10000/13380          
c   -- var.elim.:  11000/13380          
c   -- var.elim.:  12000/13380          
c   -- var.elim.:  13000/13380          
c   -- var.elim.:  13380/13380          
c   -- var.elim.:  1000/6543          
c   -- var.elim.:  2000/6543          
c   -- var.elim.:  3000/6543          
c   -- var.elim.:  4000/6543          
c   -- var.elim.:  5000/6543          
c   -- var.elim.:  6000/6543          
c   -- var.elim.:  6543/6543          
c   -- var.elim.:  1000/3837          
c   -- var.elim.:  2000/3837          
c   -- var.elim.:  3000/3837          
c   -- var.elim.:  3837/3837          
c   -- var.elim.:  1000/2725          
c   -- var.elim.:  2000/2725          
c   -- var.elim.:  2725/2725          
c   -- var.elim.:  1000/1959          
c   -- var.elim.:  1959/1959          
c   -- var.elim.:  841/841          
c   -- var.elim.:  192/192          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  1000/2022          
c   -- var.elim.:  2000/2022          
c   -- var.elim.:  2022/2022          
c   -- var.elim.:  37/37          
c |         0 |    6935    38815 |      --       0       --      -- |     --   | -14428/-14281
c |         0 |    6935    38815 |    2774       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 6.549 s)
c ==============================================================================
c [1mFound solution: 191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        17 |   20697    71694 |    6209       9      294    32.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12671          
c   -- var.elim.:  2000/12671          
c   -- var.elim.:  3000/12671          
c   -- var.elim.:  4000/12671          
c   -- var.elim.:  5000/12671          
c   -- var.elim.:  6000/12671          
c   -- var.elim.:  7000/12671          
c   -- var.elim.:  8000/12671          
c   -- var.elim.:  9000/12671          
c   -- var.elim.:  10000/12671          
c   -- var.elim.:  11000/12671          
c   -- var.elim.:  12000/12671          
c   -- var.elim.:  12671/12671          
c   -- var.elim.:  1000/5995          
c   -- var.elim.:  2000/5995          
c   -- var.elim.:  3000/5995          
c   -- var.elim.:  4000/5995          
c   -- var.elim.:  5000/5995          
c   -- var.elim.:  5995/5995          
c   -- var.elim.:  1000/3556          
c   -- var.elim.:  2000/3556          
c   -- var.elim.:  3000/3556          
c   -- var.elim.:  3556/3556          
c   -- var.elim.:  1000/2566          
c   -- var.elim.:  2000/2566          
c   -- var.elim.:  2566/2566          
c   -- var.elim.:  1000/2041          
c   -- var.elim.:  2000/2041          
c   -- var.elim.:  2041/2041          
c   -- var.elim.:  1000/1505          
c   -- var.elim.:  1505/1505          
c   -- var.elim.:  544/544          
c   -- var.elim.:  62/62          
c   -- subsuming                       
c   -- var.elim.:  669/669          
c |        17 |    6959    40496 |      --       9       --      -- |     --   | -13729/-31179
c |        17 |    6959    40496 |    2783       9      294    32.7 |  0.000 % |
c |       118 |    6959    40496 |    3061     110    22132   201.2 |  3.928 % |
c |       268 |    6908    40198 |    3343     258    54280   210.4 |  4.503 % |
c ==============================================================================
c (current CPU-time: 12.3211 s)
c ==============================================================================
c [1mFound solution: 176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       287 |   20800    74271 |    6239     277    56711   204.7 |  4.503 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12728          
c   -- var.elim.:  2000/12728          
c   -- var.elim.:  3000/12728          
c   -- var.elim.:  4000/12728          
c   -- var.elim.:  5000/12728          
c   -- var.elim.:  6000/12728          
c   -- var.elim.:  7000/12728          
c   -- var.elim.:  8000/12728          
c   -- var.elim.:  9000/12728          
c   -- var.elim.:  10000/12728          
c   -- var.elim.:  11000/12728          
c   -- var.elim.:  12000/12728          
c   -- var.elim.:  12728/12728          
c   -- var.elim.:  1000/6038          
c   -- var.elim.:  2000/6038          
c   -- var.elim.:  3000/6038          
c   -- var.elim.:  4000/6038          
c   -- var.elim.:  5000/6038          
c   -- var.elim.:  6000/6038          
c   -- var.elim.:  6038/6038          
c   -- var.elim.:  1000/3787          
c   -- var.elim.:  2000/3787          
c   -- var.elim.:  3000/3787          
c   -- var.elim.:  3787/3787          
c   -- var.elim.:  1000/2784          
c   -- var.elim.:  2000/2784          
c   -- var.elim.:  2784/2784          
c   -- var.elim.:  1000/2180          
c   -- var.elim.:  2000/2180          
c   -- var.elim.:  2180/2180          
c   -- var.elim.:  1000/1820          
c   -- var.elim.:  1820/1820          
c   -- var.elim.:  1000/1270          
c   -- var.elim.:  1270/1270          
c   -- subsuming                       
c   -- var.elim.:  949/949          
c |       287 |    7009    41816 |      --     277       --      -- |     --   | -13777/-32385
c |       287 |    7009    41816 |    2803     156    10107    64.8 |  4.503 % |
c |       388 |    6971    41502 |    3067     255    28863   113.2 |  5.594 % |
c |       541 |    6945    41327 |    3361     407    65030   159.8 |  5.940 % |
c |       767 |    6917    41140 |    3682     632   121574   192.4 |  6.286 % |
c |      1105 |    6806    40493 |    3985     965   186863   193.6 |  7.794 % |
c |      1611 |    6689    39746 |    4309    1467   285106   194.3 |  9.397 % |
c |      2371 |    6298    37321 |    4462    2211   419612   189.8 | 14.802 % |
c |      3510 |    6181    36581 |    4818    3346   806112   240.9 | 16.342 % |
c |      5223 |    6067    35953 |    5202    5046  1523347   301.9 | 17.851 % |
c |      7785 |    6042    35795 |    5698    5397  2097082   388.6 | 18.165 % |
c ==============================================================================
c (current CPU-time: 34.1388 s)
c ==============================================================================
c [1mFound solution: 163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8047 |   19420    68135 |    5825    5658  2215020   391.5 | 18.165 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11976          
c   -- var.elim.:  2000/11976          
c   -- var.elim.:  3000/11976          
c   -- var.elim.:  4000/11976          
c   -- var.elim.:  5000/11976          
c   -- var.elim.:  6000/11976          
c   -- var.elim.:  7000/11976          
c   -- var.elim.:  8000/11976          
c   -- var.elim.:  9000/11976          
c   -- var.elim.:  10000/11976          
c   -- var.elim.:  11000/11976          
c   -- var.elim.:  11976/11976          
c   -- var.elim.:  1000/5558          
c   -- var.elim.:  2000/5558          
c   -- var.elim.:  3000/5558          
c   -- var.elim.:  4000/5558          
c   -- var.elim.:  5000/5558          
c   -- var.elim.:  5558/5558          
c   -- var.elim.:  1000/3270          
c   -- var.elim.:  2000/3270          
c   -- var.elim.:  3000/3270          
c   -- var.elim.:  3270/3270          
c   -- var.elim.:  1000/2242          
c   -- var.elim.:  2000/2242          
c   -- var.elim.:  2242/2242          
c   -- var.elim.:  1000/1740          
c   -- var.elim.:  1740/1740          
c   -- var.elim.:  1000/1142          
c   -- var.elim.:  1142/1142          
c   -- var.elim.:  615/615          
c   -- var.elim.:  109/109          
c   -- subsuming                       
c   -- var.elim.:  1000/1246          
c   -- var.elim.:  1246/1246          
c   -- var.elim.:  5/5          
c |      8047 |    6149    38448 |      --    5658       --      -- |     --   | -13228/-29600
c |      8047 |    6149    38448 |    2459     869    28818    33.2 | 18.165 % |
c |      8150 |    6120    38255 |    2692     971    51942    53.5 | 24.818 % |
c |      8300 |    6060    37865 |    2933    1118    77423    69.3 | 25.516 % |
c |      8526 |    6029    37658 |    3209    1343   137942   102.7 | 25.895 % |
c |      8864 |    6029    37658 |    3530    1681   257040   152.9 | 25.895 % |
c |      9372 |    5762    34886 |    3711    2177   397583   182.6 | 28.862 % |
c |     10131 |    5556    33583 |    3937    2925   512597   175.2 | 31.539 % |
c |     11270 |    5554    33577 |    4329    4063   796293   196.0 | 31.571 % |
c |     12978 |    5433    32602 |    4658    3912   849587   217.2 | 33.110 % |
c |     15542 |    5168    30291 |    4874    6402  1642119   256.5 | 36.602 % |
c |     19386 |    4990    29038 |    5177    6032  1231746   204.2 | 38.900 % |
c ==============================================================================
c (current CPU-time: 66.7539 s)
c ==============================================================================
c [1mFound solution: 162[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24163 |   10905    42746 |    3271    5807  1338736   230.5 | 38.900 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5941          
c   -- var.elim.:  2000/5941          
c   -- var.elim.:  3000/5941          
c   -- var.elim.:  4000/5941          
c   -- var.elim.:  5000/5941          
c   -- var.elim.:  5941/5941          
c   -- var.elim.:  1000/2321          
c   -- var.elim.:  2000/2321          
c   -- var.elim.:  2321/2321          
c   -- var.elim.:  1000/1515          
c   -- var.elim.:  1515/1515          
c   -- var.elim.:  847/847          
c   -- var.elim.:  552/552          
c   -- var.elim.:  258/258          
c   -- subsuming                       
c   -- var.elim.:  423/423          
c   -- var.elim.:  15/15          
c |     24163 |    4829    27035 |      --    5807       --      -- |     --   | -6008/-15174
c |     24163 |    4829    27035 |    1931    1998    88789    44.4 | 38.900 % |
c |     24265 |    4829    27035 |    2124    2100   100147    47.7 | 45.142 % |
c |     24416 |    4829    27035 |    2337    2251   124829    55.5 | 45.143 % |
c |     24641 |    4829    27035 |    2570    2476   164461    66.4 | 45.142 % |
c |     24978 |    4829    27035 |    2828    2813   209552    74.5 | 45.142 % |
c |     25487 |    4762    26591 |    3067    3319   300173    90.4 | 45.947 % |
c |     26246 |    4762    26591 |    3374    4078   461564   113.2 | 45.947 % |
c |     27387 |    4689    26058 |    3655    3487   510424   146.4 | 46.806 % |
c |     29095 |    4522    25010 |    3877    5180   782513   151.1 | 48.712 % |
c |     31658 |    4426    24261 |    4174    5634   797728   141.6 | 49.705 % |
c |     35503 |    4218    22727 |    4376    5279   739817   140.1 | 52.228 % |
c |     41269 |    4218    22727 |    4813    6504   970925   149.3 | 52.228 % |
c |     49920 |    4218    22727 |    5295    5651   824541   145.9 | 52.228 % |
c |     62895 |    4218    22727 |    5824    5853   783386   133.8 | 52.228 % |
c |     82356 |    4218    22727 |    6407    6418   881384   137.3 | 52.228 % |
c |    111550 |    4218    22727 |    7047    6585   911784   138.5 | 52.228 % |
c |    155339 |    4218    22727 |    7752    6418  1059770   165.1 |#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 2826
Raw data (stat): 2826 (runsolver) R 2825 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421942257 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 2910 0 0 0 981 16 0 0 25 0 1 0 421942257 13647872 2715 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3332 2715 603 41 0 3291 0
vsize: 13328
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 4527 0 0 0 1968 29 0 0 25 0 1 0 421942257 19316736 3858 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4716 3858 603 41 0 4675 0
vsize: 18864
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 6130 0 0 0 2965 32 0 0 25 0 1 0 421942257 25894912 5461 4294967295 134512640 134672761 3221224576 3221223616 134614263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6322 5461 603 41 0 6281 0
vsize: 25288
[startup+40.0037 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 9064 0 0 0 3951 46 0 0 25 0 1 0 421942257 28160000 6114 4294967295 134512640 134672761 3221224576 3221223024 134643532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6875 6114 603 41 0 6834 0
vsize: 27500
[startup+50.0041 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 9091 0 0 0 4951 46 0 0 25 0 1 0 421942257 28082176 6119 4294967295 134512640 134672761 3221224576 3221223760 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6856 6119 603 41 0 6815 0
vsize: 27424
[startup+60.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 9092 0 0 0 5951 46 0 0 25 0 1 0 421942257 28082176 6120 4294967295 134512640 134672761 3221224576 3221223496 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6856 6120 603 41 0 6815 0
vsize: 27424
[startup+70.0049 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 6941 56 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223024 134643483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+80.0046 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 7940 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223720 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+90.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 8940 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 9940 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223616 134612670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 10941 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 11941 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223616 134612578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 12941 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 13941 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 14941 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 15942 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 16942 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 17942 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 18942 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 19942 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 20943 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 21943 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 22943 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 23943 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 24943 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223776 134610703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 25944 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223616 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 26944 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223408 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11492 0 0 0 27944 57 0 0 25 0 1 0 421942257 28254208 6227 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6898 6227 603 41 0 6857 0
vsize: 27592
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11498 0 0 0 28943 57 0 0 25 0 1 0 421942257 28360704 6233 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6924 6233 603 41 0 6883 0
vsize: 27696
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11498 0 0 0 29942 57 0 0 25 0 1 0 421942257 28360704 6233 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6924 6233 603 41 0 6883 0
vsize: 27696
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11498 0 0 0 30942 57 0 0 25 0 1 0 421942257 28278784 6232 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6904 6232 603 41 0 6863 0
vsize: 27616
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11570 0 0 0 31942 57 0 0 25 0 1 0 421942257 28639232 6304 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6992 6304 603 41 0 6951 0
vsize: 27968
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11570 0 0 0 32942 57 0 0 25 0 1 0 421942257 28639232 6304 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6992 6304 603 41 0 6951 0
vsize: 27968
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11570 0 0 0 33943 57 0 0 25 0 1 0 421942257 28639232 6304 4294967295 134512640 134672761 3221224576 3221223616 134612992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6992 6304 603 41 0 6951 0
vsize: 27968
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11590 0 0 0 34943 57 0 0 25 0 1 0 421942257 28733440 6324 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7015 6324 603 41 0 6974 0
vsize: 28060
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11778 0 0 0 35943 58 0 0 25 0 1 0 421942257 29507584 6512 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7204 6512 603 41 0 7163 0
vsize: 28816
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11778 0 0 0 36943 58 0 0 25 0 1 0 421942257 29462528 6512 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7193 6512 603 41 0 7152 0
vsize: 28772
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11778 0 0 0 37943 58 0 0 25 0 1 0 421942257 29462528 6512 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7193 6512 603 41 0 7152 0
vsize: 28772
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11796 0 0 0 38943 58 0 0 25 0 1 0 421942257 29577216 6530 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7221 6530 603 41 0 7180 0
vsize: 28884
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11796 0 0 0 39943 58 0 0 25 0 1 0 421942257 29577216 6530 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7221 6530 603 41 0 7180 0
vsize: 28884
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11796 0 0 0 40943 58 0 0 25 0 1 0 421942257 29569024 6530 4294967295 134512640 134672761 3221224576 3221223616 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7219 6530 603 41 0 7178 0
vsize: 28876
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 11950 0 0 0 41943 58 0 0 25 0 1 0 421942257 30224384 6684 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7379 6684 603 41 0 7338 0
vsize: 29516
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 42941 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 43942 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 44942 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 45942 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 46942 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134613818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 47942 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 48943 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 49943 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 50943 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 51943 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 52943 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 53943 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 54944 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 55944 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134613099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 56944 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 57944 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 58944 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 59944 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 60945 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134613764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 61945 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 62945 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 63945 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 64945 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223616 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 65945 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 66946 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12646 0 0 0 67946 60 0 0 25 0 1 0 421942257 33058816 7380 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7380 603 41 0 8030 0
vsize: 32284
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12658 0 0 0 68946 60 0 0 25 0 1 0 421942257 33058816 7392 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 7392 603 41 0 8030 0
vsize: 32284
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12853 0 0 0 69945 61 0 0 25 0 1 0 421942257 33841152 7587 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8262 7587 603 41 0 8221 0
vsize: 33048
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12853 0 0 0 70946 61 0 0 25 0 1 0 421942257 33841152 7587 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8262 7587 603 41 0 8221 0
vsize: 33048
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12853 0 0 0 71946 61 0 0 25 0 1 0 421942257 33841152 7587 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8262 7587 603 41 0 8221 0
vsize: 33048
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12893 0 0 0 72946 61 0 0 25 0 1 0 421942257 34066432 7627 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8317 7627 603 41 0 8276 0
vsize: 33268
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12893 0 0 0 73946 61 0 0 25 0 1 0 421942257 34066432 7627 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8317 7627 603 41 0 8276 0
vsize: 33268
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 74946 61 0 0 25 0 1 0 421942257 34058240 7628 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 7628 603 41 0 8274 0
vsize: 33260
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 75946 61 0 0 25 0 1 0 421942257 34058240 7628 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 7628 603 41 0 8274 0
vsize: 33260
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 76947 61 0 0 25 0 1 0 421942257 34058240 7628 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 7628 603 41 0 8274 0
vsize: 33260
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 77947 61 0 0 25 0 1 0 421942257 34058240 7628 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 7628 603 41 0 8274 0
vsize: 33260
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 78947 61 0 0 25 0 1 0 421942257 34017280 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7627 603 41 0 8264 0
vsize: 33220
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 79947 61 0 0 25 0 1 0 421942257 34017280 7627 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7627 603 41 0 8264 0
vsize: 33220
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 80947 61 0 0 25 0 1 0 421942257 34017280 7627 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7627 603 41 0 8264 0
vsize: 33220
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 81948 61 0 0 25 0 1 0 421942257 34017280 7627 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7627 603 41 0 8264 0
vsize: 33220
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 82948 61 0 0 25 0 1 0 421942257 34017280 7627 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7627 603 41 0 8264 0
vsize: 33220
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 83948 61 0 0 25 0 1 0 421942257 34017280 7627 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7627 603 41 0 8264 0
vsize: 33220
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 84948 61 0 0 25 0 1 0 421942257 34013184 7627 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7627 603 41 0 8263 0
vsize: 33216
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 85948 61 0 0 25 0 1 0 421942257 34013184 7627 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7627 603 41 0 8263 0
vsize: 33216
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 86949 61 0 0 25 0 1 0 421942257 34009088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8303 7627 603 41 0 8262 0
vsize: 33212
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 87949 61 0 0 25 0 1 0 421942257 34009088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8303 7627 603 41 0 8262 0
vsize: 33212
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 88949 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 89949 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 90949 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 91950 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 92950 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 93950 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 94950 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223728 134565058 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 95950 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 96951 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 97951 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 98951 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 99951 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 100951 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 101952 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 102952 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223616 134612869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 103952 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 104952 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 105952 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 106952 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 107953 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 108953 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 109953 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223616 134612854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 110953 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223616 134612972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 111953 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223824 134618067 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 112954 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223584 134522547 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 113954 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223776 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 114954 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 115954 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 116954 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223816 134610369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 117954 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12894 0 0 0 118955 61 0 0 25 0 1 0 421942257 34004992 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7627 603 41 0 8261 0
vsize: 33208
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2826
Raw data (stat): 2826 (minisat+) R 2825 29151 29150 0 -1 0 12951 0 0 0 119954 62 0 0 25 0 1 0 421942257 34267136 7684 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8366 7684 603 41 0 8325 0
vsize: 33464
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2826
Raw data (stat): 2826 (minisat+) Z 2825 29151 29150 0 -1 12 12952 0 0 0 119955 64 0 0 25 0 1 0 421942257 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.55
CPU system time (s): 0.646901
CPU usage (%): 100.012
Max. virtual memory (Kb): 33464
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####