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/synthesis-ptl-cmos-circuits/normalized-9symml.opb
MD5SUM	48809ba02390b1184dab90aed89aff8e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4517
Optimality of the best value was proved	NO
Number of terms in the objective function	651
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	28138
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	28138
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	651
Total number of constraints	1658
Number of constraints which are clauses	1656
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 5588

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 00:37:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4006 boxname=wulflinc22 idbench=246 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  48809ba02390b1184dab90aed89aff8e  /oldhome/oroussel/tmp/wulflinc22/normalized-9symml.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc22/normalized-9symml.opb /oldhome/oroussel/tmp/wulflinc22/normalized-9symml.opb
IDLAUNCH: 4006
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        854840 kB
Buffers:         31876 kB
Cached:         104960 kB
SwapCached:        524 kB
Active:          47964 kB
Inactive:        92252 kB
HighTotal:      131008 kB
HighFree:        22344 kB
LowTotal:       903652 kB
LowFree:        832496 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34084 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:57:38 (client local time) WITH STATUS 10 IN 1210.08 SECONDS
stats: 4006 7 1210.08 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1579 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 |    1516     6410 |     454       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  568/568          
c |         0 |    1439     6111 |      --       0       --      -- |     --   | -77/-299
c |         0 |    1439     6111 |     575       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.074988 s)
c ==============================================================================
c [1mFound solution: 6227[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:101537     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  240527   564352 |   72158       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/92516          
c   -- var.elim.:  2000/92516          
c   -- var.elim.:  3000/92516          
c   -- var.elim.:  4000/92516          
c   -- var.elim.:  5000/92516          
c   -- var.elim.:  6000/92516          
c   -- var.elim.:  7000/92516          
c   -- var.elim.:  8000/92516          
c   -- var.elim.:  9000/92516          
c   -- var.elim.:  10000/92516          
c   -- var.elim.:  11000/92516          
c   -- var.elim.:  12000/92516          
c   -- var.elim.:  13000/92516          
c   -- var.elim.:  14000/92516          
c   -- var.elim.:  15000/92516          
c   -- var.elim.:  16000/92516          
c   -- var.elim.:  17000/92516          
c   -- var.elim.:  18000/92516          
c   -- var.elim.:  19000/92516          
c   -- var.elim.:  20000/92516          
c   -- var.elim.:  21000/92516          
c   -- var.elim.:  22000/92516          
c   -- var.elim.:  23000/92516          
c   -- var.elim.:  24000/92516          
c   -- var.elim.:  25000/92516          
c   -- var.elim.:  26000/92516          
c   -- var.elim.:  27000/92516          
c   -- var.elim.:  28000/92516          
c   -- var.elim.:  29000/92516          
c   -- var.elim.:  30000/92516          
c   -- var.elim.:  31000/92516          
c   -- var.elim.:  32000/92516          
c   -- var.elim.:  33000/92516          
c   -- var.elim.:  34000/92516          
c   -- var.elim.:  35000/92516          
c   -- var.elim.:  36000/92516          
c   -- var.elim.:  37000/92516          
c   -- var.elim.:  38000/92516          
c   -- var.elim.:  39000/92516          
c   -- var.elim.:  40000/92516          
c   -- var.elim.:  41000/92516          
c   -- var.elim.:  42000/92516          
c   -- var.elim.:  43000/92516          
c   -- var.elim.:  44000/92516          
c   -- var.elim.:  45000/92516          
c   -- var.elim.:  46000/92516          
c   -- var.elim.:  47000/92516          
c   -- var.elim.:  48000/92516          
c   -- var.elim.:  49000/92516          
c   -- var.elim.:  50000/92516          
c   -- var.elim.:  51000/92516          
c   -- var.elim.:  52000/92516          
c   -- var.elim.:  53000/92516          
c   -- var.elim.:  54000/92516          
c   -- var.elim.:  55000/92516          
c   -- var.elim.:  56000/92516          
c   -- var.elim.:  57000/92516          
c   -- var.elim.:  58000/92516          
c   -- var.elim.:  59000/92516          
c   -- var.elim.:  60000/92516          
c   -- var.elim.:  61000/92516          
c   -- var.elim.:  62000/92516          
c   -- var.elim.:  63000/92516          
c   -- var.elim.:  64000/92516          
c   -- var.elim.:  65000/92516          
c   -- var.elim.:  66000/92516          
c   -- var.elim.:  67000/92516          
c   -- var.elim.:  68000/92516          
c   -- var.elim.:  69000/92516          
c   -- var.elim.:  70000/92516          
c   -- var.elim.:  71000/92516          
c   -- var.elim.:  72000/92516          
c   -- var.elim.:  73000/92516          
c   -- var.elim.:  74000/92516          
c   -- var.elim.:  75000/92516          
c   -- var.elim.:  76000/92516          
c   -- var.elim.:  77000/92516          
c   -- var.elim.:  78000/92516          
c   -- var.elim.:  79000/92516          
c   -- var.elim.:  80000/92516          
c   -- var.elim.:  81000/92516          
c   -- var.elim.:  82000/92516          
c   -- var.elim.:  83000/92516          
c   -- var.elim.:  84000/92516          
c   -- var.elim.:  85000/92516          
c   -- var.elim.:  86000/92516          
c   -- var.elim.:  87000/92516          
c   -- var.elim.:  88000/92516          
c   -- var.elim.:  89000/92516          
c   -- var.elim.:  90000/92516          
c   -- var.elim.:  91000/92516          
c   -- var.elim.:  92000/92516          
c   -- var.elim.:  92516/92516          
c   -- var.elim.:  1000/49356          
c   -- var.elim.:  2000/49356          
c   -- var.elim.:  3000/49356          
c   -- var.elim.:  4000/49356          
c   -- var.elim.:  5000/49356          
c   -- var.elim.:  6000/49356          
c   -- var.elim.:  7000/49356          
c   -- var.elim.:  8000/49356          
c   -- var.elim.:  9000/49356          
c   -- var.elim.:  10000/49356          
c   -- var.elim.:  11000/49356          
c   -- var.elim.:  12000/49356          
c   -- var.elim.:  13000/49356          
c   -- var.elim.:  14000/49356          
c   -- var.elim.:  15000/49356          
c   -- var.elim.:  16000/49356          
c   -- var.elim.:  17000/49356          
c   -- var.elim.:  18000/49356          
c   -- var.elim.:  19000/49356          
c   -- var.elim.:  20000/49356          
c   -- var.elim.:  21000/49356          
c   -- var.elim.:  22000/49356          
c   -- var.elim.:  23000/49356          
c   -- var.elim.:  24000/49356          
c   -- var.elim.:  25000/49356          
c   -- var.elim.:  26000/49356          
c   -- var.elim.:  27000/49356          
c   -- var.elim.:  28000/49356          
c   -- var.elim.:  29000/49356          
c   -- var.elim.:  30000/49356          
c   -- var.elim.:  31000/49356          
c   -- var.elim.:  32000/49356          
c   -- var.elim.:  33000/49356          
c   -- var.elim.:  34000/49356          
c   -- var.elim.:  35000/49356          
c   -- var.elim.:  36000/49356          
c   -- var.elim.:  37000/49356          
c   -- var.elim.:  38000/49356          
c   -- var.elim.:  39000/49356          
c   -- var.elim.:  40000/49356          
c   -- var.elim.:  41000/49356          
c   -- var.elim.:  42000/49356          
c   -- var.elim.:  43000/49356          
c   -- var.elim.:  44000/49356          
c   -- var.elim.:  45000/49356          
c   -- var.elim.:  46000/49356          
c   -- var.elim.:  47000/49356          
c   -- var.elim.:  48000/49356          
c   -- var.elim.:  49000/49356          
c   -- var.elim.:  49356/49356          
c   -- var.elim.:  47/47          
c   -- subsuming                       
c   -- var.elim.:  1000/12691          
c   -- var.elim.:  2000/12691          
c   -- var.elim.:  3000/12691          
c   -- var.elim.:  4000/12691          
c   -- var.elim.:  5000/12691          
c   -- var.elim.:  6000/12691          
c   -- var.elim.:  7000/12691          
c   -- var.elim.:  8000/12691          
c   -- var.elim.:  9000/12691          
c   -- var.elim.:  10000/12691          
c   -- var.elim.:  11000/12691          
c   -- var.elim.:  12000/12691          
c   -- var.elim.:  12691/12691          
c   -- var.elim.:  1000/1531          
c   -- var.elim.:  1531/1531          
c   -- subsuming                       
c   -- var.elim.:  480/480          
c |         0 |  211908   761726 |      --       0       --      -- |     --   | -28619/197375
c |         0 |  211908   761726 |   84763       0        0     nan |  0.000 % |
c |       101 |  211512   759631 |   93065      99      933     9.4 |  0.156 % |
c |       252 |  211512   759631 |  102371     250     1829     7.3 |  0.156 % |
c |       477 |  211512   759631 |  112608     475     3487     7.3 |  0.156 % |
c |       815 |  211512   759631 |  123869     813    18883    23.2 |  0.156 % |
c |      1321 |  211043   757601 |  135954    1318    26733    20.3 |  0.278 % |
c |      2081 |  210453   755446 |  149132    2075    34234    16.5 |  0.488 % |
c |      3220 |  210363   755158 |  163975    3209    43851    13.7 |  0.520 % |
c |      4931 |  209747   752959 |  179844    4912   315936    64.3 |  0.721 % |
c |      7497 |  209660   752568 |  197746    7476   432871    57.9 |  0.766 % |
c |     11342 |  209106   750755 |  216946   11307   543581    48.1 |  0.949 % |
c |     17108 |  209075   750475 |  238606   17061   776049    45.5 |  0.979 % |
c |     25758 |  208832   748769 |  262161   25699  1178444    45.9 |  1.063 % |
c |     38732 |  208832   748769 |  288377   38673  1856547    48.0 |  1.063 % |
c |     58194 |  208832   748769 |  317215   58135  4593732    79.0 |  1.063 % |
c |     87386 |  208783   748604 |  348855   87326  6644963    76.1 |  1.083 % |
c |    131177 |  208364   746970 |  382970  131106  9944110    75.8 |  1.268 % |
c |    196861 |  208159   745055 |  420853  196775 36431068   185.1 |  1.325 % |
c ==============================================================================
c (current CPU-time: 1095.34 s)
c ==============================================================================
c [1mFound solution: 6094[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:81756     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    201848 |  413916  1228936 |  124174  201762 36711695   182.0 |  1.325 % |
c   -- subsuming                       
c   -- var.elim.:  1000/90543          
c   -- var.elim.:  2000/90543          
c   -- var.elim.:  3000/90543          
c   -- var.elim.:  4000/90543          
c   -- var.elim.:  5000/90543          
c   -- var.elim.:  6000/90543          
c   -- var.elim.:  7000/90543          
c   -- var.elim.:  8000/90543          
c   -- var.elim.:  9000/90543          
c   -- var.elim.:  10000/90543          
c   -- var.elim.:  11000/90543          
c   -- var.elim.:  12000/90543          
c   -- var.elim.:  13000/90543          
c   -- var.elim.:  14000/90543          
c   -- var.elim.:  15000/90543          
c   -- var.elim.:  16000/90543          
c   -- var.elim.:  17000/90543          
c   -- var.elim.:  18000/90543          
c   -- var.elim.:  19000/90543          
c   -- var.elim.:  20000/90543          
c   -- var.elim.:  21000/90543          
c   -- var.elim.:  22000/90543          
c   -- var.elim.:  23000/90543          
c   -- var.elim.:  24000/90543          
c   -- var.elim.:  25000/90543          
c   -- var.elim.:  26000/90543          
c   -- var.elim.:  27000/90543          
c   -- var.elim.:  28000/90543          
c   -- var.elim.:  29000/90543          
c   -- var.elim.:  30000/90543          
c   -- var.elim.:  31000/90543          
c   -- var.elim.:  32000/90543          
c   -- var.elim.:  33000/90543          
c   -- var.elim.:  34000/90543          
c   -- var.elim.:  35000/90543          
c   -- var.elim.:  36000/90543          
c   -- var.elim.:  37000/90543          
c   -- var.elim.:  38000/90543          
c   -- var.elim.:  39000/90543          
c   -- var.elim.:  40000/90543          
c   -- var.elim.:  41000/90543          
c   -- var.elim.:  42000/90543          
c   -- var.elim.:  43000/90543          
c   -- var.elim.:  44000/90543          
c   -- var.elim.:  45000/90543          
c   -- var.elim.:  46000/90543          
c   -- var.elim.:  47000/90543          
c   -- var.elim.:  48000/90543          
c   -- var.elim.:  49000/90543          
c   -- var.elim.:  50000/90543          
c   -- var.elim.:  51000/90543          
c   -- var.elim.:  52000/90543          
c   -- var.elim.:  53000/90543          
c   -- var.elim.:  54000/90543          
c   -- var.elim.:  55000/90543          
c   -- var.elim.:  56000/90543          
c   -- var.elim.:  57000/90543          
c   -- var.elim.:  58000/90543          
c   -- var.elim.:  59000/90543          
c   -- var.elim.:  60000/90543          
c   -- var.elim.:  61000/90543          
c   -- var.elim.:  62000/90543          
c   -- var.elim.:  63000/90543          
c   -- var.elim.:  64000/90543          
c   -- var.elim.:  65000/90543          
c   -- var.elim.:  66000/90543          
c   -- var.elim.:  67000/90543          
c   -- var.elim.:  68000/90543          
c   -- var.elim.:  69000/90543          
c   -- var.elim.:  70000/90543          
c   -- var.elim.:  71000/90543          
c   -- var.elim.:  72000/90543          
c   -- var.elim.:  73000/90543          
c   -- var.elim.:  74000/90543          
c   -- var.elim.:  75000/90543          
c   -- var.elim.:  76000/90543          
c   -- var.elim.:  77000/90543          
c   -- var.elim.:  78000/90543          
c   -- var.elim.:  79000/90543          
c   -- var.elim.:  80000/90543          
c   -- var.elim.:  81000/90543          
c   -- var.elim.:  82000/90543          
c   -- var.elim.:  83000/90543          
c   -- var.elim.:  84000/90543          
c   -- var.elim.:  85000/90543          
c   -- var.elim.:  86000/90543          
c   -- var.elim.:  87000/90543          
c   -- var.elim.:  88000/90543          
c   -- var.elim.:  89000/90543          
c   -- var.elim.:  90000/90543          
c   -- var.elim.:  90543/90543          
c   -- var.elim.:  1000/47594          
c   -- var.elim.:  2000/47594          
c   -- var.elim.:  3000/47594          
c   -- var.elim.:  4000/47594          
c   -- var.elim.:  5000/47594          
c   -- var.elim.:  6000/47594          
c   -- var.elim.:  7000/47594          
c   -- var.elim.:  8000/47594          
c   -- var.elim.:  9000/47594          
c   -- var.elim.:  10000/47594          
c   -- var.elim.:  11000/47594          
c   -- var.elim.:  12000/47594          
c   -- var.elim.:  13000/47594          
c   -- var.elim.:  14000/47594          
c   -- var.elim.:  15000/47594          
c   -- var.elim.:  16000/47594          
c   -- var.elim.:  17000/47594          
c   -- var.elim.:  18000/47594          
c   -- var.elim.:  19000/47594          
c   -- var.elim.:  20000/47594          
c   -- var.elim.:  21000/47594          
c   -- var.elim.:  22000/47594          
c   -- var.elim.:  23000/47594          
c   -- var.elim.:  24000/47594          
c   -- var.elim.:  25000/47594          
c   -- var.elim.:  26000/47594          
c   -- var.elim.:  27000/47594          
c   -- var.elim.:  28000/47594          
c   -- var.elim.:  29000/47594          
c   -- var.elim.:  30000/47594          
c   -- var.elim.:  31000/47594          
c   -- var.elim.:  32000/47594          
c   -- var.elim.:  33000/47594          
c   -- var.elim.:  34000/47594          
c   -- var.elim.:  35000/47594          
c   -- var.elim.:  36000/47594          
c   -- var.elim.:  37000/47594          
c   -- var.elim.:  38000/47594          
c   -- var.elim.:  39000/47594          
c   -- var.elim.:  40000/47594          
c   -- var.elim.:  41000/47594          
c   -- var.elim.:  42000/47594          
c   -- var.elim.:  43000/47594          
c   -- var.elim.:  44000/47594          
c   -- var.elim.:  45000/47594          
c   -- var.elim.:  46000/47594          
c   -- var.elim.:  47000/47594          
c   -- var.elim.:  47594/47594          
c   -- var.elim.:  519/519          
c   -- var.elim.:  1000/1183          
c   -- var.elim.:  1183/1183          
c   -- subsuming                       
c   -- var.elim.:  1000/11854          
c   -- var.elim.:  2000/11854          
c   -- var.elim.:  3000/11854          
c   -- var.elim.:  4000/11854          
c   -- var.elim.:  5000/11854          
c   -- var.elim.:  6000/11854          
c   -- var.elim.:  7000/11854          
c   -- var.elim.:  8000/11854          
c   -- var.elim.:  9000/11854          
c   -- var.elim.:  10000/11854          
c   -- var.elim.:  11000/11854          
c   -- var.elim.:  11854/11854          
c   -- var.elim.:  571/571          
c   -- subsuming                       
c   -- var.elim.:  728/728          
c |    201848 |  386483  1377163 |      --  201762       --      -- |     --   | -27347/148432
c |    201848 |  386483  1377163 |  154593  167805  9499245    56.6 |  1.325 % |
c |    201948 |  386483  1377163 |  170052   19779   563269    28.5 |  0.807 % |
c |    202100 |  386483  1377163 |  187057   19931   564168    28.3 |  0.807 % |
c |    202325 |  386483  1377163 |  205763   20156   565806    28.1 |  0.807 % |
c |    202662 |  386483  1377163 |  226339   20493   571450    27.9 |  0.807 % |
c |    203168 |  386483  1377163 |  248973   20999   584874    27.9 |  0.807 % |
c |    203927 |  386103  1374642 |  273602   21755   599417    27.6 |  0.861 % |
c |    205073 |  386103  1374642 |  300962   22901   612370    26.7 |  0.861 % |
c |    206782 |  386103  1374642 |  331058   24610   644541    26.2 |  0.861 % |
c |    209344 |  385963  1374056 |  364032   27167   692873    25.5 |  0.895 % |
c |    213188 |  385818  1373559 |  400285   31004   778466    25.1 |  0.920 % |
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 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 30549
Raw data (stat): 30549 (runsolver) R 30548 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480324395 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 14302 0 0 0 965 33 0 0 25 0 1 0 480324395 61976576 13417 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15131 13417 603 41 0 15090 0
vsize: 60524
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 14460 0 0 0 1950 47 0 0 25 0 1 0 480324395 62263296 13484 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15201 13484 603 41 0 15160 0
vsize: 60804
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 14460 0 0 0 2950 47 0 0 25 0 1 0 480324395 61476864 13344 4294967295 134512640 134672761 3221224576 3221222976 134603791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15009 13344 603 41 0 14968 0
vsize: 60036
[startup+40.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 14709 0 0 0 3949 48 0 0 25 0 1 0 480324395 61636608 13358 4294967295 134512640 134672761 3221224576 3221223024 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15048 13358 603 41 0 15007 0
vsize: 60192
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 15328 0 0 0 4948 50 0 0 25 0 1 0 480324395 62160896 13448 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15176 13448 603 41 0 15135 0
vsize: 60704
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 15548 0 0 0 5947 50 0 0 25 0 1 0 480324395 62955520 13668 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15370 13668 603 41 0 15329 0
vsize: 61480
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 15651 0 0 0 6947 51 0 0 25 0 1 0 480324395 63504384 13771 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15504 13771 603 41 0 15463 0
vsize: 62016
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 15709 0 0 0 7947 51 0 0 25 0 1 0 480324395 63635456 13829 4294967295 134512640 134672761 3221224576 3221223616 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15536 13829 603 41 0 15495 0
vsize: 62144
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 15924 0 0 0 8947 51 0 0 25 0 1 0 480324395 64540672 14044 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15757 14044 603 41 0 15716 0
vsize: 63028
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 16093 0 0 0 9947 51 0 0 25 0 1 0 480324395 65204224 14213 4294967295 134512640 134672761 3221224576 3221223712 134614488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15919 14213 603 41 0 15878 0
vsize: 63676
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 16247 0 0 0 10947 52 0 0 25 0 1 0 480324395 65859584 14367 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16079 14367 603 41 0 16038 0
vsize: 64316
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 16364 0 0 0 11946 53 0 0 25 0 1 0 480324395 66260992 14484 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16177 14484 603 41 0 16136 0
vsize: 64708
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 16480 0 0 0 12946 53 0 0 25 0 1 0 480324395 66793472 14600 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16307 14600 603 41 0 16266 0
vsize: 65228
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 16659 0 0 0 13946 53 0 0 25 0 1 0 480324395 67575808 14779 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16498 14779 603 41 0 16457 0
vsize: 65992
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 17043 0 0 0 14945 55 0 0 25 0 1 0 480324395 69160960 15163 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16885 15163 603 41 0 16844 0
vsize: 67540
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 17165 0 0 0 15945 55 0 0 25 0 1 0 480324395 69689344 15285 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17014 15285 603 41 0 16973 0
vsize: 68056
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 17329 0 0 0 16944 55 0 0 25 0 1 0 480324395 70352896 15449 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17176 15449 603 41 0 17135 0
vsize: 68704
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 17522 0 0 0 17944 56 0 0 25 0 1 0 480324395 71147520 15642 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17370 15642 603 41 0 17329 0
vsize: 69480
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 17772 0 0 0 18944 57 0 0 25 0 1 0 480324395 72200192 15892 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17627 15892 603 41 0 17586 0
vsize: 70508
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 17992 0 0 0 19943 57 0 0 25 0 1 0 480324395 72994816 16112 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17821 16112 603 41 0 17780 0
vsize: 71284
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 18321 0 0 0 20943 58 0 0 25 0 1 0 480324395 74317824 16441 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18144 16441 603 41 0 18103 0
vsize: 72576
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 18565 0 0 0 21943 58 0 0 25 0 1 0 480324395 75378688 16685 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18403 16685 603 41 0 18362 0
vsize: 73612
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 18804 0 0 0 22942 59 0 0 25 0 1 0 480324395 76304384 16924 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18629 16924 603 41 0 18588 0
vsize: 74516
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 19105 0 0 0 23942 59 0 0 25 0 1 0 480324395 77635584 17225 4294967295 134512640 134672761 3221224576 3221223360 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18954 17225 603 41 0 18913 0
vsize: 75816
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 19341 0 0 0 24942 60 0 0 25 0 1 0 480324395 78557184 17461 4294967295 134512640 134672761 3221224576 3221223712 134614739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19179 17461 603 41 0 19138 0
vsize: 76716
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 19543 0 0 0 25941 61 0 0 25 0 1 0 480324395 79364096 17663 4294967295 134512640 134672761 3221224576 3221223616 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19376 17663 603 41 0 19335 0
vsize: 77504
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 19753 0 0 0 26941 61 0 0 25 0 1 0 480324395 80187392 17873 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19577 17873 603 41 0 19536 0
vsize: 78308
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 19937 0 0 0 27941 61 0 0 25 0 1 0 480324395 80986112 18057 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19772 18057 603 41 0 19731 0
vsize: 79088
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 20039 0 0 0 28941 62 0 0 25 0 1 0 480324395 81391616 18159 4294967295 134512640 134672761 3221224576 3221223712 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19871 18159 603 41 0 19830 0
vsize: 79484
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 20153 0 0 0 29940 62 0 0 25 0 1 0 480324395 82051072 18273 4294967295 134512640 134672761 3221224576 3221223736 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20032 18273 603 41 0 19991 0
vsize: 80128
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 20593 0 0 0 30939 63 0 0 25 0 1 0 480324395 83771392 18713 4294967295 134512640 134672761 3221224576 3221223712 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20452 18713 603 41 0 20411 0
vsize: 81808
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 20958 0 0 0 31939 64 0 0 25 0 1 0 480324395 85364736 19078 4294967295 134512640 134672761 3221224576 3221223616 134614340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20841 19078 603 41 0 20800 0
vsize: 83364
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 21178 0 0 0 32938 65 0 0 25 0 1 0 480324395 86159360 19298 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21035 19298 603 41 0 20994 0
vsize: 84140
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 21335 0 0 0 33938 66 0 0 25 0 1 0 480324395 86822912 19455 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21197 19455 603 41 0 21156 0
vsize: 84788
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 21451 0 0 0 34937 66 0 0 25 0 1 0 480324395 87355392 19571 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21327 19571 603 41 0 21286 0
vsize: 85308
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 21671 0 0 0 35937 66 0 0 25 0 1 0 480324395 88268800 19791 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21550 19791 603 41 0 21509 0
vsize: 86200
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 21986 0 0 0 36937 67 0 0 25 0 1 0 480324395 89448448 20106 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21838 20106 603 41 0 21797 0
vsize: 87352
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 22251 0 0 0 37935 69 0 0 25 0 1 0 480324395 90640384 20371 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22129 20371 603 41 0 22088 0
vsize: 88516
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 22486 0 0 0 38935 70 0 0 25 0 1 0 480324395 91561984 20606 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22354 20606 603 41 0 22313 0
vsize: 89416
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 22798 0 0 0 39935 70 0 0 25 0 1 0 480324395 92762112 20918 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22647 20918 603 41 0 22606 0
vsize: 90588
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 22950 0 0 0 40935 70 0 0 25 0 1 0 480324395 93433856 21070 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22811 21070 603 41 0 22770 0
vsize: 91244
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 23223 0 0 0 41934 71 0 0 25 0 1 0 480324395 94486528 21343 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23068 21343 603 41 0 23027 0
vsize: 92272
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 23410 0 0 0 42933 72 0 0 25 0 1 0 480324395 95277056 21530 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23261 21530 603 41 0 23220 0
vsize: 93044
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 23552 0 0 0 43933 73 0 0 25 0 1 0 480324395 95801344 21672 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23389 21672 603 41 0 23348 0
vsize: 93556
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 23723 0 0 0 44932 73 0 0 25 0 1 0 480324395 96595968 21843 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 21843 603 41 0 23542 0
vsize: 94332
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 23884 0 0 0 45932 73 0 0 25 0 1 0 480324395 97255424 22004 4294967295 134512640 134672761 3221224576 3221223712 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23744 22004 603 41 0 23703 0
vsize: 94976
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 24061 0 0 0 46932 74 0 0 25 0 1 0 480324395 97918976 22181 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23906 22181 603 41 0 23865 0
vsize: 95624
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 24208 0 0 0 47932 74 0 0 25 0 1 0 480324395 98455552 22328 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24037 22328 603 41 0 23996 0
vsize: 96148
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 24379 0 0 0 48932 75 0 0 25 0 1 0 480324395 99241984 22499 4294967295 134512640 134672761 3221224576 3221223760 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24229 22499 603 41 0 24188 0
vsize: 96916
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 24538 0 0 0 49931 75 0 0 25 0 1 0 480324395 99897344 22658 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24389 22658 603 41 0 24348 0
vsize: 97556
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 24733 0 0 0 50931 76 0 0 25 0 1 0 480324395 100683776 22853 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24581 22853 603 41 0 24540 0
vsize: 98324
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 24902 0 0 0 51931 76 0 0 25 0 1 0 480324395 101343232 23022 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24742 23022 603 41 0 24701 0
vsize: 98968
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 25072 0 0 0 52930 77 0 0 25 0 1 0 480324395 102006784 23192 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24904 23192 603 41 0 24863 0
vsize: 99616
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 25244 0 0 0 53930 77 0 0 25 0 1 0 480324395 102670336 23364 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25066 23364 603 41 0 25025 0
vsize: 100264
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 25433 0 0 0 54929 78 0 0 25 0 1 0 480324395 103460864 23553 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25259 23553 603 41 0 25218 0
vsize: 101036
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 25621 0 0 0 55929 79 0 0 25 0 1 0 480324395 104251392 23741 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25452 23741 603 41 0 25411 0
vsize: 101808
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 25695 0 0 0 56929 79 0 0 25 0 1 0 480324395 104517632 23815 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25517 23815 603 41 0 25476 0
vsize: 102068
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 25951 0 0 0 57928 80 0 0 25 0 1 0 480324395 105570304 24071 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25774 24071 603 41 0 25733 0
vsize: 103096
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 26065 0 0 0 58928 80 0 0 25 0 1 0 480324395 106627072 24185 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26032 24185 603 41 0 25991 0
vsize: 104128
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 26181 0 0 0 59929 80 0 0 25 0 1 0 480324395 107032576 24301 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26131 24301 603 41 0 26090 0
vsize: 104524
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 26320 0 0 0 60928 81 0 0 25 0 1 0 480324395 107569152 24440 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26262 24440 603 41 0 26221 0
vsize: 105048
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 26468 0 0 0 61928 82 0 0 25 0 1 0 480324395 108236800 24588 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26425 24588 603 41 0 26384 0
vsize: 105700
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 26613 0 0 0 62927 82 0 0 25 0 1 0 480324395 108769280 24733 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26555 24733 603 41 0 26514 0
vsize: 106220
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 26883 0 0 0 63927 83 0 0 25 0 1 0 480324395 109826048 25003 4294967295 134512640 134672761 3221224576 3221223712 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26813 25003 603 41 0 26772 0
vsize: 107252
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 27300 0 0 0 64927 83 0 0 25 0 1 0 480324395 111517696 25420 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27226 25420 603 41 0 27185 0
vsize: 108904
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 27618 0 0 0 65926 84 0 0 25 0 1 0 480324395 112812032 25738 4294967295 134512640 134672761 3221224576 3221223776 134610683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27542 25738 603 41 0 27501 0
vsize: 110168
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 28143 0 0 0 66925 85 0 0 25 0 1 0 480324395 115073024 26263 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28094 26263 603 41 0 28053 0
vsize: 112376
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 28534 0 0 0 67924 87 0 0 25 0 1 0 480324395 116658176 26654 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28481 26654 603 41 0 28440 0
vsize: 113924
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 28686 0 0 0 68924 87 0 0 25 0 1 0 480324395 117182464 26806 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28609 26806 603 41 0 28568 0
vsize: 114436
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 29165 0 0 0 69923 88 0 0 25 0 1 0 480324395 119152640 27285 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29090 27285 603 41 0 29049 0
vsize: 116360
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 30330 0 0 0 70920 91 0 0 25 0 1 0 480324395 123916288 28450 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30253 28450 603 41 0 30212 0
vsize: 121012
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 30992 0 0 0 71918 93 0 0 25 0 1 0 480324395 126693376 29112 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30931 29112 603 41 0 30890 0
vsize: 123724
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 31422 0 0 0 72918 94 0 0 25 0 1 0 480324395 128401408 29542 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31348 29542 603 41 0 31307 0
vsize: 125392
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 32060 0 0 0 73916 95 0 0 25 0 1 0 480324395 130969600 30180 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31975 30180 603 41 0 31934 0
vsize: 127900
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 32594 0 0 0 74915 97 0 0 25 0 1 0 480324395 133181440 30714 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32515 30714 603 41 0 32474 0
vsize: 130060
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 33455 0 0 0 75913 99 0 0 25 0 1 0 480324395 136732672 31575 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33382 31575 603 41 0 33341 0
vsize: 133528
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 34288 0 0 0 76912 100 0 0 25 0 1 0 480324395 140107776 32408 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34206 32408 603 41 0 34165 0
vsize: 136824
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 35165 0 0 0 77910 103 0 0 25 0 1 0 480324395 143728640 33285 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35090 33285 603 41 0 35049 0
vsize: 140360
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 36055 0 0 0 78908 104 0 0 25 0 1 0 480324395 147415040 34175 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35990 34175 603 41 0 35949 0
vsize: 143960
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 37089 0 0 0 79906 107 0 0 25 0 1 0 480324395 151547904 35209 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36999 35209 603 41 0 36958 0
vsize: 147996
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 37843 0 0 0 80904 109 0 0 25 0 1 0 480324395 154644480 35963 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37755 35963 603 41 0 37714 0
vsize: 151020
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 38742 0 0 0 81901 112 0 0 25 0 1 0 480324395 158375936 36862 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38666 36862 603 41 0 38625 0
vsize: 154664
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 39496 0 0 0 82900 114 0 0 25 0 1 0 480324395 161394688 37616 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39403 37616 603 41 0 39362 0
vsize: 157612
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 40468 0 0 0 83897 117 0 0 25 0 1 0 480324395 165412864 38588 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40384 38588 603 41 0 40343 0
vsize: 161536
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 41232 0 0 0 84895 119 0 0 25 0 1 0 480324395 168493056 39352 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41136 39352 603 41 0 41095 0
vsize: 164544
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 41902 0 0 0 85893 121 0 0 25 0 1 0 480324395 171331584 40022 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41829 40022 603 41 0 41788 0
vsize: 167316
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 42536 0 0 0 86892 122 0 0 25 0 1 0 480324395 173916160 40656 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42460 40656 603 41 0 42419 0
vsize: 169840
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 43231 0 0 0 87890 125 0 0 25 0 1 0 480324395 176672768 41351 4294967295 134512640 134672761 3221224576 3221223616 134613118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43133 41351 603 41 0 43092 0
vsize: 172532
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 43947 0 0 0 88888 126 0 0 25 0 1 0 480324395 179666944 42067 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43864 42067 603 41 0 43823 0
vsize: 175456
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 44921 0 0 0 89887 128 0 0 25 0 1 0 480324395 183676928 43041 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44843 43041 603 41 0 44802 0
vsize: 179372
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 45972 0 0 0 90884 131 0 0 25 0 1 0 480324395 187981824 44092 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45894 44092 603 41 0 45853 0
vsize: 183576
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 47022 0 0 0 91883 133 0 0 25 0 1 0 480324395 192208896 45142 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46926 45142 603 41 0 46885 0
vsize: 187704
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 47831 0 0 0 92881 135 0 0 25 0 1 0 480324395 195620864 45951 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47759 45951 603 41 0 47718 0
vsize: 191036
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 48529 0 0 0 93880 136 0 0 25 0 1 0 480324395 198451200 46649 4294967295 134512640 134672761 3221224576 3221223616 134614243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48450 46649 603 41 0 48409 0
vsize: 193800
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 49372 0 0 0 94878 138 0 0 25 0 1 0 480324395 201854976 47492 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49281 47492 603 41 0 49240 0
vsize: 197124
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 50266 0 0 0 95876 140 0 0 25 0 1 0 480324395 205508608 48386 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50173 48386 603 41 0 50132 0
vsize: 200692
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51219 0 0 0 96874 142 0 0 25 0 1 0 480324395 209498112 49339 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51147 49339 603 41 0 51106 0
vsize: 204588
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51324 0 0 0 97874 143 0 0 25 0 1 0 480324395 209903616 49444 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51246 49444 603 41 0 51205 0
vsize: 204984
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51469 0 0 0 98873 143 0 0 25 0 1 0 480324395 210432000 49589 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51375 49589 603 41 0 51334 0
vsize: 205500
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51587 0 0 0 99873 144 0 0 25 0 1 0 480324395 210960384 49707 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51504 49707 603 41 0 51463 0
vsize: 206016
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51705 0 0 0 100873 144 0 0 25 0 1 0 480324395 211353600 49825 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51600 49825 603 41 0 51559 0
vsize: 206400
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51887 0 0 0 101873 145 0 0 25 0 1 0 480324395 212144128 50007 4294967295 134512640 134672761 3221224576 3221223616 134612992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51793 50007 603 41 0 51752 0
vsize: 207172
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 51977 0 0 0 102872 145 0 0 25 0 1 0 480324395 212545536 50097 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51891 50097 603 41 0 51850 0
vsize: 207564
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 52051 0 0 0 103872 146 0 0 25 0 1 0 480324395 212807680 50171 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51955 50171 603 41 0 51914 0
vsize: 207820
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 52161 0 0 0 104872 146 0 0 25 0 1 0 480324395 213204992 50281 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52052 50281 603 41 0 52011 0
vsize: 208208
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 52445 0 0 0 105872 146 0 0 25 0 1 0 480324395 214401024 50565 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52344 50565 603 41 0 52303 0
vsize: 209376
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 52668 0 0 0 106871 147 0 0 25 0 1 0 480324395 215322624 50788 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52569 50788 603 41 0 52528 0
vsize: 210276
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 52879 0 0 0 107871 148 0 0 25 0 1 0 480324395 216121344 50999 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52764 50999 603 41 0 52723 0
vsize: 211056
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 53116 0 0 0 108870 149 0 0 25 0 1 0 480324395 217182208 51236 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53023 51236 603 41 0 52982 0
vsize: 212092
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 67419 0 0 0 109831 187 0 0 25 0 1 0 480324395 268242944 62046 4294967295 134512640 134672761 3221224576 3221223344 134629744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65489 62046 603 41 0 65448 0
vsize: 261956
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 68350 0 0 0 110783 208 0 0 25 0 1 0 480324395 264888320 61519 4294967295 134512640 134672761 3221224576 3221223024 134643910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64670 61519 603 41 0 64629 0
vsize: 258680
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 68382 0 0 0 111780 211 0 0 25 0 1 0 480324395 264843264 61462 4294967295 134512640 134672761 3221224576 3221223024 134643559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64659 61462 603 41 0 64618 0
vsize: 258636
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 69581 0 0 0 112777 214 0 0 25 0 1 0 480324395 272564224 62461 4294967295 134512640 134672761 3221224576 3221223068 134642971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66544 62461 603 41 0 66503 0
vsize: 266176
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 69593 0 0 0 113777 215 0 0 25 0 1 0 480324395 264208384 61370 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64504 61370 603 41 0 64463 0
vsize: 258016
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70826 0 0 0 114774 218 0 0 25 0 1 0 480324395 265117696 61539 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64726 61539 603 41 0 64685 0
vsize: 258904
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70835 0 0 0 115775 218 0 0 25 0 1 0 480324395 265117696 61548 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64726 61548 603 41 0 64685 0
vsize: 258904
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70848 0 0 0 116775 218 0 0 25 0 1 0 480324395 265379840 61561 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 61561 603 41 0 64749 0
vsize: 259160
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70848 0 0 0 117775 218 0 0 25 0 1 0 480324395 265379840 61561 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 61561 603 41 0 64749 0
vsize: 259160
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70848 0 0 0 118775 218 0 0 25 0 1 0 480324395 265379840 61561 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 61561 603 41 0 64749 0
vsize: 259160
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70848 0 0 0 119775 218 0 0 25 0 1 0 480324395 265379840 61561 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 61561 603 41 0 64749 0
vsize: 259160
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30549
Raw data (stat): 30549 (minisat+) R 30548 26298 26297 0 -1 0 70848 0 0 0 120775 218 0 0 25 0 1 0 480324395 265379840 61561 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 61561 603 41 0 64749 0
vsize: 259160
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.17 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30549
Raw data (stat): 30549 (minisat+) Z 30548 26298 26297 0 -1 12 70849 0 0 0 120775 231 0 0 25 0 1 0 480324395 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): 1210.17
CPU time (s): 1210.08
CPU user time (s): 1207.76
CPU system time (s): 2.31865
CPU usage (%): 99.9921
Max. virtual memory (Kb): 266176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####