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-ii32c1.opb
MD5SUM	8afff0cc8710524125079d5ef00fedc0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167
Optimality of the best value was proved	NO
Number of terms in the objective function	450
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	450
Total number of constraints	1505
Number of constraints which are clauses	1505
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 5469

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 00:08:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3911 boxname=wulflinc21 idbench=151 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8afff0cc8710524125079d5ef00fedc0  /oldhome/oroussel/tmp/wulflinc21/normalized-ii32c1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-ii32c1.opb /oldhome/oroussel/tmp/wulflinc21/normalized-ii32c1.opb
IDLAUNCH: 3911
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        902596 kB
Buffers:         27028 kB
Cached:          85172 kB
SwapCached:          0 kB
Active:          34224 kB
Inactive:        80864 kB
HighTotal:      131008 kB
HighFree:        42168 kB
LowTotal:       903652 kB
LowFree:        860428 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11256 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:25:08 (client local time) WITH STATUS 30 IN 1022.5 SECONDS
stats: 3911 0 1022.5 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1505 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 |    1505     6531 |     451       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  450/450          
c |         0 |    1505     6531 |     602       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.077988 s)
c ==============================================================================
c [1mFound solution: 216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |   21667    53698 |    6500       1       30    30.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13516          
c   -- var.elim.:  2000/13516          
c   -- var.elim.:  3000/13516          
c   -- var.elim.:  4000/13516          
c   -- var.elim.:  5000/13516          
c   -- var.elim.:  6000/13516          
c   -- var.elim.:  7000/13516          
c   -- var.elim.:  8000/13516          
c   -- var.elim.:  9000/13516          
c   -- var.elim.:  10000/13516          
c   -- var.elim.:  11000/13516          
c   -- var.elim.:  12000/13516          
c   -- var.elim.:  13000/13516          
c   -- var.elim.:  13516/13516          
c   -- var.elim.:  1000/6617          
c   -- var.elim.:  2000/6617          
c   -- var.elim.:  3000/6617          
c   -- var.elim.:  4000/6617          
c   -- var.elim.:  5000/6617          
c   -- var.elim.:  6000/6617          
c   -- var.elim.:  6617/6617          
c   -- var.elim.:  1000/3807          
c   -- var.elim.:  2000/3807          
c   -- var.elim.:  3000/3807          
c   -- var.elim.:  3807/3807          
c   -- var.elim.:  1000/2654          
c   -- var.elim.:  2000/2654          
c   -- var.elim.:  2654/2654          
c   -- var.elim.:  1000/2163          
c   -- var.elim.:  2000/2163          
c   -- var.elim.:  2163/2163          
c   -- var.elim.:  1000/1356          
c   -- var.elim.:  1356/1356          
c   -- var.elim.:  168/168          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/1964          
c   -- var.elim.:  1964/1964          
c   -- var.elim.:  328/328          
c |         1 |    6829    37859 |      --       1       --      -- |     --   | -14830/-15815
c |         1 |    6829    37859 |    2731       1       30    30.0 |  0.000 % |
c ==============================================================================
c (current CPU-time: 7.70083 s)
c ==============================================================================
c [1mFound solution: 206[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 |         5 |   21774    74441 |    6532       4      143    35.8 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13351          
c   -- var.elim.:  2000/13351          
c   -- var.elim.:  3000/13351          
c   -- var.elim.:  4000/13351          
c   -- var.elim.:  5000/13351          
c   -- var.elim.:  6000/13351          
c   -- var.elim.:  7000/13351          
c   -- var.elim.:  8000/13351          
c   -- var.elim.:  9000/13351          
c   -- var.elim.:  10000/13351          
c   -- var.elim.:  11000/13351          
c   -- var.elim.:  12000/13351          
c   -- var.elim.:  13000/13351          
c   -- var.elim.:  13351/13351          
c   -- var.elim.:  1000/6426          
c   -- var.elim.:  2000/6426          
c   -- var.elim.:  3000/6426          
c   -- var.elim.:  4000/6426          
c   -- var.elim.:  5000/6426          
c   -- var.elim.:  6000/6426          
c   -- var.elim.:  6426/6426          
c   -- var.elim.:  1000/3857          
c   -- var.elim.:  2000/3857          
c   -- var.elim.:  3000/3857          
c   -- var.elim.:  3857/3857          
c   -- var.elim.:  1000/2834          
c   -- var.elim.:  2000/2834          
c   -- var.elim.:  2834/2834          
c   -- var.elim.:  1000/2317          
c   -- var.elim.:  2000/2317          
c   -- var.elim.:  2317/2317          
c   -- var.elim.:  1000/1614          
c   -- var.elim.:  1614/1614          
c   -- var.elim.:  741/741          
c   -- var.elim.:  145/145          
c   -- subsuming                       
c   -- var.elim.:  996/996          
c   -- var.elim.:  32/32          
c |         5 |    7124    41538 |      --       4       --      -- |     --   | -14641/-32860
c |         5 |    7124    41538 |    2849       4      143    35.8 |  0.000 % |
c ==============================================================================
c (current CPU-time: 15.0057 s)
c ==============================================================================
c [1mFound solution: 192[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 |         8 |   21679    77263 |    6503       7      353    50.4 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13160          
c   -- var.elim.:  2000/13160          
c   -- var.elim.:  3000/13160          
c   -- var.elim.:  4000/13160          
c   -- var.elim.:  5000/13160          
c   -- var.elim.:  6000/13160          
c   -- var.elim.:  7000/13160          
c   -- var.elim.:  8000/13160          
c   -- var.elim.:  9000/13160          
c   -- var.elim.:  10000/13160          
c   -- var.elim.:  11000/13160          
c   -- var.elim.:  12000/13160          
c   -- var.elim.:  13000/13160          
c   -- var.elim.:  13160/13160          
c   -- var.elim.:  1000/6349          
c   -- var.elim.:  2000/6349          
c   -- var.elim.:  3000/6349          
c   -- var.elim.:  4000/6349          
c   -- var.elim.:  5000/6349          
c   -- var.elim.:  6000/6349          
c   -- var.elim.:  6349/6349          
c   -- var.elim.:  1000/3982          
c   -- var.elim.:  2000/3982          
c   -- var.elim.:  3000/3982          
c   -- var.elim.:  3982/3982          
c   -- var.elim.:  1000/2923          
c   -- var.elim.:  2000/2923          
c   -- var.elim.:  2923/2923          
c   -- var.elim.:  1000/2491          
c   -- var.elim.:  2000/2491          
c   -- var.elim.:  2491/2491          
c   -- var.elim.:  1000/2092          
c   -- var.elim.:  2000/2092          
c   -- var.elim.:  2092/2092          
c   -- var.elim.:  1000/1545          
c   -- var.elim.:  1545/1545          
c   -- var.elim.:  719/719          
c   -- var.elim.:  129/129          
c   -- subsuming                       
c   -- var.elim.:  986/986          
c   -- var.elim.:  7/7          
c |         8 |    7357    43797 |      --       7       --      -- |     --   | -14310/-33432
c |         8 |    7357    43797 |    2942       7      353    50.4 |  0.000 % |
c ==============================================================================
c (current CPU-time: 23.6524 s)
c ==============================================================================
c [1mFound solution: 182[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 |        15 |   21521    78637 |    6456      14      633    45.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12952          
c   -- var.elim.:  2000/12952          
c   -- var.elim.:  3000/12952          
c   -- var.elim.:  4000/12952          
c   -- var.elim.:  5000/12952          
c   -- var.elim.:  6000/12952          
c   -- var.elim.:  7000/12952          
c   -- var.elim.:  8000/12952          
c   -- var.elim.:  9000/12952          
c   -- var.elim.:  10000/12952          
c   -- var.elim.:  11000/12952          
c   -- var.elim.:  12000/12952          
c   -- var.elim.:  12952/12952          
c   -- var.elim.:  1000/6213          
c   -- var.elim.:  2000/6213          
c   -- var.elim.:  3000/6213          
c   -- var.elim.:  4000/6213          
c   -- var.elim.:  5000/6213          
c   -- var.elim.:  6000/6213          
c   -- var.elim.:  6213/6213          
c   -- var.elim.:  1000/3716          
c   -- var.elim.:  2000/3716          
c   -- var.elim.:  3000/3716          
c   -- var.elim.:  3716/3716          
c   -- var.elim.:  1000/2844          
c   -- var.elim.:  2000/2844          
c   -- var.elim.:  2844/2844          
c   -- var.elim.:  1000/2286          
c   -- var.elim.:  2000/2286          
c   -- var.elim.:  2286/2286          
c   -- var.elim.:  1000/2052          
c   -- var.elim.:  2000/2052          
c   -- var.elim.:  2052/2052          
c   -- var.elim.:  1000/1341          
c   -- var.elim.:  1341/1341          
c   -- var.elim.:  256/256          
c   -- subsuming                       
c   -- var.elim.:  1000/1141          
c   -- var.elim.:  1141/1141          
c |        15 |    7476    47493 |      --      14       --      -- |     --   | -14024/-30915
c |        15 |    7476    47493 |    2990      14      633    45.2 |  0.000 % |
c ==============================================================================
c (current CPU-time: 33.2459 s)
c ==============================================================================
c [1mFound solution: 181[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 |        91 |   19558    77119 |    5867      90    11323   125.8 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11038          
c   -- var.elim.:  2000/11038          
c   -- var.elim.:  3000/11038          
c   -- var.elim.:  4000/11038          
c   -- var.elim.:  5000/11038          
c   -- var.elim.:  6000/11038          
c   -- var.elim.:  7000/11038          
c   -- var.elim.:  8000/11038          
c   -- var.elim.:  9000/11038          
c   -- var.elim.:  10000/11038          
c   -- var.elim.:  11000/11038          
c   -- var.elim.:  11038/11038          
c   -- var.elim.:  1000/5214          
c   -- var.elim.:  2000/5214          
c   -- var.elim.:  3000/5214          
c   -- var.elim.:  4000/5214          
c   -- var.elim.:  5000/5214          
c   -- var.elim.:  5214/5214          
c   -- var.elim.:  1000/3245          
c   -- var.elim.:  2000/3245          
c   -- var.elim.:  3000/3245          
c   -- var.elim.:  3245/3245          
c   -- var.elim.:  1000/2274          
c   -- var.elim.:  2000/2274          
c   -- var.elim.:  2274/2274          
c   -- var.elim.:  1000/1663          
c   -- var.elim.:  1663/1663          
c   -- var.elim.:  922/922          
c   -- var.elim.:  183/183          
c   -- subsuming                       
c   -- var.elim.:  32/32          
c |        91 |    7510    48049 |      --      90       --      -- |     --   | -12048/-29069
c |        91 |    7510    48049 |    3004      90    11323   125.8 |  0.000 % |
c |       191 |    6796    42996 |    2990     151    12150    80.5 | 11.052 % |
c |       341 |    6745    42701 |    3264     298    47524   159.5 | 11.736 % |
c |       569 |    6745    42701 |    3591     526   118338   225.0 | 11.735 % |
c |       906 |    6743    42695 |    3948     860   256429   298.2 | 11.767 % |
c |      1413 |    6669    42202 |    4296    1364   478731   351.0 | 12.574 % |
c |      2173 |    6527    41047 |    4625    2115   704370   333.0 | 14.375 % |
c |      3314 |    6118    38063 |    4768    3233  1080911   334.3 | 19.249 % |
c |      5025 |    5775    35679 |    4951    4918  1685435   342.7 | 23.968 % |
c ==============================================================================
c (current CPU-time: 54.1588 s)
c ==============================================================================
c [1mFound solution: 179[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 |      7141 |   17887    64026 |    5366    5005  1465845   292.9 | 23.968 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10935          
c   -- var.elim.:  2000/10935          
c   -- var.elim.:  3000/10935          
c   -- var.elim.:  4000/10935          
c   -- var.elim.:  5000/10935          
c   -- var.elim.:  6000/10935          
c   -- var.elim.:  7000/10935          
c   -- var.elim.:  8000/10935          
c   -- var.elim.:  9000/10935          
c   -- var.elim.:  10000/10935          
c   -- var.elim.:  10935/10935          
c   -- var.elim.:  1000/5009          
c   -- var.elim.:  2000/5009          
c   -- var.elim.:  3000/5009          
c   -- var.elim.:  4000/5009          
c   -- var.elim.:  5000/5009          
c   -- var.elim.:  5009/5009          
c   -- var.elim.:  1000/2905          
c   -- var.elim.:  2000/2905          
c   -- var.elim.:  2905/2905          
c   -- var.elim.:  1000/1877          
c   -- var.elim.:  1877/1877          
c   -- var.elim.:  1000/1333          
c   -- var.elim.:  1333/1333          
c   -- var.elim.:  1000/1071          
c   -- var.elim.:  1071/1071          
c   -- var.elim.:  745/745          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  894/894          
c |      7141 |    5565    35664 |      --    5005       --      -- |     --   | -12245/-28207
c |      7141 |    5565    35664 |    2226    1340    53524    39.9 | 23.968 % |
c |      7241 |    5565    35664 |    2448    1440    75875    52.7 | 36.361 % |
c |      7391 |    5565    35664 |    2693    1590   120087    75.5 | 36.361 % |
c |      7617 |    5565    35664 |    2962    1816   181041    99.7 | 36.361 % |
c |      7954 |    5495    34825 |    3218    2151   259434   120.6 | 36.992 % |
c |      8461 |    5425    34337 |    3494    2655   403174   151.9 | 37.871 % |
c |      9220 |    5425    34337 |    3844    3414   637975   186.9 | 37.870 % |
c |     10359 |    5425    34337 |    4228    4553   965201   212.0 | 37.870 % |
c |     12068 |    5267    32991 |    4516    6226  1367872   219.7 | 39.682 % |
c |     14631 |    5267    32991 |    4967    6714  1748182   260.4 | 39.682 % |
c |     18475 |    5194    32364 |    5388    6053  1186198   196.0 | 40.532 % |
c |     24241 |    5040    31062 |    5751    6710  1822591   271.6 | 42.481 % |
c |     32891 |    4967    30429 |    6235    7157  1676265   234.2 | 43.359 % |
c |     45865 |    4967    30429 |    6858    8320  2483749   298.5 | 43.359 % |
c |     65327 |    4965    30423 |    7541    6250  1750100   280.0 | 43.386 % |
c ==============================================================================
c (current CPU-time: 241.143 s)
c ==============================================================================
c [1mFound solution: 168[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 |     84477 |   17335    60041 |    5200    8778  2643054   301.1 | 43.386 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10617          
c   -- var.elim.:  2000/10617          
c   -- var.elim.:  3000/10617          
c   -- var.elim.:  4000/10617          
c   -- var.elim.:  5000/10617          
c   -- var.elim.:  6000/10617          
c   -- var.elim.:  7000/10617          
c   -- var.elim.:  8000/10617          
c   -- var.elim.:  9000/10617          
c   -- var.elim.:  10000/10617          
c   -- var.elim.:  10617/10617          
c   -- var.elim.:  1000/4699          
c   -- var.elim.:  2000/4699          
c   -- var.elim.:  3000/4699          
c   -- var.elim.:  4000/4699          
c   -- var.elim.:  4699/4699          
c   -- var.elim.:  1000/2666          
c   -- var.elim.:  2000/2666          
c   -- var.elim.:  2666/2666          
c   -- var.elim.:  1000/1615          
c   -- var.elim.:  1615/1615          
c   -- var.elim.:  1000/1204          
c   -- var.elim.:  1204/1204          
c   -- var.elim.:  889/889          
c   -- var.elim.:  675/675          
c   -- var.elim.:  333/333          
c   -- subsuming                       
c   -- var.elim.:  746/746          
c   -- var.elim.:  10/10          
c |     84477 |    5040    31946 |      --    8778       --      -- |     --   | -12228/-27788
c |     84477 |    5040    31946 |    2016    3037   149631    49.3 | 43.386 % |
c |     84577 |    5040    31946 |    2217    3137   163485    52.1 | 47.926 % |
c |     84727 |    5040    31946 |    2439    3287   182228    55.4 | 47.926 % |
c |     84953 |    5040    31946 |    2683    3513   220442    62.8 | 47.926 % |
c |     85292 |    5040    31946 |    2951    3852   260289    67.6 | 47.926 % |
c |     85799 |    5040    31946 |    3246    4359   363410    83.4 | 47.926 % |
c |     86562 |    4999    31536 |    3542    5118   524219   102.4 | 48.307 % |
c |     87701 |    4918    30928 |    3833    4432   585223   132.0 | 49.173 % |
c |     89411 |    4918    30928 |    4216    6142   961535   156.6 | 49.173 % |
c |     91975 |    4918    30928 |    4638    6341  1132654   178.6 | 49.173 % |
c |     95820 |    4918    30928 |    5102    5214  1001360   192.1 | 49.173 % |
c |    101586 |    4918    30928 |    5612    5773  1237750   214.4 | 49.173 % |
c |    110235 |    4918    30928 |    6173    6067  1164207   191.9 | 49.173 % |
c |    123211 |    4918    30928 |    6791    7435  1563515   210.3 | 49.175 % |
c ==============================================================================
c (current CPU-time: 326.608 s)
c ==============================================================================
c [1mFound solution: 167[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 |    126259 |   16958    59712 |    5087    7367  1360371   184.7 | 49.175 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10305          
c   -- var.elim.:  2000/10305          
c   -- var.elim.:  3000/10305          
c   -- var.elim.:  4000/10305          
c   -- var.elim.:  5000/10305          
c   -- var.elim.:  6000/10305          
c   -- var.elim.:  7000/10305          
c   -- var.elim.:  8000/10305          
c   -- var.elim.:  9000/10305          
c   -- var.elim.:  10000/10305          
c   -- var.elim.:  10305/10305          
c   -- var.elim.:  1000/4533          
c   -- var.elim.:  2000/4533          
c   -- var.elim.:  3000/4533          
c   -- var.elim.:  4000/4533          
c   -- var.elim.:  4533/4533          
c   -- var.elim.:  1000/2589          
c   -- var.elim.:  2000/2589          
c   -- var.elim.:  2589/2589          
c   -- var.elim.:  1000/1634          
c   -- var.elim.:  1634/1634          
c   -- var.elim.:  1000/1250          
c   -- var.elim.:  1250/1250          
c   -- var.elim.:  925/925          
c   -- var.elim.:  675/675          
c   -- var.elim.:  351/351          
c   -- subsuming                       
c   -- var.elim.:  597/597          
c   -- var.elim.:  10/10          
c |    126259 |    4953    32043 |      --    7367       --      -- |     --   | -11994/-27646
c |    126259 |    4953    32043 |    1981    4427   379163    85.6 | 49.175 % |
c |    126359 |    4913    31729 |    2161    3051   198256    65.0 | 50.525 % |
c |    126512 |    4913    31729 |    2377    3204   223717    69.8 | 50.525 % |
c |    126737 |    4890    31530 |    2603    3428   265170    77.4 | 50.800 % |
c |    127075 |    4890    31530 |    2863    3766   342673    91.0 | 50.800 % |
c |    127582 |    4890    31530 |    3150    4273   448497   105.0 | 50.800 % |
c |    128343 |    4890    31530 |    3465    5034   611272   121.4 | 50.800 % |
c |    129483 |    4890    31530 |    3811    6174   843110   136.6 | 50.800 % |
c |    131191 |    4857    31222 |    4164    5823   913068   156.8 | 51.176 % |
c |    133753 |    4613    28568 |    4350    6298   936533   148.7 | 53.702 % |
c |    137601 |    4613    28568 |    4785    5324   932630   175.2 | 53.702 % |
c |    143367 |    4533    27858 |    5173    6097   975056   159.9 | 54.652 % |
c |    152017 |    4488    27428 |    5634    6849  1050685   153.4 | 55.203 % |
c |    164992 |    4488    27428 |    6197    6014   850326   141.4 | 55.203 % |
c |    184453 |    4488    27428 |    6817    7867  1495914   190.2 | 55.203 % |
c |    213649 |    4488    27428 |    7498    8856  1638381   185.0 | 55.203 % |
c |    257438 |    4488    27428 |    8248    9219  1426230   154.7 | 55.203 % |
c |    323122 |    4488    27428 |    9073    9903  1679514   169.6 | 55.203 % |
c |    421651 |    4488    27428 |    9981   10961  2153600   196.5 | 55.203 % |
c ==============================================================================
c [1mOptimal solution: 167[0m
s OPTIMUM FOUND
v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 -x79 x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 -x125 x126 x127 -x128 -x129 -x130 x131 -x132 -x133 -x134 x135 -x136 -x137 -x138 x139 -x140 x141 -x142 -x143 -x144 -x145 -x146 x147 -x148 -x149 -x150 x151 -x152 -x153 -x154 x155 -x156 x157 -x158 -x159 x160 -x161 -x162 x163 -x164 -x165 -x166 x167 -x168 x169 -x170 -x171 -x172 -x173 -x174 x175 -x176 x177 -x178 -x179 x180 -x181 -x182 x183 -x184 -x185 -x186 x187 -x188 x189 -x190 -x191 -x192 x193 -x194 -x195 -x196 -x197 -x198 x199 -x200 -x201 -x202 x203 -x204 -x205 -x206 x207 -x208 -x209 -x210 x211 -x212 -x213 -x214 x215 -x216 x217 -x218 -x219 -x220 x221 -x222 -x223 -x224 -x225 -x226 x227 -x228 -x229 -x230 x231 -x232 -x233 -x234 x235 -x236 -x237 -x238 x239 -x240 x241 -x242 -x243 x244 x245 -x246 -x247 -x248 -x249 -x250 x251 -x252 x253 -x254 -x255 -x256 x257 -x258 -x259 -x260 -x261 -x262 x263 -x264 -x265 -x266 x267 -x268 x269 -x270 -x271 -x272 -x273 -x274 x275 -x276 x277 -x278 -x279 -x280 x281 -x282 -x283 -x284 x285 -x286 -x287 -x288 x289 -x290 -x291 -x292 x293 -x294 -x295 -x296 x297 -x298 -x299 -x300 x301 -x302 -x303 -x304 -x305 -x306 x307 -x308 -x309 -x310 x311 -x312 -x313 -x314 x315 -x316 x317 -x318 -x319 -x320 x321 -x322 -x323 -x324 -x325 -x326 x327 -x328 -x329 x330 x331 -x332 -x333 -x334 x335 -x336 x337 -x338 -x339 x340 x341 -x342 -x343 -x344 -x345 -x346 x347 -x348 x349 -x350 -x351 -x352 x353 -x354 -x355 x356 -x357 -x358 x359 -x360 -x361 -x362 x363 -x364 x365 -x366 -x367 -x368 x369 -x370 -x371 -x372 x373 -x374 -x375 -x376 -x377 -x378 x379 -x380 x381 -x382 -x383 -x384 x385 -x386 -x387 x388 -x389 x390 x391 -x392 -x393 x394 -x395 x396 x397 -x398 -x399 x400 -x401 x402 x403 -x404 -x405 x406 -x407 x408 x409 -x410 -x411 x412 -x413 x414 x415 -x416 -x417 x418 -x419 x420 -x421 x422 -x423 x424 x425 -x426 -x427 x428 x429 -x430 -x431 x432 x433 -x434 -x435 x436 -x437 x438 x439 -x440 -x441 x442 -x443 x444 x445 -x446 -x447 x448 -x449 x450
c _______________________________________________________________________________
c 
c restarts              : 62
c conflicts             : 463750         (454 /sec)
c decisions             : 1028239        (1007 /sec)
c propagations          : 110779889      (108504 /sec)
c inspects              : 964677494      (944857 /sec)
c CPU time              : 1020.98 s
c _______________________________________________________________________________
#### 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/55 2793
Raw data (stat): 2793 (runsolver) R 2792 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 357413405 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 3143 0 0 0 982 16 0 0 25 0 1 0 357413405 13905920 2777 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2777 603 41 0 3354 0
vsize: 13580
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 4791 0 0 0 1969 29 0 0 25 0 1 0 357413405 19918848 3950 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4863 3950 603 41 0 4822 0
vsize: 19452
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 7241 0 0 0 2951 47 0 0 25 0 1 0 357413405 19263488 3929 4294967295 134512640 134672761 3221224576 3221223024 134643471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4703 3929 603 41 0 4662 0
vsize: 18812
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 10829 0 0 0 3924 67 0 0 25 0 1 0 357413405 20246528 4249 4294967295 134512640 134672761 3221224576 3221222856 1075353074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4943 4249 603 41 0 4902 0
vsize: 19772
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 12385 0 0 0 4920 71 0 0 25 0 1 0 357413405 26370048 5792 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6438 5792 603 41 0 6397 0
vsize: 25752
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 16427 0 0 0 5899 92 0 0 25 0 1 0 357413405 28225536 6375 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6891 6375 603 41 0 6850 0
vsize: 27564
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 16448 0 0 0 6898 92 0 0 25 0 1 0 357413405 28196864 6368 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6884 6368 603 41 0 6843 0
vsize: 27536
[startup+80.0016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 16492 0 0 0 7898 93 0 0 25 0 1 0 357413405 28459008 6412 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6948 6412 603 41 0 6907 0
vsize: 27792
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 16606 0 0 0 8898 93 0 0 25 0 1 0 357413405 28852224 6526 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7044 6526 603 41 0 7003 0
vsize: 28176
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17087 0 0 0 9897 94 0 0 25 0 1 0 357413405 30814208 7007 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7523 7007 603 41 0 7482 0
vsize: 30092
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17097 0 0 0 10897 94 0 0 25 0 1 0 357413405 30973952 7017 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7562 7017 603 41 0 7521 0
vsize: 30248
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17244 0 0 0 11897 95 0 0 25 0 1 0 357413405 31571968 7164 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7165 603 41 0 7667 0
vsize: 30832
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17690 0 0 0 12895 96 0 0 25 0 1 0 357413405 33390592 7610 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8152 7610 603 41 0 8111 0
vsize: 32608
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17819 0 0 0 13895 97 0 0 25 0 1 0 357413405 33918976 7739 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8281 7739 603 41 0 8240 0
vsize: 33124
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17819 0 0 0 14896 97 0 0 25 0 1 0 357413405 33914880 7739 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8280 7739 603 41 0 8239 0
vsize: 33120
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17819 0 0 0 15896 97 0 0 25 0 1 0 357413405 33910784 7739 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7739 603 41 0 8238 0
vsize: 33116
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17819 0 0 0 16896 97 0 0 25 0 1 0 357413405 33910784 7739 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7739 603 41 0 8238 0
vsize: 33116
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 17917 0 0 0 17896 97 0 0 25 0 1 0 357413405 34304000 7837 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8375 7837 603 41 0 8334 0
vsize: 33500
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 18032 0 0 0 18896 97 0 0 25 0 1 0 357413405 34791424 7952 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 7952 603 41 0 8453 0
vsize: 33976
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 18033 0 0 0 19896 97 0 0 25 0 1 0 357413405 34791424 7953 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 7953 603 41 0 8453 0
vsize: 33976
[startup+209.999 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 18157 0 0 0 20896 97 0 0 25 0 1 0 357413405 35295232 8077 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8617 8077 603 41 0 8576 0
vsize: 34468
[startup+219.999 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 18303 0 0 0 21895 98 0 0 25 0 1 0 357413405 35893248 8223 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8223 603 41 0 8722 0
vsize: 35052
[startup+230 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 18335 0 0 0 22895 98 0 0 25 0 1 0 357413405 36020224 8255 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8794 8255 603 41 0 8753 0
vsize: 35176
[startup+240 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 18335 0 0 0 23895 98 0 0 25 0 1 0 357413405 36020224 8255 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8794 8255 603 41 0 8753 0
vsize: 35176
[startup+249.999 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 24876 117 0 0 25 0 1 0 357413405 42348544 8764 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10339 8764 603 41 0 10298 0
vsize: 41356
[startup+259.999 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 25876 118 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+269.999 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 26876 118 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+280 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 27876 118 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+290 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 28876 118 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+300 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 29876 118 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+309.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 30876 118 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+320 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 22975 0 0 0 31876 119 0 0 25 0 1 0 357413405 42344448 8763 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 8763 603 41 0 10297 0
vsize: 41352
[startup+330.001 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 32860 135 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223164 134516532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+340.001 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 33856 139 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134613822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+350.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 34856 139 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134613818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+360.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 35856 139 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+370 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 36856 139 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+380.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 37856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+390.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 38856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+400.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 39856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+410.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 40856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134614212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+420.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 41856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+430.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 42856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+440.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 43856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134614239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+450.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 44856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+460.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 45856 140 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+470.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 46856 141 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223632 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+480.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 47856 141 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221222384 134645354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+490.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 48856 141 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+500.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 49856 141 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+510.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 50856 141 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+520.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 51856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+530.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 52856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134613756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+540.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 53856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223712 134614518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+550.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 54856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+560.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 55856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+570.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 56856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+580.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27082 0 0 0 57856 142 0 0 25 0 1 0 357413405 42295296 8916 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8916 603 41 0 10285 0
vsize: 41304
[startup+590.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 58856 142 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+600.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 59856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+610.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 60856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223408 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+620.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 61856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223680 134603947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+630.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 62856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+640.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 63856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+650.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 64856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+660.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 65856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+670.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 66856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+680.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 67856 143 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+690.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 68856 144 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+700.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 69856 144 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+710.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27083 0 0 0 70856 144 0 0 25 0 1 0 357413405 42295296 8917 4294967295 134512640 134672761 3221224576 3221223760 134616020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8917 603 41 0 10285 0
vsize: 41304
[startup+720.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 71856 144 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+730.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 72856 144 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+740.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 73856 144 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223512 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+750.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 74856 144 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+760.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 75856 144 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+770.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 76856 144 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+780.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 77856 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+790.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 78857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+800.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 79857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+810.009 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 80857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+820.01 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 81857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+830.01 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 82857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+840.01 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 83857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+850.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 84857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+860.01 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 85857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+870.01 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 86857 145 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223728 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+880.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 87857 146 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+890.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 88857 146 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+900.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27084 0 0 0 89857 146 0 0 25 0 1 0 357413405 42295296 8918 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 8918 603 41 0 10285 0
vsize: 41304
[startup+910.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 90856 146 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+920.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 91856 146 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+930.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 92856 147 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+940.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 93857 147 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+950.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 94856 147 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+960.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 95857 147 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+970.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 96856 147 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223616 134612848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+980.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 97856 147 0 0 25 0 1 0 357413405 42819584 9030 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9030 603 41 0 10413 0
vsize: 41816
[startup+990.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 98856 148 0 0 25 0 1 0 357413405 42795008 9030 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10448 9030 603 41 0 10407 0
vsize: 41792
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 99857 148 0 0 25 0 1 0 357413405 42795008 9030 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10448 9030 603 41 0 10407 0
vsize: 41792
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 100857 148 0 0 25 0 1 0 357413405 42795008 9030 4294967295 134512640 134672761 3221224576 3221223528 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10448 9030 603 41 0 10407 0
vsize: 41792
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 101857 148 0 0 25 0 1 0 357413405 42795008 9030 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10448 9030 603 41 0 10407 0
vsize: 41792
[startup+1022.46 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 2793
Raw data (stat): 2793 (minisat+) R 2792 30927 30926 0 -1 0 27196 0 0 0 101857 148 0 0 25 0 1 0 357413405 42795008 9030 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10448 9030 603 41 0 10407 0
vsize: 0

Child status: 30
Real time (s): 1022.46
CPU time (s): 1022.5
CPU user time (s): 1020.98
CPU system time (s): 1.51777
CPU usage (%): 100.004
Max. virtual memory (Kb): 41816
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	167
#### END VERIFIER DATA ####