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/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb
MD5SUM	f88781e3d6e9a5487d13eaa213c27b55
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4272
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	205
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	105
Trace number 14702

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 00:51:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19485 boxname=wulflinc15 idbench=1499 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1_1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 19485
/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:        740988 kB
Buffers:         33720 kB
Cached:         236016 kB
SwapCached:       2060 kB
Active:         115444 kB
Inactive:       159060 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        740736 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13416 kB
Committed_AS:    63516 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:12:02 (client local time) WITH STATUS 10 IN 1200.45 SECONDS
stats: 19485 7 1200.45 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Adder-cost: 554   maxlim: 438520   bits: 20/19
c ---[   8]---> Adder-cost: 562   maxlim: 469716   bits: 20/19
c ---[   6]---> Adder-cost: 644   maxlim: 485238   bits: 20/19
c ---[   4]---> Adder-cost: 446   maxlim: 425237   bits: 20/19
c ---[   2]---> Adder-cost: 494   maxlim: 433357   bits: 20/19
c ---[   0]---> Adder-cost: 474   maxlim: 432725   bits: 20/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   21948    78939 |    6584       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3252          
c   -- var.elim.:  2000/3252          
c   -- var.elim.:  3000/3252          
c   -- var.elim.:  3252/3252          
c   -- var.elim.:  335/335          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  106/106          
c |         0 |   21058    74687 |      --       0       --      -- |     --   | -416/-1259
c |         0 |   21058    74687 |    8423       0        0     nan |  0.000 % |
c |       100 |   21058    74687 |    9265     100      474     4.7 |  7.957 % |
c |       251 |   21058    74687 |   10192     251     4605    18.3 |  7.957 % |
c ==============================================================================
c (current CPU-time: 0.764883 s)
c ==============================================================================
c [1mFound solution: 704990[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       466 |   24770    83354 |    7430     466     7488    16.1 |  7.957 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1397          
c   -- var.elim.:  1397/1397          
c   -- var.elim.:  767/767          
c   -- var.elim.:  13/13          
c   -- subsuming                       
c   -- var.elim.:  218/218          
c   -- var.elim.:  78/78          
c |       466 |   24206    84520 |      --     466       --      -- |     --   | -564/1167
c |       466 |   24206    84520 |    9682     466     7488    16.1 |  7.957 % |
c ==============================================================================
c (current CPU-time: 1.03484 s)
c ==============================================================================
c [1mFound solution: 514457[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       524 |   24394    85048 |    7318     524     7903    15.1 |  7.957 % |
c   -- subsuming                       
c   -- var.elim.:  423/423          
c   -- var.elim.:  200/200          
c |       524 |   24287    85189 |      --     524       --      -- |     --   | -107/142
c |       524 |   24287    85189 |    9714     524     7903    15.1 |  7.957 % |
c ==============================================================================
c (current CPU-time: 1.15182 s)
c ==============================================================================
c [1mFound solution: 321680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       564 |   24384    85480 |    7315     564     8275    14.7 |  7.957 % |
c   -- subsuming                       
c   -- var.elim.:  202/202          
c   -- var.elim.:  135/135          
c |       564 |   24334    85649 |      --     564       --      -- |     --   | -50/170
c |       564 |   24334    85649 |    9733     564     8275    14.7 |  7.957 % |
c |       664 |   24334    85649 |   10706     664    11441    17.2 |  6.711 % |
c |       814 |   24334    85649 |   11777     814    16489    20.3 |  6.711 % |
c |      1039 |   24334    85649 |   12955    1039    19819    19.1 |  6.711 % |
c |      1376 |   24334    85649 |   14250    1376    56643    41.2 |  6.711 % |
c |      1882 |   24334    85649 |   15676    1882    67800    36.0 |  6.711 % |
c ==============================================================================
c (current CPU-time: 2.11768 s)
c ==============================================================================
c [1mFound solution: 268848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1956 |   24416    85890 |    7324    1956    70737    36.2 |  6.711 % |
c   -- subsuming                       
c   -- var.elim.:  159/159          
c   -- var.elim.:  113/113          
c |      1956 |   24376    85971 |      --    1956       --      -- |     --   | -40/82
c |      1956 |   24376    85971 |    9750    1956    70737    36.2 |  6.711 % |
c |      2059 |   24376    85971 |   10725    2059    72658    35.3 |  6.729 % |
c |      2209 |   24376    85971 |   11797    2209    73651    33.3 |  6.729 % |
c |      2435 |   24376    85971 |   12977    2435    76363    31.4 |  6.729 % |
c |      2773 |   24376    85971 |   14275    2773   121358    43.8 |  6.729 % |
c |      3280 |   24376    85971 |   15703    3280   149641    45.6 |  6.729 % |
c |      4039 |   24376    85971 |   17273    4039   169407    41.9 |  6.729 % |
c |      5183 |   24376    85971 |   19000    5183   195483    37.7 |  6.729 % |
c ==============================================================================
c (current CPU-time: 4.23536 s)
c ==============================================================================
c [1mFound solution: 219088[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5502 |   24454    86207 |    7336    5502   200496    36.4 |  6.729 % |
c   -- subsuming                       
c   -- var.elim.:  156/156          
c   -- var.elim.:  110/110          
c |      5502 |   24412    86263 |      --    5502       --      -- |     --   | -42/57
c |      5502 |   24412    86263 |    9764    5502   200496    36.4 |  6.729 % |
c |      5602 |   24412    86263 |   10741    5602   204180    36.4 |  6.740 % |
c |      5752 |   24412    86263 |   11815    5752   215267    37.4 |  6.740 % |
c |      5978 |   24412    86263 |   12996    5978   218142    36.5 |  6.740 % |
c |      6319 |   24412    86263 |   14296    6319   226725    35.9 |  6.740 % |
c |      6825 |   24412    86263 |   15726    6825   248999    36.5 |  6.740 % |
c |      7585 |   24412    86263 |   17298    7585   306491    40.4 |  6.740 % |
c |      8725 |   24412    86263 |   19028    8725   437992    50.2 |  6.740 % |
c |     10433 |   24412    86263 |   20931   10433   507720    48.7 |  6.740 % |
c |     12996 |   24412    86263 |   23024   12996   617035    47.5 |  6.740 % |
c ==============================================================================
c (current CPU-time: 10.9853 s)
c ==============================================================================
c [1mFound solution: 186619[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14702 |   24449    86388 |    7334   14702   694308    47.2 |  6.740 % |
c   -- subsuming                       
c   -- var.elim.:  85/85          
c   -- var.elim.:  65/65          
c |     14702 |   24428    86453 |      --   14702       --      -- |     --   | -21/66
c |     14702 |   24428    86453 |    9771   14702   694308    47.2 |  6.740 % |
c |     14802 |   24428    86453 |   10748    9902   477283    48.2 |  6.758 % |
c |     14952 |   24428    86453 |   11823   10052   481495    47.9 |  6.758 % |
c |     15179 |   24428    86453 |   13005   10279   488278    47.5 |  6.758 % |
c |     15516 |   24421    86429 |   14301   10614   503310    47.4 |  6.782 % |
c |     16023 |   24421    86429 |   15732   11121   513346    46.2 |  6.782 % |
c ==============================================================================
c (current CPU-time: 13.5379 s)
c ==============================================================================
c [1mFound solution: 155072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16360 |   24469    86597 |    7340   11458   566076    49.4 |  6.782 % |
c   -- subsuming                       
c   -- var.elim.:  132/132          
c   -- var.elim.:  91/91          
c |     16360 |   24442    86704 |      --   11458       --      -- |     --   | -27/108
c |     16360 |   24442    86704 |    9776   11458   566076    49.4 |  6.782 % |
c |     16461 |   24435    86622 |   10751    7739   296158    38.3 |  6.824 % |
c |     16611 |   24435    86622 |   11826    7889   300603    38.1 |  6.824 % |
c |     16836 |   24435    86622 |   13009    8114   306911    37.8 |  6.824 % |
c |     17174 |   24435    86622 |   14310    8452   319091    37.8 |  6.824 % |
c |     17681 |   24435    86622 |   15741    8959   336758    37.6 |  6.824 % |
c |     18441 |   24435    86622 |   17315    9719   363930    37.4 |  6.824 % |
c |     19583 |   24435    86622 |   19046   10861   419778    38.7 |  6.824 % |
c |     21291 |   24435    86622 |   20951   12569   484016    38.5 |  6.824 % |
c |     23853 |   24435    86622 |   23046   15131   625008    41.3 |  6.824 % |
c |     27698 |   24398    86351 |   25312   18971   804595    42.4 |  6.897 % |
c ==============================================================================
c (current CPU-time: 22.7175 s)
c ==============================================================================
c [1mFound solution: 143770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     28374 |   24453    86550 |    7335   19647   838493    42.7 |  6.897 % |
c   -- subsuming                       
c   -- var.elim.:  196/196          
c   -- var.elim.:  123/123          
c |     28374 |   24414    86594 |      --   19647       --      -- |     --   | -39/45
c |     28374 |   24414    86594 |    9765   19630   836747    42.6 |  6.897 % |
c |     28475 |   24414    86594 |   10742    8617   337434    39.2 |  6.918 % |
c |     28625 |   24414    86594 |   11816    8767   339764    38.8 |  6.918 % |
c |     28851 |   24414    86594 |   12998    8993   346583    38.5 |  6.918 % |
c |     29189 |   24414    86594 |   14297    9331   359129    38.5 |  6.918 % |
c |     29700 |   24414    86594 |   15727    9842   369561    37.5 |  6.918 % |
c |     30459 |   24414    86594 |   17300   10601   395120    37.3 |  6.918 % |
c |     31599 |   24414    86594 |   19030   11741   430665    36.7 |  6.918 % |
c |     33307 |   24414    86594 |   20933   13449   499601    37.1 |  6.918 % |
c |     35871 |   24414    86594 |   23026   16013   613172    38.3 |  6.918 % |
c ==============================================================================
c (current CPU-time: 28.5467 s)
c ==============================================================================
c [1mFound solution: 140538[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36041 |   24460    86773 |    7337   16183   628652    38.8 |  6.918 % |
c   -- subsuming                       
c   -- var.elim.:  132/132          
c   -- var.elim.:  103/103          
c |     36041 |   24431    86837 |      --   16183       --      -- |     --   | -29/65
c |     36041 |   24431    86837 |    9772   16183   628652    38.8 |  6.918 % |
c |     36141 |   24431    86837 |   10749    7293   232647    31.9 |  6.938 % |
c |     36294 |   24431    86837 |   11824    7446   236472    31.8 |  6.938 % |
c |     36520 |   24431    86837 |   13007    7672   242672    31.6 |  6.938 % |
c |     36857 |   24431    86837 |   14307    8009   252463    31.5 |  6.938 % |
c |     37364 |   24431    86837 |   15738    8516   269947    31.7 |  6.938 % |
c |     38123 |   24431    86837 |   17312    9275   290751    31.3 |  6.938 % |
c |     39262 |   24431    86837 |   19043   10414   336534    32.3 |  6.938 % |
c |     40972 |   24431    86837 |   20948   12124   401199    33.1 |  6.938 % |
c |     43534 |   24431    86837 |   23042   14686   601193    40.9 |  6.938 % |
c |     47379 |   24431    86837 |   25347   18531   813633    43.9 |  6.938 % |
c |     53145 |   24431    86837 |   27881   24297  1188258    48.9 |  6.938 % |
c |     61794 |   24431    86837 |  #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.96 0.91 2/54 26522
Raw data (stat): 26522 (runsolver) R 26521 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482676969 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.96 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 2795 0 0 0 991 8 0 0 25 0 1 0 482676969 10330112 2051 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2522 2051 603 41 0 2481 0
vsize: 10088
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 3209 0 0 0 1990 9 0 0 25 0 1 0 482676969 11231232 2302 4294967295 134512640 134672761 3221224528 3221223568 134613116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2302 603 41 0 2701 0
vsize: 10968
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 3674 0 0 0 2988 11 0 0 25 0 1 0 482676969 12390400 2577 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3025 2577 603 41 0 2984 0
vsize: 12100
[startup+40.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 3861 0 0 0 3987 12 0 0 25 0 1 0 482676969 13180928 2764 4294967295 134512640 134672761 3221224528 3221223568 134612873 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3218 2764 603 41 0 3177 0
vsize: 12872
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 4353 0 0 0 4985 13 0 0 25 0 1 0 482676969 15134720 3256 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3695 3256 603 41 0 3654 0
vsize: 14780
[startup+60.0032 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 4353 0 0 0 5985 14 0 0 25 0 1 0 482676969 15134720 3256 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3695 3256 603 41 0 3654 0
vsize: 14780
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 4877 0 0 0 6983 16 0 0 25 0 1 0 482676969 17510400 3780 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4275 3780 603 41 0 4234 0
vsize: 17100
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 5010 0 0 0 7983 16 0 0 25 0 1 0 482676969 18231296 3913 4294967295 134512640 134672761 3221224528 3221223480 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4451 3913 603 41 0 4410 0
vsize: 17804
[startup+90.0047 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 5010 0 0 0 8983 17 0 0 25 0 1 0 482676969 18231296 3913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4451 3913 603 41 0 4410 0
vsize: 17804
[startup+100.108 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 5095 0 0 0 9993 17 0 0 25 0 1 0 482676969 18366464 3998 4294967295 134512640 134672761 3221224528 3221223712 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4484 3998 603 41 0 4443 0
vsize: 17936
[startup+110.111 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 5379 0 0 0 10992 18 0 0 25 0 1 0 482676969 19431424 4275 4294967295 134512640 134672761 3221224528 3221223664 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4744 4275 603 41 0 4703 0
vsize: 18976
[startup+120.111 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 5379 0 0 0 11992 18 0 0 25 0 1 0 482676969 19431424 4275 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4744 4275 603 41 0 4703 0
vsize: 18976
[startup+130.112 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 5622 0 0 0 12991 19 0 0 25 0 1 0 482676969 20492288 4518 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5003 4518 603 41 0 4962 0
vsize: 20012
[startup+140.113 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6192 0 0 0 13989 22 0 0 25 0 1 0 482676969 22872064 5088 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5584 5088 603 41 0 5543 0
vsize: 22336
[startup+150.114 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6555 0 0 0 14988 23 0 0 25 0 1 0 482676969 24055808 5410 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5410 603 41 0 5832 0
vsize: 23492
[startup+160.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6555 0 0 0 15987 23 0 0 25 0 1 0 482676969 24055808 5410 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5410 603 41 0 5832 0
vsize: 23492
[startup+170.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6555 0 0 0 16987 23 0 0 25 0 1 0 482676969 24055808 5410 4294967295 134512640 134672761 3221224528 3221223568 134614258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5410 603 41 0 5832 0
vsize: 23492
[startup+180.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6555 0 0 0 17987 23 0 0 25 0 1 0 482676969 24055808 5410 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5410 603 41 0 5832 0
vsize: 23492
[startup+190.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6555 0 0 0 18987 24 0 0 25 0 1 0 482676969 24055808 5410 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5410 603 41 0 5832 0
vsize: 23492
[startup+200.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6555 0 0 0 19987 24 0 0 25 0 1 0 482676969 24055808 5410 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5410 603 41 0 5832 0
vsize: 23492
[startup+210.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6598 0 0 0 20986 25 0 0 25 0 1 0 482676969 24051712 5410 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5872 5410 603 41 0 5831 0
vsize: 23488
[startup+220.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6598 0 0 0 21986 25 0 0 25 0 1 0 482676969 24051712 5410 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5872 5410 603 41 0 5831 0
vsize: 23488
[startup+230.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6598 0 0 0 22986 25 0 0 25 0 1 0 482676969 24051712 5410 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5872 5410 603 41 0 5831 0
vsize: 23488
[startup+240.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 6598 0 0 0 23986 26 0 0 25 0 1 0 482676969 24051712 5410 4294967295 134512640 134672761 3221224528 3221223712 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5872 5410 603 41 0 5831 0
vsize: 23488
[startup+250.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7345 0 0 0 24983 29 0 0 25 0 1 0 482676969 27095040 6157 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6615 6157 603 41 0 6574 0
vsize: 26460
[startup+260.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7484 0 0 0 25982 29 0 0 25 0 1 0 482676969 27586560 6250 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6735 6250 603 41 0 6694 0
vsize: 26940
[startup+270.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7484 0 0 0 26982 29 0 0 25 0 1 0 482676969 27586560 6250 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6735 6250 603 41 0 6694 0
vsize: 26940
[startup+280.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7484 0 0 0 27983 29 0 0 25 0 1 0 482676969 27586560 6250 4294967295 134512640 134672761 3221224528 3221223568 134612799 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6735 6250 603 41 0 6694 0
vsize: 26940
[startup+290.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7484 0 0 0 28982 30 0 0 25 0 1 0 482676969 27586560 6250 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6735 6250 603 41 0 6694 0
vsize: 26940
[startup+300.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 29982 30 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+310.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 30983 30 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+320.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 31983 30 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+330.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 32983 30 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+340.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 33982 31 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223712 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+350.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 34982 31 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223520 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+360.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7529 0 0 0 35982 31 0 0 25 0 1 0 482676969 27582464 6249 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6249 603 41 0 6693 0
vsize: 26936
[startup+370.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 7951 0 0 0 36980 33 0 0 25 0 1 0 482676969 29417472 6671 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7182 6671 603 41 0 7141 0
vsize: 28728
[startup+380.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 8444 0 0 0 37979 35 0 0 25 0 1 0 482676969 31379456 7164 4294967295 134512640 134672761 3221224528 3221223520 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7661 7164 603 41 0 7620 0
vsize: 30644
[startup+390.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 8935 0 0 0 38976 37 0 0 25 0 1 0 482676969 33353728 7655 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7655 603 41 0 8102 0
vsize: 32572
[startup+400.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 9317 0 0 0 39975 38 0 0 25 0 1 0 482676969 34926592 8037 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8527 8037 603 41 0 8486 0
vsize: 34108
[startup+410.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 9692 0 0 0 40974 39 0 0 25 0 1 0 482676969 36507648 8412 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8913 8412 603 41 0 8872 0
vsize: 35652
[startup+420.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10033 0 0 0 41973 41 0 0 25 0 1 0 482676969 37953536 8753 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9266 8753 603 41 0 9225 0
vsize: 37064
[startup+430.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 42972 42 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+440.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 43972 42 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+450.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 44972 42 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+460.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 45972 42 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+470.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 46972 43 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+480.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26522
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 47971 43 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+490.137 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 48971 43 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+500.137 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10231 0 0 0 49971 43 0 0 25 0 1 0 482676969 38547456 8932 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9411 8932 603 41 0 9370 0
vsize: 37644
[startup+510.137 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10473 0 0 0 50970 44 0 0 25 0 1 0 482676969 39583744 9174 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9664 9174 603 41 0 9623 0
vsize: 38656
[startup+520.138 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 10899 0 0 0 51970 45 0 0 25 0 1 0 482676969 41418752 9600 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10112 9600 603 41 0 10071 0
vsize: 40448
[startup+530.139 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 11323 0 0 0 52969 46 0 0 25 0 1 0 482676969 43126784 10024 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10529 10024 603 41 0 10488 0
vsize: 42116
[startup+540.14 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 11750 0 0 0 53967 48 0 0 25 0 1 0 482676969 44818432 10451 4294967295 134512640 134672761 3221224528 3221223568 134612578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10942 10451 603 41 0 10901 0
vsize: 43768
[startup+550.14 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 26575
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 12106 0 0 0 54966 49 0 0 25 0 1 0 482676969 46264320 10807 4294967295 134512640 134672761 3221224528 3221223712 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11295 10807 603 41 0 11254 0
vsize: 45180
[startup+560.14 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 12476 0 0 0 55965 50 0 0 25 0 1 0 482676969 47861760 11177 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11685 11177 603 41 0 11644 0
vsize: 46740
[startup+570.14 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 12820 0 0 0 56964 51 0 0 25 0 1 0 482676969 49283072 11521 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12032 11521 603 41 0 11991 0
vsize: 48128
[startup+580.141 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 13157 0 0 0 57963 53 0 0 25 0 1 0 482676969 50585600 11858 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12350 11858 603 41 0 12309 0
vsize: 49400
[startup+590.142 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 13498 0 0 0 58963 53 0 0 25 0 1 0 482676969 52023296 12199 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12701 12199 603 41 0 12660 0
vsize: 50804
[startup+600.142 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 13845 0 0 0 59962 55 0 0 25 0 1 0 482676969 53460992 12546 4294967295 134512640 134672761 3221224528 3221223712 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13052 12546 603 41 0 13011 0
vsize: 52208
[startup+610.143 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 60961 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+620.142 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 61962 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+630.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 62962 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223728 134610712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+640.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 63962 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+650.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 64962 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+660.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 65962 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+670.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 66963 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+680.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 67963 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+690.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 68964 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+700.252 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 69974 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+710.252 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 70974 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+720.253 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 71974 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+730.261 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 72975 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+740.261 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14025 0 0 0 73975 55 0 0 25 0 1 0 482676969 53932032 12676 4294967295 134512640 134672761 3221224528 3221223568 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12676 603 41 0 13126 0
vsize: 52668
[startup+750.261 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14026 0 0 0 74976 55 0 0 25 0 1 0 482676969 53932032 12677 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12677 603 41 0 13126 0
vsize: 52668
[startup+760.262 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14038 0 0 0 75976 55 0 0 25 0 1 0 482676969 54063104 12689 4294967295 134512640 134672761 3221224528 3221223712 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13199 12689 603 41 0 13158 0
vsize: 52796
[startup+770.262 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14449 0 0 0 76975 57 0 0 25 0 1 0 482676969 55762944 13100 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13614 13100 603 41 0 13573 0
vsize: 54456
[startup+780.263 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 14890 0 0 0 77974 58 0 0 25 0 1 0 482676969 57593856 13541 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14061 13541 603 41 0 14020 0
vsize: 56244
[startup+790.263 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15277 0 0 0 78973 59 0 0 25 0 1 0 482676969 59179008 13928 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14448 13928 603 41 0 14407 0
vsize: 57792
[startup+800.263 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15619 0 0 0 79972 60 0 0 25 0 1 0 482676969 60616704 14270 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14799 14270 603 41 0 14758 0
vsize: 59196
[startup+810.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15781 0 0 0 80973 60 0 0 25 0 1 0 482676969 60948480 14382 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14382 603 41 0 14839 0
vsize: 59520
[startup+820.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15781 0 0 0 81973 60 0 0 25 0 1 0 482676969 60948480 14382 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14382 603 41 0 14839 0
vsize: 59520
[startup+830.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15781 0 0 0 82973 60 0 0 25 0 1 0 482676969 60948480 14382 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14382 603 41 0 14839 0
vsize: 59520
[startup+840.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26577
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15781 0 0 0 83974 60 0 0 25 0 1 0 482676969 60948480 14382 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14382 603 41 0 14839 0
vsize: 59520
[startup+850.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15781 0 0 0 84974 60 0 0 25 0 1 0 482676969 60948480 14382 4294967295 134512640 134672761 3221224528 3221223712 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14382 603 41 0 14839 0
vsize: 59520
[startup+860.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15782 0 0 0 85974 60 0 0 25 0 1 0 482676969 60948480 14383 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14383 603 41 0 14839 0
vsize: 59520
[startup+870.274 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 86974 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+880.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 87974 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+890.274 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 88974 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+900.273 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 89974 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+910.274 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 90975 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+920.274 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 91975 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+930.275 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 92975 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+940.275 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 93975 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+950.276 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 94975 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+960.276 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 95976 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+970.276 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 96976 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+980.278 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 97976 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+990.278 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 98976 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1000.28 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 99976 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1010.28 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 100977 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1020.28 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 101977 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1030.28 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 102977 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1040.28 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 103977 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223676 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1050.28 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 104978 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1060.28 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 105978 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1070.28 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 106978 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1080.28 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 107978 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223568 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1090.28 s]
Raw data (loadavg): 1.32 1.07 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 108978 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1100.28 s]
Raw data (loadavg): 1.27 1.06 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 109978 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1110.28 s]
Raw data (loadavg): 1.23 1.06 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 110979 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1120.28 s]
Raw data (loadavg): 1.19 1.06 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 111979 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223728 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1130.28 s]
Raw data (loadavg): 1.16 1.06 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 112979 60 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1140.29 s]
Raw data (loadavg): 1.14 1.05 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 113979 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1150.28 s]
Raw data (loadavg): 1.11 1.05 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 114979 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1160.28 s]
Raw data (loadavg): 1.10 1.05 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 115980 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223728 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1170.28 s]
Raw data (loadavg): 1.08 1.05 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 116980 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1180.29 s]
Raw data (loadavg): 1.07 1.05 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 117980 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1190.29 s]
Raw data (loadavg): 1.06 1.04 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 118980 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223688 134614477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
[startup+1200.29 s]
Raw data (loadavg): 1.05 1.04 0.94 2/54 26579
Raw data (stat): 26522 (minisat+) R 26521 29151 29150 0 -1 0 15844 0 0 0 119980 61 0 0 25 0 1 0 482676969 60948480 14391 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14880 14391 603 41 0 14839 0
vsize: 59520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.32 s]
Raw data (loadavg): 1.05 1.04 0.94 1/54 26579
Raw data (stat): 26522 (minisat+) Z 26521 29151 29150 0 -1 12 15845 0 0 0 119980 63 0 0 25 0 1 0 482676969 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.32
CPU time (s): 1200.45
CPU user time (s): 1199.81
CPU system time (s): 0.637903
CPU usage (%): 100.011
Max. virtual memory (Kb): 59520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####