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-ii32c2.opb
MD5SUM	b78d16df5ec546c41fce5f9f07c0fd92
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	207
Optimality of the best value was proved	NO
Number of terms in the objective function	498
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	498
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	498
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.03184
Number of variables	498
Total number of constraints	2431
Number of constraints which are clauses	2431
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 5483

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        900976 kB
Buffers:         33872 kB
Cached:          78368 kB
SwapCached:       2272 kB
Active:          53888 kB
Inactive:        63448 kB
HighTotal:      131008 kB
HighFree:        48748 kB
LowTotal:       903652 kB
LowFree:        852228 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10704 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:28:45 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3912 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2431 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 |    2431    12171 |     729       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  498/498          
c |         0 |    2431    12171 |     972       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.141978 s)
c ==============================================================================
c [1mFound solution: 232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:18940     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         9 |   25048    65080 |    7514       9      419    46.6 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15145          
c   -- var.elim.:  2000/15145          
c   -- var.elim.:  3000/15145          
c   -- var.elim.:  4000/15145          
c   -- var.elim.:  5000/15145          
c   -- var.elim.:  6000/15145          
c   -- var.elim.:  7000/15145          
c   -- var.elim.:  8000/15145          
c   -- var.elim.:  9000/15145          
c   -- var.elim.:  10000/15145          
c   -- var.elim.:  11000/15145          
c   -- var.elim.:  12000/15145          
c   -- var.elim.:  13000/15145          
c   -- var.elim.:  14000/15145          
c   -- var.elim.:  15000/15145          
c   -- var.elim.:  15145/15145          
c   -- var.elim.:  1000/7419          
c   -- var.elim.:  2000/7419          
c   -- var.elim.:  3000/7419          
c   -- var.elim.:  4000/7419          
c   -- var.elim.:  5000/7419          
c   -- var.elim.:  6000/7419          
c   -- var.elim.:  7000/7419          
c   -- var.elim.:  7419/7419          
c   -- var.elim.:  1000/4388          
c   -- var.elim.:  2000/4388          
c   -- var.elim.:  3000/4388          
c   -- var.elim.:  4000/4388          
c   -- var.elim.:  4388/4388          
c   -- var.elim.:  1000/3064          
c   -- var.elim.:  2000/3064          
c   -- var.elim.:  3000/3064          
c   -- var.elim.:  3064/3064          
c   -- var.elim.:  1000/2340          
c   -- var.elim.:  2000/2340          
c   -- var.elim.:  2340/2340          
c   -- var.elim.:  1000/1706          
c   -- var.elim.:  1706/1706          
c   -- var.elim.:  1000/1291          
c   -- var.elim.:  1291/1291          
c   -- var.elim.:  211/211          
c   -- subsuming                       
c   -- var.elim.:  1000/2141          
c   -- var.elim.:  2000/2141          
c   -- var.elim.:  2141/2141          
c   -- var.elim.:  57/57          
c |         9 |    8229    46119 |      --       9       --      -- |     --   | -16809/-18931
c |         9 |    8229    46119 |    3291       9      419    46.6 |  0.000 % |
c ==============================================================================
c (current CPU-time: 8.10877 s)
c ==============================================================================
c [1mFound solution: 216[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 |        72 |   25216    87664 |    7564      72     4608    64.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15014          
c   -- var.elim.:  2000/15014          
c   -- var.elim.:  3000/15014          
c   -- var.elim.:  4000/15014          
c   -- var.elim.:  5000/15014          
c   -- var.elim.:  6000/15014          
c   -- var.elim.:  7000/15014          
c   -- var.elim.:  8000/15014          
c   -- var.elim.:  9000/15014          
c   -- var.elim.:  10000/15014          
c   -- var.elim.:  11000/15014          
c   -- var.elim.:  12000/15014          
c   -- var.elim.:  13000/15014          
c   -- var.elim.:  14000/15014          
c   -- var.elim.:  15000/15014          
c   -- var.elim.:  15014/15014          
c   -- var.elim.:  1000/7257          
c   -- var.elim.:  2000/7257          
c   -- var.elim.:  3000/7257          
c   -- var.elim.:  4000/7257          
c   -- var.elim.:  5000/7257          
c   -- var.elim.:  6000/7257          
c   -- var.elim.:  7000/7257          
c   -- var.elim.:  7257/7257          
c   -- var.elim.:  1000/4577          
c   -- var.elim.:  2000/4577          
c   -- var.elim.:  3000/4577          
c   -- var.elim.:  4000/4577          
c   -- var.elim.:  4577/4577          
c   -- var.elim.:  1000/3281          
c   -- var.elim.:  2000/3281          
c   -- var.elim.:  3000/3281          
c   -- var.elim.:  3281/3281          
c   -- var.elim.:  1000/2842          
c   -- var.elim.:  2000/2842          
c   -- var.elim.:  2842/2842          
c   -- var.elim.:  1000/2364          
c   -- var.elim.:  2000/2364          
c   -- var.elim.:  2364/2364          
c   -- var.elim.:  1000/2044          
c   -- var.elim.:  2000/2044          
c   -- var.elim.:  2044/2044          
c   -- var.elim.:  548/548          
c   -- var.elim.:  66/66          
c   -- subsuming                       
c   -- var.elim.:  1000/2003          
c   -- var.elim.:  2000/2003          
c   -- var.elim.:  2003/2003          
c   -- var.elim.:  20/20          
c |        72 |    8582    52934 |      --      72       --      -- |     --   | -16623/-34698
c |        72 |    8582    52934 |    3432      72     4608    64.0 |  0.000 % |
c |       172 |    8582    52934 |    3776     172    12323    71.6 |  0.691 % |
c |       322 |    8582    52934 |    4153     322    48843   151.7 |  0.691 % |
c |       548 |    8509    52420 |    4530     544   114338   210.2 |  1.533 % |
c |       885 |    8447    51980 |    4946     878   175361   199.7 |  2.284 % |
c |      1392 |    8294    51028 |    5343    1378   400459   290.6 |  4.147 % |
c |      2152 |    8249    50712 |    5845    2134   742855   348.1 |  4.748 % |
c ==============================================================================
c (current CPU-time: 21.1098 s)
c ==============================================================================
c [1mFound solution: 214[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 |      2222 |   23892    88866 |    7167    2203   754142   342.3 |  4.748 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14173          
c   -- var.elim.:  2000/14173          
c   -- var.elim.:  3000/14173          
c   -- var.elim.:  4000/14173          
c   -- var.elim.:  5000/14173          
c   -- var.elim.:  6000/14173          
c   -- var.elim.:  7000/14173          
c   -- var.elim.:  8000/14173          
c   -- var.elim.:  9000/14173          
c   -- var.elim.:  10000/14173          
c   -- var.elim.:  11000/14173          
c   -- var.elim.:  12000/14173          
c   -- var.elim.:  13000/14173          
c   -- var.elim.:  14000/14173          
c   -- var.elim.:  14173/14173          
c   -- var.elim.:  1000/6744          
c   -- var.elim.:  2000/6744          
c   -- var.elim.:  3000/6744          
c   -- var.elim.:  4000/6744          
c   -- var.elim.:  5000/6744          
c   -- var.elim.:  6000/6744          
c   -- var.elim.:  6744/6744          
c   -- var.elim.:  1000/4181          
c   -- var.elim.:  2000/4181          
c   -- var.elim.:  3000/4181          
c   -- var.elim.:  4000/4181          
c   -- var.elim.:  4181/4181          
c   -- var.elim.:  1000/2994          
c   -- var.elim.:  2000/2994          
c   -- var.elim.:  2994/2994          
c   -- var.elim.:  1000/2425          
c   -- var.elim.:  2000/2425          
c   -- var.elim.:  2425/2425          
c   -- var.elim.:  1000/2251          
c   -- var.elim.:  2000/2251          
c   -- var.elim.:  2251/2251          
c   -- var.elim.:  1000/1576          
c   -- var.elim.:  1576/1576          
c   -- var.elim.:  768/768          
c   -- subsuming                       
c   -- var.elim.:  1000/1716          
c   -- var.elim.:  1716/1716          
c   -- var.elim.:  27/27          
c |      2222 |    8280    51966 |      --    2203       --      -- |     --   | -15565/-36394
c |      2222 |    8280    51966 |    3312    2203   754142   342.3 |  4.748 % |
c |      2327 |    8255    51781 |    3632    1012    85905    84.9 |  8.580 % |
c |      2479 |    8255    51781 |    3995    1164   145840   125.3 |  8.580 % |
c |      2704 |    8249    51746 |    4391    1388   234061   168.6 |  8.638 % |
c |      3041 |    8203    51396 |    4804    1722   300200   174.3 |  9.214 % |
c |      3550 |    8147    50573 |    5248    2229   445404   199.8 |  9.675 % |
c |      4311 |    8147    50573 |    5773    2990   701542   234.6 |  9.675 % |
c |      5454 |    8124    50328 |    6332    4132   887209   214.7 |  9.934 % |
c |      7162 |    7984    49329 |    6845    5833  1338440   229.5 | 11.604 % |
c |      9726 |    7984    49329 |    7530    5831   828032   142.0 | 11.604 % |
c |     13571 |    7824    48145 |    8117    6901  1540131   223.2 | 13.591 % |
c |     19342 |    7762    47695 |    8858    9623  4011129   416.8 | 14.368 % |
c ==============================================================================
c (current CPU-time: 95.7274 s)
c ==============================================================================
c [1mFound solution: 210[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 |     27251 |   22675    82136 |    6802    7819  2789983   356.8 | 14.368 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13449          
c   -- var.elim.:  2000/13449          
c   -- var.elim.:  3000/13449          
c   -- var.elim.:  4000/13449          
c   -- var.elim.:  5000/13449          
c   -- var.elim.:  6000/13449          
c   -- var.elim.:  7000/13449          
c   -- var.elim.:  8000/13449          
c   -- var.elim.:  9000/13449          
c   -- var.elim.:  10000/13449          
c   -- var.elim.:  11000/13449          
c   -- var.elim.:  12000/13449          
c   -- var.elim.:  13000/13449          
c   -- var.elim.:  13449/13449          
c   -- var.elim.:  1000/6241          
c   -- var.elim.:  2000/6241          
c   -- var.elim.:  3000/6241          
c   -- var.elim.:  4000/6241          
c   -- var.elim.:  5000/6241          
c   -- var.elim.:  6000/6241          
c   -- var.elim.:  6241/6241          
c   -- var.elim.:  1000/3743          
c   -- var.elim.:  2000/3743          
c   -- var.elim.:  3000/3743          
c   -- var.elim.:  3743/3743          
c   -- var.elim.:  1000/2559          
c   -- var.elim.:  2000/2559          
c   -- var.elim.:  2559/2559          
c   -- var.elim.:  1000/2085          
c   -- var.elim.:  2000/2085          
c   -- var.elim.:  2085/2085          
c   -- var.elim.:  1000/1856          
c   -- var.elim.:  1856/1856          
c   -- var.elim.:  1000/1257          
c   -- var.elim.:  1257/1257          
c   -- var.elim.:  79/79          
c   -- subsuming                       
c   -- var.elim.:  1000/1605          
c   -- var.elim.:  1605/1605          
c   -- var.elim.:  15/15          
c |     27251 |    7479    46643 |      --    7819       --      -- |     --   | -15084/-34622
c |     27251 |    7479    46643 |    2991    2845   129529    45.5 | 14.368 % |
c |     27351 |    7479    46643 |    3290    2945   145647    49.5 | 27.901 % |
c |     27502 |    7479    46643 |    3619    3096   181317    58.6 | 27.901 % |
c |     27728 |    7460    46487 |    3971    3321   253137    76.2 | 28.131 % |
c |     28067 |    7437    46292 |    4355    3657   342922    93.8 | 28.386 % |
c |     28574 |    7416    46144 |    4777    4163   468618   112.6 | 28.615 % |
c |     29333 |    7291    45024 |    5166    4914   702928   143.0 | 30.069 % |
c |     30472 |    7291    45024 |    5683    6053  1230814   203.3 | 30.069 % |
c |     32186 |    7291    45024 |    6251    5203  1655251   318.1 | 30.069 % |
c |     34753 |    7227    44513 |    6816    7767  2822379   363.4 | 30.758 % |
c |     38597 |    6692    40352 |    6942    6090  2041762   335.3 | 36.725 % |
c |     44364 |    6655    40043 |    7594    8613  2956015   343.2 | 37.108 % |
c ==============================================================================
c (current CPU-time: 166.375 s)
c ==============================================================================
c [1mFound solution: 209[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 |     50530 |   20462    72921 |    6138    8527  2502312   293.5 | 37.108 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12089          
c   -- var.elim.:  2000/12089          
c   -- var.elim.:  3000/12089          
c   -- var.elim.:  4000/12089          
c   -- var.elim.:  5000/12089          
c   -- var.elim.:  6000/12089          
c   -- var.elim.:  7000/12089          
c   -- var.elim.:  8000/12089          
c   -- var.elim.:  9000/12089          
c   -- var.elim.:  10000/12089          
c   -- var.elim.:  11000/12089          
c   -- var.elim.:  12000/12089          
c   -- var.elim.:  12089/12089          
c   -- var.elim.:  1000/5421          
c   -- var.elim.:  2000/5421          
c   -- var.elim.:  3000/5421          
c   -- var.elim.:  4000/5421          
c   -- var.elim.:  5000/5421          
c   -- var.elim.:  5421/5421          
c   -- var.elim.:  1000/3168          
c   -- var.elim.:  2000/3168          
c   -- var.elim.:  3000/3168          
c   -- var.elim.:  3168/3168          
c   -- var.elim.:  1000/2112          
c   -- var.elim.:  2000/2112          
c   -- var.elim.:  2112/2112          
c   -- var.elim.:  1000/1584          
c   -- var.elim.:  1584/1584          
c   -- var.elim.:  1000/1123          
c   -- var.elim.:  1123/1123          
c   -- var.elim.:  723/723          
c   -- var.elim.:  166/166          
c   -- subsuming                       
c   -- var.elim.:  828/828          
c   -- var.elim.:  10/10          
c |     50530 |    6634    40279 |      --    8527       --      -- |     --   | -13767/-32519
c |     50530 |    6634    40279 |    2653    3078   147410    47.9 | 37.108 % |
c |     50630 |    6634    40279 |    2918    3178   171679    54.0 | 42.985 % |
c |     50780 |    6598    39949 |    3193    3321   206708    62.2 | 43.383 % |
c |     51005 |    6598    39949 |    3512    3546   257590    72.6 | 43.384 % |
c |     51342 |    6307    37687 |    3693    3873   334975    86.5 | 46.504 % |
c |     51849 |    6273    37418 |    4041    4379   461394   105.4 | 46.879 % |
c |     52609 |    6273    37418 |    4445    5139   722193   140.5 | 46.879 % |
c |     53748 |    6271    37412 |    4888    6277  1101259   175.4 | 46.903 % |
c |     55456 |    6271    37412 |    5376    5513  1372258   248.9 | 46.903 % |
c |     58019 |    6271    37412 |    5914    5473  1437045   262.6 | 46.904 % |
c |     61864 |    6271    37412 |    6506    6451  1704265   264.2 | 46.903 % |
c ==============================================================================
c (current CPU-time: 197.093 s)
c ==============================================================================
c [1mFound solution: 208[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 |     63409 |   16362    61567 |    4908    7996  2259076   282.5 | 46.903 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9174          
c   -- var.elim.:  2000/9174          
c   -- var.elim.:  3000/9174          
c   -- var.elim.:  4000/9174          
c   -- var.elim.:  5000/9174          
c   -- var.elim.:  6000/9174          
c   -- var.elim.:  7000/9174          
c   -- var.elim.:  8000/9174          
c   -- var.elim.:  9000/9174          
c   -- var.elim.:  9174/9174          
c   -- var.elim.:  1000/3959          
c   -- var.elim.:  2000/3959          
c   -- var.elim.:  3000/3959          
c   -- var.elim.:  3959/3959          
c   -- var.elim.:  1000/2276          
c   -- var.elim.:  2000/2276          
c   -- var.elim.:  2276/2276          
c   -- var.elim.:  1000/1197          
c   -- var.elim.:  1197/1197          
c   -- var.elim.:  873/873          
c   -- var.elim.:  523/523          
c   -- var.elim.:  32/32          
c   -- subsuming                       
c   -- var.elim.:  496/496          
c   -- var.elim.:  5/5          
c |     63409 |    6245    36178 |      --    7996       --      -- |     --   | -10068/-24421
c |     63409 |    6245    36178 |    2498    4573   513554   112.3 | 46.903 % |
c |     63509 |    6245    36178 |    2747    4673   548409   117.4 | 47.772 % |
c |     63659 |    6245    36178 |    3022    4823   596351   123.6 | 47.772 % |
c |     63889 |    6245    36178 |    3324    5053   672495   133.1 | 47.772 % |
c |     64227 |    6245    36178 |    3657    5391   808413   150.0 | 47.772 % |
c |     64733 |    6245    36178 |    4023    5897  1014598   172.1 | 47.772 % |
c |     65492 |    6245    36178 |    4425    6656  1285958   193.2 | 47.772 % |
c |     66631 |    6245    36178 |    4867    5577  1487128   266.7 | 47.772 % |
c |     68340 |    6245    36178 |    5354    7286  2316483   317.9 | 47.772 % |
c |     70902 |    6245    36178 |    5890    7105  2402178   338.1 | 47.772 % |
c |     74747 |    6245    36178 |    6479    8059  2391509   296.8 | 47.772 % |
c |     80513 |    6208    35881 |    7084    7564  2475090   327.2 | 48.113 % |
c |     89164 |    6044    34619 |    7587    9705  2863771   295.1 | 49.727 % |
c |    102143 |    6004    34293 |    8290    8669  2956587   341.1 | 50.136 % |
c |    121604 |    6004    34293 |    9120    9301  2667342   286.8 | 50.136 % |
c |    150797 |    6004    34293 |   10032   10422  3409151   327.1 | 50.136 % |
c |    194586 |    6004    34293 |   11035   10943  3636951   332.4 | 50.136 % |
c |    260270 |    5853    33176 |   11833   10979  2893286   263.5 | 51.523 % |
c |    358796 |    5806    32801 |   12912   11534  3003022   260.4 | 51.978 % |
c 
c *** TERMINATED ***
s SATISFIABLE
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 x3#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 27570
Raw data (stat): 27570 (runsolver) R 27569 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421932905 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99974 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 3290 0 0 0 980 18 0 0 25 0 1 0 421932905 14991360 3085 4294967295 134512640 134672761 3221224576 3221223024 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3660 3085 603 41 0 3619 0
vsize: 14640
[startup+20 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 3678 0 0 0 1976 22 0 0 25 0 1 0 421932905 16412672 3448 4294967295 134512640 134672761 3221224576 3221223492 1074972064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3448 603 41 0 3966 0
vsize: 16028
[startup+30.0005 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 5882 0 0 0 2962 35 0 0 25 0 1 0 421932905 24551424 5158 4294967295 134512640 134672761 3221224576 3221223024 134643768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5994 5158 603 41 0 5953 0
vsize: 23976
[startup+40 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 5883 0 0 0 3962 35 0 0 25 0 1 0 421932905 24551424 5159 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5994 5159 603 41 0 5953 0
vsize: 23976
[startup+50.001 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 6158 0 0 0 4961 36 0 0 25 0 1 0 421932905 25653248 5434 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5434 603 41 0 6222 0
vsize: 25052
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 7150 0 0 0 5959 38 0 0 25 0 1 0 421932905 29650944 6426 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7239 6426 603 41 0 7198 0
vsize: 28956
[startup+70.0002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 8650 0 0 0 6955 42 0 0 25 0 1 0 421932905 35819520 7926 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8745 7926 603 41 0 8704 0
vsize: 34980
[startup+80.0012 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 8831 0 0 0 7955 43 0 0 25 0 1 0 421932905 36605952 8107 4294967295 134512640 134672761 3221224576 3221223720 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8107 603 41 0 8896 0
vsize: 35748
[startup+90.001 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 8910 0 0 0 8955 43 0 0 25 0 1 0 421932905 36868096 8186 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9001 8186 603 41 0 8960 0
vsize: 36004
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10450 0 0 0 9944 54 0 0 25 0 1 0 421932905 37056512 8382 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9047 8382 603 41 0 9006 0
vsize: 36188
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10450 0 0 0 10941 57 0 0 25 0 1 0 421932905 37048320 8380 4294967295 134512640 134672761 3221224576 3221223568 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9045 8380 603 41 0 9004 0
vsize: 36180
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10450 0 0 0 11941 57 0 0 25 0 1 0 421932905 37048320 8380 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9045 8380 603 41 0 9004 0
vsize: 36180
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10450 0 0 0 12941 57 0 0 25 0 1 0 421932905 37048320 8380 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9045 8380 603 41 0 9004 0
vsize: 36180
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10451 0 0 0 13942 57 0 0 25 0 1 0 421932905 37048320 8381 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9045 8381 603 41 0 9004 0
vsize: 36180
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10451 0 0 0 14942 57 0 0 25 0 1 0 421932905 37048320 8381 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9045 8381 603 41 0 9004 0
vsize: 36180
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 10451 0 0 0 15941 57 0 0 25 0 1 0 421932905 37048320 8381 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9045 8381 603 41 0 9004 0
vsize: 36180
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 12845 0 0 0 16927 70 0 0 25 0 1 0 421932905 37093376 8515 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9056 8515 603 41 0 9015 0
vsize: 36224
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 12845 0 0 0 17926 72 0 0 25 0 1 0 421932905 37093376 8515 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9056 8515 603 41 0 9015 0
vsize: 36224
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 12845 0 0 0 18926 72 0 0 25 0 1 0 421932905 37093376 8515 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9056 8515 603 41 0 9015 0
vsize: 36224
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 19909 89 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221222992 134631613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 20906 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 21906 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 22906 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 23907 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 24907 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 25907 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16588 0 0 0 26907 92 0 0 25 0 1 0 421932905 43950080 9078 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9078 603 41 0 10689 0
vsize: 42920
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16589 0 0 0 27907 92 0 0 25 0 1 0 421932905 43950080 9079 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9079 603 41 0 10689 0
vsize: 42920
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16694 0 0 0 28907 92 0 0 25 0 1 0 421932905 44457984 9184 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10854 9184 603 41 0 10813 0
vsize: 43416
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16694 0 0 0 29907 92 0 0 25 0 1 0 421932905 44457984 9184 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10854 9184 603 41 0 10813 0
vsize: 43416
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16953 0 0 0 30907 93 0 0 25 0 1 0 421932905 45506560 9443 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11110 9443 603 41 0 11069 0
vsize: 44440
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16953 0 0 0 31907 93 0 0 25 0 1 0 421932905 45506560 9443 4294967295 134512640 134672761 3221224576 3221223760 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11110 9443 603 41 0 11069 0
vsize: 44440
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16954 0 0 0 32907 93 0 0 25 0 1 0 421932905 45494272 9444 4294967295 134512640 134672761 3221224576 3221223672 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11107 9444 603 41 0 11066 0
vsize: 44428
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16954 0 0 0 33907 93 0 0 25 0 1 0 421932905 45494272 9444 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11107 9444 603 41 0 11066 0
vsize: 44428
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16954 0 0 0 34907 93 0 0 25 0 1 0 421932905 45490176 9444 4294967295 134512640 134672761 3221224576 3221223672 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11106 9444 603 41 0 11065 0
vsize: 44424
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16954 0 0 0 35908 93 0 0 25 0 1 0 421932905 45490176 9444 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11106 9444 603 41 0 11065 0
vsize: 44424
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16954 0 0 0 36908 93 0 0 25 0 1 0 421932905 45490176 9444 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11106 9444 603 41 0 11065 0
vsize: 44424
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 16955 0 0 0 37908 93 0 0 25 0 1 0 421932905 45490176 9445 4294967295 134512640 134672761 3221224576 3221223808 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11106 9445 603 41 0 11065 0
vsize: 44424
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17011 0 0 0 38908 93 0 0 25 0 1 0 421932905 45748224 9501 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11169 9501 603 41 0 11128 0
vsize: 44676
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17015 0 0 0 39908 93 0 0 25 0 1 0 421932905 45748224 9505 4294967295 134512640 134672761 3221224576 3221223408 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11169 9505 603 41 0 11128 0
vsize: 44676
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17015 0 0 0 40908 93 0 0 25 0 1 0 421932905 45748224 9505 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11169 9505 603 41 0 11128 0
vsize: 44676
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17015 0 0 0 41908 93 0 0 25 0 1 0 421932905 45748224 9505 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11169 9505 603 41 0 11128 0
vsize: 44676
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17015 0 0 0 42909 93 0 0 25 0 1 0 421932905 45748224 9505 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11169 9505 603 41 0 11128 0
vsize: 44676
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17065 0 0 0 43909 94 0 0 25 0 1 0 421932905 46006272 9555 4294967295 134512640 134672761 3221224576 3221223616 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11232 9555 603 41 0 11191 0
vsize: 44928
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17289 0 0 0 44909 94 0 0 25 0 1 0 421932905 46882816 9779 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11446 9779 603 41 0 11405 0
vsize: 45784
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17412 0 0 0 45908 95 0 0 25 0 1 0 421932905 47386624 9902 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11569 9902 603 41 0 11528 0
vsize: 46276
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17445 0 0 0 46908 95 0 0 25 0 1 0 421932905 47517696 9935 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11601 9935 603 41 0 11560 0
vsize: 46404
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17666 0 0 0 47908 95 0 0 25 0 1 0 421932905 48418816 10156 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10156 603 41 0 11780 0
vsize: 47284
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17666 0 0 0 48908 95 0 0 25 0 1 0 421932905 48418816 10156 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10156 603 41 0 11780 0
vsize: 47284
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17666 0 0 0 49908 95 0 0 25 0 1 0 421932905 48418816 10156 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10156 603 41 0 11780 0
vsize: 47284
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 50908 95 0 0 25 0 1 0 421932905 48418816 10162 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10162 603 41 0 11780 0
vsize: 47284
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 51909 95 0 0 25 0 1 0 421932905 48418816 10162 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10162 603 41 0 11780 0
vsize: 47284
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 52909 95 0 0 25 0 1 0 421932905 48418816 10162 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10162 603 41 0 11780 0
vsize: 47284
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 53909 95 0 0 25 0 1 0 421932905 48418816 10162 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10162 603 41 0 11780 0
vsize: 47284
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 54909 95 0 0 25 0 1 0 421932905 48418816 10162 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10162 603 41 0 11780 0
vsize: 47284
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 55909 95 0 0 25 0 1 0 421932905 48418816 10162 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10162 603 41 0 11780 0
vsize: 47284
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 56909 95 0 0 25 0 1 0 421932905 48414720 10162 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11820 10162 603 41 0 11779 0
vsize: 47280
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 57910 95 0 0 25 0 1 0 421932905 48414720 10162 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11820 10162 603 41 0 11779 0
vsize: 47280
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17672 0 0 0 58910 95 0 0 25 0 1 0 421932905 48414720 10162 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11820 10162 603 41 0 11779 0
vsize: 47280
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 59909 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 60910 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 61910 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 62910 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 63910 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 64910 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223616 134612799 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 65910 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 66911 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+680.013 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 67911 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+690.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 68911 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+700.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 69911 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+710.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 70912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+720.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 71912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+730.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 72912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+740.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 73912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+750.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 74912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+760.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 75912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+770.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 76912 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+780.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17933 0 0 0 77913 96 0 0 25 0 1 0 421932905 49475584 10423 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10423 603 41 0 12038 0
vsize: 48316
[startup+790.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17934 0 0 0 78913 96 0 0 25 0 1 0 421932905 49475584 10424 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10424 603 41 0 12038 0
vsize: 48316
[startup+800.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17934 0 0 0 79913 96 0 0 25 0 1 0 421932905 49475584 10424 4294967295 134512640 134672761 3221224576 3221223760 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10424 603 41 0 12038 0
vsize: 48316
[startup+810.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 17934 0 0 0 80913 96 0 0 25 0 1 0 421932905 49475584 10424 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 10424 603 41 0 12038 0
vsize: 48316
[startup+820.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18291 0 0 0 81913 97 0 0 25 0 1 0 421932905 50933760 10781 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12435 10781 603 41 0 12394 0
vsize: 49740
[startup+830.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 82912 97 0 0 25 0 1 0 421932905 51269632 10855 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12517 10855 603 41 0 12476 0
vsize: 50068
[startup+840.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 83913 97 0 0 25 0 1 0 421932905 51269632 10855 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12517 10855 603 41 0 12476 0
vsize: 50068
[startup+850.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 84913 97 0 0 25 0 1 0 421932905 51269632 10855 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12517 10855 603 41 0 12476 0
vsize: 50068
[startup+860.019 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 85913 97 0 0 25 0 1 0 421932905 51154944 10842 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12489 10842 603 41 0 12448 0
vsize: 49956
[startup+870.018 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 86913 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+880.019 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 87913 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+890.019 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 88914 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+900.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 89914 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+910.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 90914 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223700 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+920.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 91914 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+930.021 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 92914 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+940.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 93915 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+950.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 94915 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+960.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 95915 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+970.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 96915 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+980.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 97915 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+990.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 98915 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 99916 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 100916 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 101916 97 0 0 25 0 1 0 421932905 51109888 10831 4294967295 134512640 134672761 3221224576 3221223616 134612533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12478 10831 603 41 0 12437 0
vsize: 49912
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18365 0 0 0 102916 97 0 0 25 0 1 0 421932905 51105792 10830 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10830 603 41 0 12436 0
vsize: 49908
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18366 0 0 0 103916 97 0 0 25 0 1 0 421932905 51105792 10831 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10831 603 41 0 12436 0
vsize: 49908
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18366 0 0 0 104917 97 0 0 25 0 1 0 421932905 51105792 10831 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10831 603 41 0 12436 0
vsize: 49908
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18366 0 0 0 105917 97 0 0 25 0 1 0 421932905 51105792 10831 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10831 603 41 0 12436 0
vsize: 49908
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18366 0 0 0 106917 97 0 0 25 0 1 0 421932905 51105792 10831 4294967295 134512640 134672761 3221224576 3221223760 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10831 603 41 0 12436 0
vsize: 49908
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18366 0 0 0 107917 97 0 0 25 0 1 0 421932905 51105792 10831 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10831 603 41 0 12436 0
vsize: 49908
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18367 0 0 0 108917 97 0 0 25 0 1 0 421932905 51105792 10832 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10832 603 41 0 12436 0
vsize: 49908
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18367 0 0 0 109918 97 0 0 25 0 1 0 421932905 51105792 10832 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10832 603 41 0 12436 0
vsize: 49908
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18367 0 0 0 110918 97 0 0 25 0 1 0 421932905 51105792 10832 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10832 603 41 0 12436 0
vsize: 49908
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18367 0 0 0 111918 97 0 0 25 0 1 0 421932905 51105792 10832 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12477 10832 603 41 0 12436 0
vsize: 49908
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 112918 98 0 0 25 0 1 0 421932905 52142080 11069 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12730 11069 603 41 0 12689 0
vsize: 50920
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 113918 98 0 0 25 0 1 0 421932905 52142080 11069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12730 11069 603 41 0 12689 0
vsize: 50920
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 114918 98 0 0 25 0 1 0 421932905 52142080 11069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12730 11069 603 41 0 12689 0
vsize: 50920
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 115918 98 0 0 25 0 1 0 421932905 52133888 11069 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12728 11069 603 41 0 12687 0
vsize: 50912
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 116918 98 0 0 25 0 1 0 421932905 52133888 11069 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12728 11069 603 41 0 12687 0
vsize: 50912
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 117918 98 0 0 25 0 1 0 421932905 52133888 11069 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12728 11069 603 41 0 12687 0
vsize: 50912
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 118919 98 0 0 25 0 1 0 421932905 52133888 11069 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12728 11069 603 41 0 12687 0
vsize: 50912
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27570
Raw data (stat): 27570 (minisat+) R 27569 24215 24214 0 -1 0 18604 0 0 0 119919 98 0 0 25 0 1 0 421932905 52133888 11069 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12728 11069 603 41 0 12687 0
vsize: 50912
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 27570
Raw data (stat): 27570 (minisat+) Z 27569 24215 24214 0 -1 12 18605 0 0 0 119919 102 0 0 25 0 1 0 421932905 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.19
CPU system time (s): 1.02084
CPU usage (%): 100.013
Max. virtual memory (Kb): 50920
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####