PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-gr4x6.opb
MD5SUM	c1c7537cd9b3e10215a81ec1ca3be5cb
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2605440
Optimality of the best value was proved	NO
Number of terms in the objective function	504
Biggest coefficient in the objective function	148373504
Number of bits for the biggest coefficient in the objective function	28
Sum of the numbers in the objective function	3393589600
Number of bits of the sum of numbers in the objective function	32
Biggest number in a constraint	148373504
Number of bits of the biggest number in a constraint	28
Biggest sum of numbers in a constraint	3393589600
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	504
Total number of constraints	34
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	34
Minimum length of a constraint	21
Maximum length of a constraint	120
Trace number 17848

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 12:22:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18991 boxname=wulflinc3 idbench=1461 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1c7537cd9b3e10215a81ec1ca3be5cb  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-gr4x6.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-gr4x6.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-gr4x6.opb
IDLAUNCH: 18991
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        759212 kB
Buffers:         16116 kB
Cached:         236912 kB
SwapCached:          0 kB
Active:          13108 kB
Inactive:       242704 kB
HighTotal:      131008 kB
HighFree:        99456 kB
LowTotal:       903652 kB
LowFree:        659756 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13960 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:42:33 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 18991 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 44 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): (none)
c ---[  42]---> Sorter-cost:  972     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  972     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  888     Base: 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   16397    38689 |    4919       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5206          
c   -- var.elim.:  2000/5206          
c   -- var.elim.:  3000/5206          
c   -- var.elim.:  4000/5206          
c   -- var.elim.:  5000/5206          
c   -- var.elim.:  5206/5206          
c   -- var.elim.:  1000/2921          
c   -- var.elim.:  2000/2921          
c   -- var.elim.:  2921/2921          
c   -- var.elim.:  63/63          
c   -- subsuming                       
c   -- var.elim.:  836/836          
c   -- var.elim.:  456/456          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  56/56          
c   -- var.elim.:  15/15          
c |         0 |   13211    39259 |      --       0       --      -- |     --   | -2138/3191
c |         0 |   13211    39259 |    5284       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.845871 s)
c ==============================================================================
c [1mFound solution: 6128144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63755     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        71 |  190290   452763 |   57086      71      339     4.8 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/60590          
c   -- var.elim.:  2000/60590          
c   -- var.elim.:  3000/60590          
c   -- var.elim.:  4000/60590          
c   -- var.elim.:  5000/60590          
c   -- var.elim.:  6000/60590          
c   -- var.elim.:  7000/60590          
c   -- var.elim.:  8000/60590          
c   -- var.elim.:  9000/60590          
c   -- var.elim.:  10000/60590          
c   -- var.elim.:  11000/60590          
c   -- var.elim.:  12000/60590          
c   -- var.elim.:  13000/60590          
c   -- var.elim.:  14000/60590          
c   -- var.elim.:  15000/60590          
c   -- var.elim.:  16000/60590          
c   -- var.elim.:  17000/60590          
c   -- var.elim.:  18000/60590          
c   -- var.elim.:  19000/60590          
c   -- var.elim.:  20000/60590          
c   -- var.elim.:  21000/60590          
c   -- var.elim.:  22000/60590          
c   -- var.elim.:  23000/60590          
c   -- var.elim.:  24000/60590          
c   -- var.elim.:  25000/60590          
c   -- var.elim.:  26000/60590          
c   -- var.elim.:  27000/60590          
c   -- var.elim.:  28000/60590          
c   -- var.elim.:  29000/60590          
c   -- var.elim.:  30000/60590          
c   -- var.elim.:  31000/60590          
c   -- var.elim.:  32000/60590          
c   -- var.elim.:  33000/60590          
c   -- var.elim.:  34000/60590          
c   -- var.elim.:  35000/60590          
c   -- var.elim.:  36000/60590          
c   -- var.elim.:  37000/60590          
c   -- var.elim.:  38000/60590          
c   -- var.elim.:  39000/60590          
c   -- var.elim.:  40000/60590          
c   -- var.elim.:  41000/60590          
c   -- var.elim.:  42000/60590          
c   -- var.elim.:  43000/60590          
c   -- var.elim.:  44000/60590          
c   -- var.elim.:  45000/60590          
c   -- var.elim.:  46000/60590          
c   -- var.elim.:  47000/60590          
c   -- var.elim.:  48000/60590          
c   -- var.elim.:  49000/60590          
c   -- var.elim.:  50000/60590          
c   -- var.elim.:  51000/60590          
c   -- var.elim.:  52000/60590          
c   -- var.elim.:  53000/60590          
c   -- var.elim.:  54000/60590          
c   -- var.elim.:  55000/60590          
c   -- var.elim.:  56000/60590          
c   -- var.elim.:  57000/60590          
c   -- var.elim.:  58000/60590          
c   -- var.elim.:  59000/60590          
c   -- var.elim.:  60000/60590          
c   -- var.elim.:  60590/60590          
c   -- var.elim.:  1000/33394          
c   -- var.elim.:  2000/33394          
c   -- var.elim.:  3000/33394          
c   -- var.elim.:  4000/33394          
c   -- var.elim.:  5000/33394          
c   -- var.elim.:  6000/33394          
c   -- var.elim.:  7000/33394          
c   -- var.elim.:  8000/33394          
c   -- var.elim.:  9000/33394          
c   -- var.elim.:  10000/33394          
c   -- var.elim.:  11000/33394          
c   -- var.elim.:  12000/33394          
c   -- var.elim.:  13000/33394          
c   -- var.elim.:  14000/33394          
c   -- var.elim.:  15000/33394          
c   -- var.elim.:  16000/33394          
c   -- var.elim.:  17000/33394          
c   -- var.elim.:  18000/33394          
c   -- var.elim.:  19000/33394          
c   -- var.elim.:  20000/33394          
c   -- var.elim.:  21000/33394          
c   -- var.elim.:  22000/33394          
c   -- var.elim.:  23000/33394          
c   -- var.elim.:  24000/33394          
c   -- var.elim.:  25000/33394          
c   -- var.elim.:  26000/33394          
c   -- var.elim.:  27000/33394          
c   -- var.elim.:  28000/33394          
c   -- var.elim.:  29000/33394          
c   -- var.elim.:  30000/33394          
c   -- var.elim.:  31000/33394          
c   -- var.elim.:  32000/33394          
c   -- var.elim.:  33000/33394          
c   -- var.elim.:  33394/33394          
c   -- var.elim.:  382/382          
c   -- var.elim.:  238/238          
c   -- subsuming                       
c   -- var.elim.:  1000/1892          
c   -- var.elim.:  1892/1892          
c   -- var.elim.:  777/777          
c   -- subsuming                       
c   -- var.elim.:  363/363          
c   -- var.elim.:  34/34          
c |        71 |  174207   535218 |      --      71       --      -- |     --   | -16083/82456
c |        71 |  174207   535218 |   69682      70      336     4.8 |  0.000 % |
c |       173 |  174207   535218 |   76651     172     1186     6.9 |  1.712 % |
c |       323 |  174207   535218 |   84316     322     1938     6.0 |  1.712 % |
c |       552 |  174207   535218 |   92747     551     4444     8.1 |  1.712 % |
c |       889 |  174207   535218 |  102022     888    12514    14.1 |  1.712 % |
c ==============================================================================
c (current CPU-time: 14.8467 s)
c ==============================================================================
c [1mFound solution: 5921722[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1028 |  177406   544002 |   53221    1027    15732    15.3 |  1.712 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4651          
c   -- var.elim.:  2000/4651          
c   -- var.elim.:  3000/4651          
c   -- var.elim.:  4000/4651          
c   -- var.elim.:  4651/4651          
c   -- var.elim.:  1000/2773          
c   -- var.elim.:  2000/2773          
c   -- var.elim.:  2773/2773          
c   -- subsuming                       
c   -- var.elim.:  484/484          
c |      1028 |  175575   545046 |      --    1027       --      -- |     --   | -1831/1045
c |      1028 |  175575   545046 |   70230    1027    15732    15.3 |  1.712 % |
c ==============================================================================
c (current CPU-time: 17.0264 s)
c ==============================================================================
c [1mFound solution: 5533300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1077 |  176733   548975 |   53019    1076    16053    14.9 |  1.712 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2724          
c   -- var.elim.:  2000/2724          
c   -- var.elim.:  2724/2724          
c   -- var.elim.:  1000/1856          
c   -- var.elim.:  1856/1856          
c   -- subsuming                       
c   -- var.elim.:  457/457          
c |      1077 |  175980   550011 |      --    1076       --      -- |     --   | -753/1037
c |      1077 |  175980   550011 |   70392    1076    16053    14.9 |  1.712 % |
c |      1177 |  175980   550011 |   77431    1176    16500    14.0 |  1.699 % |
c |      1328 |  175980   550011 |   85174    1327    18819    14.2 |  1.699 % |
c |      1556 |  175980   550011 |   93691    1555    26879    17.3 |  1.699 % |
c ==============================================================================
c (current CPU-time: 20.6729 s)
c ==============================================================================
c [1mFound solution: 4651499[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1626 |  176330   551807 |   52898    1625    27763    17.1 |  1.699 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1410          
c   -- var.elim.:  1410/1410          
c   -- var.elim.:  1000/1148          
c   -- var.elim.:  1148/1148          
c   -- subsuming                       
c   -- var.elim.:  373/373          
c |      1626 |  176095   553740 |      --    1625       --      -- |     --   | -235/1934
c |      1626 |  176095   553740 |   70438    1625    27763    17.1 |  1.699 % |
c |      1727 |  176095   553740 |   77481    1726    30990    18.0 |  1.701 % |
c |      1880 |  176095   553740 |   85229    1879    36231    19.3 |  1.701 % |
c |      2105 |  176057   552882 |   93732    2103    41542    19.8 |  1.715 % |
c |      2443 |  176057   552882 |  103106    2441   101769    41.7 |  1.715 % |
c |      2949 |  176057   552882 |  113416    2947   112577    38.2 |  1.715 % |
c |      3708 |  176057   552882 |  124758    3706   142422    38.4 |  1.715 % |
c ==============================================================================
c (current CPU-time: 32.0561 s)
c ==============================================================================
c [1mFound solution: 4495958[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4078 |  176316   554547 |   52894    4076   161608    39.6 |  1.715 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1425          
c   -- var.elim.:  1425/1425          
c   -- var.elim.:  1000/1204          
c   -- var.elim.:  1204/1204          
c   -- var.elim.:  99/99          
c |      4078 |  176127   557814 |      --    4076       --      -- |     --   | -189/3268
c |      4078 |  176127   557814 |   70450    4076   161608    39.6 |  1.715 % |
c |      4179 |  176127   557814 |   77495    4177   162491    38.9 |  1.717 % |
c |      4329 |  176127   557814 |   85245    4327   168107    38.9 |  1.717 % |
c |      4554 |  175999   556545 |   93701    4551   170837    37.5 |  1.768 % |
c |      4891 |  175999   556545 |  103072    4888   183798    37.6 |  1.768 % |
c |      5397 |  175999   556545 |  113379    5394   188099    34.9 |  1.768 % |
c |      6156 |  175999   556545 |  124717    6153   196456    31.9 |  1.768 % |
c |      7296 |  175999   556545 |  137188    7293   215745    29.6 |  1.768 % |
c |      9004 |  175999   556545 |  150907    9001   255479    28.4 |  1.768 % |
c |     11566 |  175573   554499 |  165596   11554   618841    53.6 |  1.917 % |
c ==============================================================================
c (current CPU-time: 67.0888 s)
c ==============================================================================
c [1mFound solution: 4457447[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14272 |  175581   553339 |   52674   14256  1189142    83.4 |  1.917 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1795          
c   -- var.elim.:  1795/1795          
c   -- var.elim.:  1000/1619          
c   -- var.elim.:  1619/1619          
c   -- var.elim.:  389/389          
c   -- var.elim.:  250/250          
c   -- subsuming                       
c   -- var.elim.:  376/376          
c   -- var.elim.:  340/340          
c   -- var.elim.:  314/314          
c |     14272 |  175371   554512 |      --   14256       --      -- |     --   | -210/1174
c |     14272 |  175371   554512 |   70148   13760   736602    53.5 |  1.917 % |
c |     14373 |  175371   554512 |   77163   13861   737515    53.2 |  1.957 % |
c |     14523 |  175342   554150 |   84865   14010   740419    52.8 |  1.965 % |
c |     14748 |  175342   554150 |   93352   14235   742303    52.1 |  1.965 % |
c |     15085 |  175328   554093 |  102679   14571   781199    53.6 |  1.970 % |
c |     15591 |  175328   554093 |  112946   15077   790120    52.4 |  1.970 % |
c |     16350 |  175295   553519 |  124218   15835   805111    50.8 |  1.979 % |
c ==============================================================================
c (current CPU-time: 73.7228 s)
c ==============================================================================
c [1mFound solution: 4439936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16479 |  175416   554851 |   52624   15964   807051    50.6 |  1.979 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1532          
c   -- var.elim.:  1532/1532          
c   -- var.elim.:  1000/1193          
c   -- var.elim.:  1193/1193          
c   -- var.elim.:  363/363          
c   -- var.elim.:  29/29          
c   -- subsuming                       
c   -- var.elim.:  214/214          
c |     16479 |  175255   558402 |      --   15964       --      -- |     --   | -160/3554
c |     16479 |  175255   558402 |   70102   15759   726426    46.1 |  1.979 % |
c |     16579 |  175255   558402 |   77112   15859   741917    46.8 |  2.003 % |
c |     16729 |  175255   558402 |   84823   16009   743264    46.4 |  2.003 % |
c |     16954 |  175255   558402 |   93305   16234   746262    46.0 |  2.003 % |
c |     17291 |  175255   558402 |  102636   16571   750046    45.3 |  2.003 % |
c |     17797 |  175170   557999 |  112845   17076   757598    44.4 |  2.028 % |
c |     18558 |  175170   557999 |  124129   17837   769405    43.1 |  2.028 % |
c |     19699 |  175170   557999 |  136542   18978   804076    42.4 |  2.028 % |
c |     21407 |  175170   557999 |  150196   20686  1221645    59.1 |  2.028 % |
c |     23969 |  175170   557999 |  165216   23248  1478971    63.6 |  2.028 % |
c ==============================================================================
c (current CPU-time: 107.707 s)
c ==============================================================================
c [1mFound solution: 3348812[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26290 |  174698   554901 |   52409   25555  1545039    60.5 |  2.028 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2458          
c   -- var.elim.:  2000/2458          
c   -- var.elim.:  2458/2458          
c   -- var.elim.:  1000/1901          
c   -- var.elim.:  1901/1901          
c   -- var.elim.:  252/252          
c   -- subsuming                       
c   -- var.elim.:  214/214          
c   -- var.elim.:  39/39          
c |     26290 |  174240   558941 |      --   25555       --      -- |     --   | -455/4047
c |     26290 |  174240   558941 |   69696   24501  1068284    43.6 |  2.028 % |
c |     26390 |  174240   558941 |   76665   24601  1072115    43.6 |  2.392 % |
c |     26541 |  174204   558833 |   84314   24751  1086652    43.9 |  2.406 % |
c |     26767 |  174204   558833 |   92746   24977  1127175    45.1 |  2.406 % |
c |     27106 |  174177   558730 |  102005   25314  1167375    46.1 |  2.417 % |
c ==============================================================================
c (current CPU-time: 118.169 s)
c ==============================================================================
c [1mFound solution: 3183328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     27331 |  174333   560004 |   52299   25539  1192935    46.7 |  2.417 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1203          
c   -- var.elim.:  1203/1203          
c   -- var.elim.:  1000/1055          
c   -- var.elim.:  1055/1055          
c   -- var.elim.:  493/493          
c   -- var.elim.:  566/566          
c |     27331 |  174200   561978 |      --   25539       --      -- |     --   | -133/1975
c |     27331 |  174200   561978 |   69680   25064  1123611    44.8 |  2.417 % |
c |     27432 |  174200   561978 |   76648   25165  1129264    44.9 |  2.422 % |
c |     27582 |  174200   561978 |   84312   25315  1148407    45.4 |  2.422 % |
c |     27808 |  174191   561944 |   92739   25540  1181979    46.3 |  2.425 % |
c |     28146 |  174191   561944 |  102013   25878  1262414    48.8 |  2.425 % |
c |     28653 |  174172   561747 |  112202   26384  1268198    48.1 |  2.435 % |
c |     29413 |  174172   561747 |  123422   27144  1310131    48.3 |  2.435 % |
c |     30552 |  174172   561747 |  135764   28283  2005240    70.9 |  2.435 % |
c |     32260 |  174172   561747 |  149341   29991  2521747    84.1 |  2.435 % |
c ==============================================================================
c (current CPU-time: 173.006 s)
c ==============================================================================
c [1mFound solution: 3031424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     34009 |  174301   562881 |   52290   31732  2872557    90.5 |  2.435 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1569          
c   -- var.elim.:  1569/1569          
c   -- var.elim.:  1000/1271          
c   -- var.elim.:  1271/1271          
c   -- var.elim.:  396/396          
c   -- var.elim.:  26/26          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  50/50          
c   -- var.elim.:  18/18          
c |     34009 |  174060   564579 |      --   31732       --      -- |     --   | -240/1701
c |     34009 |  174060   564579 |   69624   29005  1602523    55.2 |  2.435 % |
c |     34109 |  174060   564579 |   76586   29105  1609070    55.3 |  2.467 % |
c |     34259 |  174060   564579 |   84245   29255  1618928    55.3 |  2.467 % |
c |     34486 |  174060   564579 |   92669   29482  1679233    57.0 |  2.467 % |
c |     34823 |  174060   564579 |  101936   29819  1710767    57.4 |  2.467 % |
c |     35329 |  174060   564579 |  112130   30325  1899922    62.7 |  2.467 % |
c ==============================================================================
c (current CPU-time: 187.198 s)
c ==============================================================================
c [1mFound solution: 2950400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35395 |  174139   565597 |   52241   30391  1905639    62.7 |  2.467 % |
c   -- subsuming                       
c   -- var.elim.:  934/934          
c   -- var.elim.:  879/879          
c   -- var.elim.:  537/537          
c |     35395 |  174086   568003 |      --   30391       --      -- |     --   | -53/2407
c |     35395 |  174086   568003 |   69634   30391  1905639    62.7 |  2.467 % |
c |     35496 |  174086   568003 |   76597   30492  1908538    62.6 |  2.469 % |
c |     35646 |  174057   567902 |   84243   30641  1922286    62.7 |  2.477 % |
c |     35873 |  174057   567902 |   92667   30868  1968980    63.8 |  2.477 % |
c |     36212 |  174057   567902 |  101934   31207  2040774    65.4 |  2.477 % |
c |     36719 |  174057   567902 |  112128   31714  2064435    65.1 |  2.477 % |
c |     37481 |  174057   567902 |  123341   32476  2324953    71.6 |  2.477 % |
c |     38620 |  174057   567902 |  135675   33615  2749924    81.8 |  2.477 % |
c |     40328 |  174057   567902 |  149242   35323  3586379   101.5 |  2.477 % |
c |     42890 |  174047   567872 |  164157   37884  4479535   118.2 |  2.482 % |
c |     46735 |  173937   567434 |  180459   41712  5980433   143.4 |  2.523 % |
c ==============================================================================
c (current CPU-time: 305.827 s)
c ==============================================================================
c [1mFound solution: 2909440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     47446 |  174043   568335 |   52212   42423  6352204   149.7 |  2.523 % |
c   -- subsuming                       
c   -- var.elim.:  901/901          
c   -- var.elim.:  972/972          
c   -- var.elim.:  214/214          
c   -- subsuming                       
c   -- var.elim.:  168/168          
c   -- var.elim.:  114/114          
c |     47446 |  173931   568500 |      --   42423       --      -- |     --   | -112/166
c |     47446 |  173931   568500 |   69572   35743  2271700    63.6 |  2.523 % |
c |     47546 |  173931   568500 |   76529   35843  2285864    63.8 |  2.527 % |
c |     47697 |  173931   568500 |   84182   35994  2310883    64.2 |  2.527 % |
c |     47923 |  173931   568500 |   92600   36220  2364706    65.3 |  2.527 % |
c |     48261 |  173931   568500 |  101860   36558  2458406    67.2 |  2.527 % |
c |     48767 |  173931   568500 |  112047   37064  2562857    69.1 |  2.527 % |
c |     49527 |  173931   568500 |  123251   37824  2919134    77.2 |  2.527 % |
c |     50666 |  173931   568500 |  135576   38963  3298156    84.6 |  2.527 % |
c |     52376 |  173931   568500 |  149134   40673  4087051   100.5 |  2.527 % |
c |     54939 |  173931   568500 |  164048   43236  5686432   131.5 |  2.527 % |
c |     58785 |  173931   568500 |  180452   47082  7856789   166.9 |  2.527 % |
c |     64552 |  173760   567823 |  198303   52844 12187869   230.6 |  2.609 % |
c |     73202 |  173547   564418 |  217865   61460 15867148   258.2 |  2.685 % |
c |     86176 |  173547   564418 |  239652   74434 22915202   307.9 |  2.685 % |
c |    105637 |  173036   560231 |  262841   93886 36095975   384.5 |  2.867 % |
c ==============================================================================
c (current CPU-time: 1144.65 s)
c ==============================================================================
c [1mFound solution: 2844160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    113471 |  173090   560993 |   51926  101720 41885605   411.8 |  2.867 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2050          
c   -- var.elim.:  2000/2050          
c   -- var.elim.:  2050/2050          
c   -- var.elim.:  1000/1462          
c   -- var.elim.:  1462/1462          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  7/7          
c |    113471 |  172969   564710 |      --  101720       --      -- |     --   | -118/3724
c |    113471 |  172969   564710 |   69187   78120 13689596   175.2 |  2.867 % |
c |    113571 |  172969   564710 |   76106   15799  3869965   244.9 |  2.883 % |
c |    113724 |  172969   564710 |   83716   15952  3943471   247.2 |  2.883 % |
c |    113949 |  172969   564710 |   92088   16177  4042314   249.9 |  2.883 % |
c |    114286 |  172969   564710 |  101297   16514  4143418   250.9 |  2.883 % |
c |    114794 |  172961   564682 |  111422   17021  4413167   259.3 |  2.885 % |
c |    115554 |  172961   564682 |  122564   17781  4730095   266.0 |  2.886 % |
c |    116693 |  172961   564682 |  134820   18920  5213785   275.6 |  2.886 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 X0_bit0 X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 X3_bit0 -X3_bit1 X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 X4_bit0 -X4_bit1 X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 X7_bit1 X7_bit2 X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 X8_bit0 -X8_bit1 X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_#### 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 12249
Raw data (stat): 12249 (runsolver) R 12248 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486819695 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0005 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 10392 0 0 0 958 39 0 0 25 0 1 0 486819695 49033216 9616 4294967295 134512640 134672761 3221224544 3221223088 134621359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11971 9616 603 41 0 11930 0
vsize: 47884
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 16760 0 0 0 1935 61 0 0 25 0 1 0 486819695 49766400 9881 4294967295 134512640 134672761 3221224544 3221223628 1074733103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12150 9881 603 41 0 12109 0
vsize: 48600
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 19658 0 0 0 2924 72 0 0 25 0 1 0 486819695 49770496 9886 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12151 9886 603 41 0 12110 0
vsize: 48604
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 22454 0 0 0 3914 82 0 0 25 0 1 0 486819695 50229248 9985 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12263 9985 603 41 0 12222 0
vsize: 49052
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 22809 0 0 0 4913 83 0 0 25 0 1 0 486819695 51634176 10340 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12606 10340 603 41 0 12565 0
vsize: 50424
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 23166 0 0 0 5911 85 0 0 25 0 1 0 486819695 53186560 10697 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12985 10697 603 41 0 12944 0
vsize: 51940
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 26571 0 0 0 6900 97 0 0 25 0 1 0 486819695 54206464 10972 4294967295 134512640 134672761 3221224544 3221223800 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13234 10972 603 41 0 13193 0
vsize: 52936
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 29407 0 0 0 7889 107 0 0 25 0 1 0 486819695 54251520 10993 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13245 10993 603 41 0 13204 0
vsize: 52980
[startup+90.0036 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 29442 0 0 0 8889 107 0 0 25 0 1 0 486819695 54509568 11028 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13308 11028 603 41 0 13267 0
vsize: 53232
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 29624 0 0 0 9888 108 0 0 25 0 1 0 486819695 55169024 11210 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13469 11210 603 41 0 13428 0
vsize: 53876
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 32168 0 0 0 10879 117 0 0 25 0 1 0 486819695 55988224 11417 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13669 11417 603 41 0 13628 0
vsize: 54676
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 34962 0 0 0 11870 127 0 0 25 0 1 0 486819695 69898240 13397 4294967295 134512640 134672761 3221224544 3221223024 134618950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17065 13397 603 41 0 17024 0
vsize: 68260
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 35523 0 0 0 12866 130 0 0 25 0 1 0 486819695 56143872 11459 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 11459 603 41 0 13666 0
vsize: 54828
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 35697 0 0 0 13866 130 0 0 25 0 1 0 486819695 56864768 11633 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13883 11633 603 41 0 13842 0
vsize: 55532
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 36118 0 0 0 14866 131 0 0 25 0 1 0 486819695 58691584 12054 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14329 12054 603 41 0 14288 0
vsize: 57316
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 36500 0 0 0 15864 132 0 0 25 0 1 0 486819695 60145664 12436 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14684 12436 603 41 0 14643 0
vsize: 58736
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 36733 0 0 0 16862 133 0 0 25 0 1 0 486819695 61198336 12669 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14941 12669 603 41 0 14900 0
vsize: 59764
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 40070 0 0 0 17851 145 0 0 25 0 1 0 486819695 61808640 12845 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15090 12845 603 41 0 15049 0
vsize: 60360
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 42052 0 0 0 18843 153 0 0 25 0 1 0 486819695 61808640 12846 4294967295 134512640 134672761 3221224544 3221222048 134604049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15090 12846 603 41 0 15049 0
vsize: 60360
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 42386 0 0 0 19842 154 0 0 25 0 1 0 486819695 61808640 12846 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15090 12846 603 41 0 15049 0
vsize: 60360
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 42419 0 0 0 20842 154 0 0 25 0 1 0 486819695 62070784 12879 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15154 12879 603 41 0 15113 0
vsize: 60616
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 42420 0 0 0 21841 154 0 0 25 0 1 0 486819695 62070784 12880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15154 12880 603 41 0 15113 0
vsize: 60616
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 42948 0 0 0 22841 155 0 0 25 0 1 0 486819695 64270336 13408 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15691 13408 603 41 0 15650 0
vsize: 62764
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 43368 0 0 0 23840 156 0 0 25 0 1 0 486819695 66068480 13828 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16130 13828 603 41 0 16089 0
vsize: 64520
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 43633 0 0 0 24839 157 0 0 25 0 1 0 486819695 67088384 14093 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16379 14093 603 41 0 16338 0
vsize: 65516
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 44033 0 0 0 25838 159 0 0 25 0 1 0 486819695 68751360 14493 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16785 14493 603 41 0 16744 0
vsize: 67140
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 44403 0 0 0 26837 160 0 0 25 0 1 0 486819695 70209536 14863 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17141 14863 603 41 0 17100 0
vsize: 68564
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 44818 0 0 0 27836 161 0 0 25 0 1 0 486819695 71909376 15278 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17556 15278 603 41 0 17515 0
vsize: 70224
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 45141 0 0 0 28835 162 0 0 25 0 1 0 486819695 73302016 15601 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 15601 603 41 0 17855 0
vsize: 71584
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 45562 0 0 0 29835 163 0 0 25 0 1 0 486819695 75018240 16022 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18315 16022 603 41 0 18274 0
vsize: 73260
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 30824 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 31824 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 32824 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 33824 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 34824 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 35825 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 36825 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 37825 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49122 0 0 0 38825 174 0 0 25 0 1 0 486819695 76607488 16434 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16434 603 41 0 18662 0
vsize: 74812
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49123 0 0 0 39825 174 0 0 25 0 1 0 486819695 76607488 16435 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 16435 603 41 0 18662 0
vsize: 74812
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49284 0 0 0 40825 174 0 0 25 0 1 0 486819695 77361152 16596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18887 16596 603 41 0 18846 0
vsize: 75548
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 49641 0 0 0 41824 175 0 0 25 0 1 0 486819695 78798848 16953 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19238 16953 603 41 0 19197 0
vsize: 76952
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 50066 0 0 0 42823 176 0 0 25 0 1 0 486819695 80498688 17378 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19653 17378 603 41 0 19612 0
vsize: 78612
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 50692 0 0 0 43822 178 0 0 25 0 1 0 486819695 83099648 18004 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20288 18004 603 41 0 20247 0
vsize: 81152
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 51299 0 0 0 44819 180 0 0 25 0 1 0 486819695 85532672 18611 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20882 18611 603 41 0 20841 0
vsize: 83528
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 51751 0 0 0 45819 181 0 0 25 0 1 0 486819695 87519232 19063 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21367 19063 603 41 0 21326 0
vsize: 85468
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 52158 0 0 0 46817 183 0 0 25 0 1 0 486819695 89059328 19470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21743 19470 603 41 0 21702 0
vsize: 86972
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 53031 0 0 0 47815 185 0 0 25 0 1 0 486819695 92639232 20343 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22617 20343 603 41 0 22576 0
vsize: 90468
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 53698 0 0 0 48814 187 0 0 25 0 1 0 486819695 95477760 21010 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23310 21010 603 41 0 23269 0
vsize: 93240
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 54503 0 0 0 49812 189 0 0 25 0 1 0 486819695 98697216 21815 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24096 21815 603 41 0 24055 0
vsize: 96384
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 55090 0 0 0 50810 191 0 0 25 0 1 0 486819695 101093376 22402 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24681 22402 603 41 0 24640 0
vsize: 98724
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 55779 0 0 0 51808 193 0 0 25 0 1 0 486819695 103964672 23091 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25382 23091 603 41 0 25341 0
vsize: 101528
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 56231 0 0 0 52807 195 0 0 25 0 1 0 486819695 105734144 23543 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25814 23543 603 41 0 25773 0
vsize: 103256
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 56474 0 0 0 53807 195 0 0 25 0 1 0 486819695 106762240 23786 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26065 23786 603 41 0 26024 0
vsize: 104260
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 56768 0 0 0 54806 196 0 0 25 0 1 0 486819695 107954176 24080 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26356 24080 603 41 0 26315 0
vsize: 105424
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 57069 0 0 0 55805 197 0 0 25 0 1 0 486819695 109150208 24381 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26648 24381 603 41 0 26607 0
vsize: 106592
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 57376 0 0 0 56804 198 0 0 25 0 1 0 486819695 110448640 24688 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26965 24688 603 41 0 26924 0
vsize: 107860
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 57722 0 0 0 57803 200 0 0 25 0 1 0 486819695 111898624 25034 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27319 25034 603 41 0 27278 0
vsize: 109276
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 58028 0 0 0 58802 200 0 0 25 0 1 0 486819695 113070080 25340 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27605 25340 603 41 0 27564 0
vsize: 110420
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 58388 0 0 0 59802 201 0 0 25 0 1 0 486819695 114638848 25700 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27988 25700 603 41 0 27947 0
vsize: 111952
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 58687 0 0 0 60801 202 0 0 25 0 1 0 486819695 115834880 25999 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28280 25999 603 41 0 28239 0
vsize: 113120
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 58991 0 0 0 61801 203 0 0 25 0 1 0 486819695 117022720 26303 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28570 26303 603 41 0 28529 0
vsize: 114280
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 59336 0 0 0 62800 204 0 0 25 0 1 0 486819695 118439936 26648 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28916 26648 603 41 0 28875 0
vsize: 115664
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 59755 0 0 0 63799 205 0 0 25 0 1 0 486819695 120123392 27067 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29327 27067 603 41 0 29286 0
vsize: 117308
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 60303 0 0 0 64797 207 0 0 25 0 1 0 486819695 122413056 27615 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29886 27615 603 41 0 29845 0
vsize: 119544
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 60856 0 0 0 65796 208 0 0 25 0 1 0 486819695 124989440 28168 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30515 28168 603 41 0 30474 0
vsize: 122060
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 61327 0 0 0 66795 209 0 0 25 0 1 0 486819695 126894080 28639 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30980 28639 603 41 0 30939 0
vsize: 123920
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 61643 0 0 0 67795 210 0 0 25 0 1 0 486819695 128192512 28955 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31297 28955 603 41 0 31256 0
vsize: 125188
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 61943 0 0 0 68794 211 0 0 25 0 1 0 486819695 129359872 29255 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31582 29255 603 41 0 31541 0
vsize: 126328
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 62259 0 0 0 69793 212 0 0 25 0 1 0 486819695 130662400 29571 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31900 29571 603 41 0 31859 0
vsize: 127600
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 62575 0 0 0 70793 213 0 0 25 0 1 0 486819695 131932160 29887 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 29887 603 41 0 32169 0
vsize: 128840
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 63021 0 0 0 71792 214 0 0 25 0 1 0 486819695 133767168 30333 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32658 30333 603 41 0 32617 0
vsize: 130632
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 63512 0 0 0 72791 215 0 0 25 0 1 0 486819695 135831552 30824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33162 30824 603 41 0 33121 0
vsize: 132648
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 64128 0 0 0 73789 217 0 0 25 0 1 0 486819695 138305536 31440 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33766 31440 603 41 0 33725 0
vsize: 135064
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 64722 0 0 0 74788 218 0 0 25 0 1 0 486819695 140832768 32034 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34383 32034 603 41 0 34342 0
vsize: 137532
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 65140 0 0 0 75787 219 0 0 25 0 1 0 486819695 142520320 32452 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34795 32452 603 41 0 34754 0
vsize: 139180
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 65658 0 0 0 76786 220 0 0 25 0 1 0 486819695 144584704 32970 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35299 32970 603 41 0 35258 0
vsize: 141196
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 66044 0 0 0 77786 221 0 0 25 0 1 0 486819695 146161664 33356 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35684 33356 603 41 0 35643 0
vsize: 142736
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 66249 0 0 0 78786 221 0 0 25 0 1 0 486819695 147070976 33561 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35906 33561 603 41 0 35865 0
vsize: 143624
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 66603 0 0 0 79785 222 0 0 25 0 1 0 486819695 148492288 33915 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36253 33915 603 41 0 36212 0
vsize: 145012
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 66760 0 0 0 80785 222 0 0 25 0 1 0 486819695 149143552 34072 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36412 34072 603 41 0 36371 0
vsize: 145648
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 67195 0 0 0 81784 223 0 0 25 0 1 0 486819695 150945792 34507 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36852 34507 603 41 0 36811 0
vsize: 147408
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 67700 0 0 0 82783 225 0 0 25 0 1 0 486819695 152915968 35012 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37333 35012 603 41 0 37292 0
vsize: 149332
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 68032 0 0 0 83783 225 0 0 25 0 1 0 486819695 154337280 35344 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37680 35344 603 41 0 37639 0
vsize: 150720
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 68446 0 0 0 84783 226 0 0 25 0 1 0 486819695 156016640 35758 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38090 35758 603 41 0 38049 0
vsize: 152360
[startup+860.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 68851 0 0 0 85782 227 0 0 25 0 1 0 486819695 157708288 36163 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38503 36163 603 41 0 38462 0
vsize: 154012
[startup+870.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 69334 0 0 0 86780 229 0 0 25 0 1 0 486819695 159666176 36646 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38981 36646 603 41 0 38940 0
vsize: 155924
[startup+880.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 69916 0 0 0 87779 230 0 0 25 0 1 0 486819695 162009088 37228 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39553 37228 603 41 0 39512 0
vsize: 158212
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 70421 0 0 0 88777 232 0 0 25 0 1 0 486819695 164089856 37733 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40061 37733 603 41 0 40020 0
vsize: 160244
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 70971 0 0 0 89776 233 0 0 25 0 1 0 486819695 166395904 38283 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40624 38283 603 41 0 40583 0
vsize: 162496
[startup+910.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 71466 0 0 0 90776 234 0 0 25 0 1 0 486819695 168308736 38778 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41091 38778 603 41 0 41050 0
vsize: 164364
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 71946 0 0 0 91774 235 0 0 25 0 1 0 486819695 170283008 39258 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41573 39258 603 41 0 41532 0
vsize: 166292
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 72517 0 0 0 92773 236 0 0 25 0 1 0 486819695 172609536 39829 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42141 39829 603 41 0 42100 0
vsize: 168564
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 73184 0 0 0 93772 238 0 0 25 0 1 0 486819695 175443968 40496 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42833 40496 603 41 0 42792 0
vsize: 171332
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 73935 0 0 0 94771 239 0 0 25 0 1 0 486819695 178491392 41247 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43577 41247 603 41 0 43536 0
vsize: 174308
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 74698 0 0 0 95768 242 0 0 25 0 1 0 486819695 181551104 42010 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44324 42010 603 41 0 44283 0
vsize: 177296
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 75300 0 0 0 96767 243 0 0 25 0 1 0 486819695 184074240 42612 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44940 42612 603 41 0 44899 0
vsize: 179760
[startup+980.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 75825 0 0 0 97766 245 0 0 25 0 1 0 486819695 186261504 43137 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45474 43137 603 41 0 45433 0
vsize: 181896
[startup+990.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 76369 0 0 0 98765 246 0 0 25 0 1 0 486819695 188366848 43681 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45988 43681 603 41 0 45947 0
vsize: 183952
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 76956 0 0 0 99764 247 0 0 25 0 1 0 486819695 190816256 44268 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46586 44268 603 41 0 46545 0
vsize: 186344
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 77805 0 0 0 100763 249 0 0 25 0 1 0 486819695 194342912 45117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47447 45117 603 41 0 47406 0
vsize: 189788
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 78269 0 0 0 101762 249 0 0 25 0 1 0 486819695 196157440 45581 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47890 45581 603 41 0 47849 0
vsize: 191560
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 78712 0 0 0 102761 251 0 0 25 0 1 0 486819695 198012928 46024 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48343 46024 603 41 0 48302 0
vsize: 193372
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 79191 0 0 0 103760 252 0 0 25 0 1 0 486819695 199974912 46503 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48822 46503 603 41 0 48781 0
vsize: 195288
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 79695 0 0 0 104759 254 0 0 25 0 1 0 486819695 201986048 47007 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49313 47007 603 41 0 49272 0
vsize: 197252
[startup+1060.04 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 80187 0 0 0 105758 255 0 0 25 0 1 0 486819695 204042240 47499 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49815 47499 603 41 0 49774 0
vsize: 199260
[startup+1070.04 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 80556 0 0 0 106757 255 0 0 25 0 1 0 486819695 205504512 47868 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50172 47868 603 41 0 50131 0
vsize: 200688
[startup+1080.04 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 81085 0 0 0 107756 257 0 0 25 0 1 0 486819695 207769600 48397 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50725 48397 603 41 0 50684 0
vsize: 202900
[startup+1090.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 81433 0 0 0 108755 258 0 0 25 0 1 0 486819695 209195008 48745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51073 48745 603 41 0 51032 0
vsize: 204292
[startup+1100.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 81885 0 0 0 109755 259 0 0 25 0 1 0 486819695 210964480 49197 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51505 49197 603 41 0 51464 0
vsize: 206020
[startup+1110.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 82294 0 0 0 110754 259 0 0 25 0 1 0 486819695 212639744 49606 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51914 49606 603 41 0 51873 0
vsize: 207656
[startup+1120.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 82948 0 0 0 111752 262 0 0 25 0 1 0 486819695 215330816 50260 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52571 50260 603 41 0 52530 0
vsize: 210284
[startup+1130.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 83611 0 0 0 112751 263 0 0 25 0 1 0 486819695 218009600 50923 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53225 50923 603 41 0 53184 0
vsize: 212900
[startup+1140.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 84157 0 0 0 113750 264 0 0 25 0 1 0 486819695 220229632 51469 4294967295 134512640 134672761 3221224544 3221223744 134610705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53767 51469 603 41 0 53726 0
vsize: 215068
[startup+1150.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 87837 0 0 0 114739 275 0 0 25 0 1 0 486819695 222674944 52067 4294967295 134512640 134672761 3221224544 3221223800 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54364 52067 603 41 0 54323 0
vsize: 217456
[startup+1160.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 87999 0 0 0 115738 275 0 0 25 0 1 0 486819695 223199232 52152 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54492 52152 603 41 0 54451 0
vsize: 217968
[startup+1170.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 87999 0 0 0 116737 275 0 0 25 0 1 0 486819695 223199232 52152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54492 52152 603 41 0 54451 0
vsize: 217968
[startup+1180.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 87999 0 0 0 117737 276 0 0 25 0 1 0 486819695 223199232 52152 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54492 52152 603 41 0 54451 0
vsize: 217968
[startup+1190.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 87999 0 0 0 118737 276 0 0 25 0 1 0 486819695 223199232 52152 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54492 52152 603 41 0 54451 0
vsize: 217968
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12249
Raw data (stat): 12249 (minisat+) R 12248 10720 10719 0 -1 0 87999 0 0 0 119737 276 0 0 25 0 1 0 486819695 223199232 52152 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54492 52152 603 41 0 54451 0
vsize: 217968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 12249
Raw data (stat): 12249 (minisat+) Z 12248 10720 10719 0 -1 12 88000 0 0 0 119738 286 0 0 25 0 1 0 486819695 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.15
CPU time (s): 1200.24
CPU user time (s): 1197.38
CPU system time (s): 2.86356
CPU usage (%): 100.008
Max. virtual memory (Kb): 217968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####