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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-2.opb
MD5SUM	270e069f649d19b0da4e4d23c0e1ebfc
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	760
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	760
Total number of constraints	41263
Number of constraints which are clauses	41263
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5618

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        900300 kB
Buffers:         34824 kB
Cached:          78800 kB
SwapCached:          4 kB
Active:          57548 kB
Inactive:        58916 kB
HighTotal:      131008 kB
HighFree:        48440 kB
LowTotal:       903652 kB
LowFree:        851860 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12360 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:17:48 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4085 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41263 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 |   41263    82526 |   12378       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   41263    82526 |   16505       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.70874 s)
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   77411   167438 |   23223       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24738          
c   -- var.elim.:  2000/24738          
c   -- var.elim.:  3000/24738          
c   -- var.elim.:  4000/24738          
c   -- var.elim.:  5000/24738          
c   -- var.elim.:  6000/24738          
c   -- var.elim.:  7000/24738          
c   -- var.elim.:  8000/24738          
c   -- var.elim.:  9000/24738          
c   -- var.elim.:  10000/24738          
c   -- var.elim.:  11000/24738          
c   -- var.elim.:  12000/24738          
c   -- var.elim.:  13000/24738          
c   -- var.elim.:  14000/24738          
c   -- var.elim.:  15000/24738          
c   -- var.elim.:  16000/24738          
c   -- var.elim.:  17000/24738          
c   -- var.elim.:  18000/24738          
c   -- var.elim.:  19000/24738          
c   -- var.elim.:  20000/24738          
c   -- var.elim.:  21000/24738          
c   -- var.elim.:  22000/24738          
c   -- var.elim.:  23000/24738          
c   -- var.elim.:  24000/24738          
c   -- var.elim.:  24738/24738          
c   -- var.elim.:  1000/12567          
c   -- var.elim.:  2000/12567          
c   -- var.elim.:  3000/12567          
c   -- var.elim.:  4000/12567          
c   -- var.elim.:  5000/12567          
c   -- var.elim.:  6000/12567          
c   -- var.elim.:  7000/12567          
c   -- var.elim.:  8000/12567          
c   -- var.elim.:  9000/12567          
c   -- var.elim.:  10000/12567          
c   -- var.elim.:  11000/12567          
c   -- var.elim.:  12000/12567          
c   -- var.elim.:  12567/12567          
c   -- var.elim.:  1000/2560          
c   -- var.elim.:  2000/2560          
c   -- var.elim.:  2560/2560          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  1000/4992          
c   -- var.elim.:  2000/4992          
c   -- var.elim.:  3000/4992          
c   -- var.elim.:  4000/4992          
c   -- var.elim.:  4992/4992          
c   -- var.elim.:  282/282          
c |         0 |   51927   167225 |      --       0       --      -- |     --   | -25484/-212
c |         0 |   51927   167225 |   20770       0        0     nan |  0.000 % |
c |       100 |   51927   167225 |   22847     100    12937   129.4 | 52.695 % |
c |       251 |   51927   167225 |   25132     251    32632   130.0 | 52.695 % |
c |       476 |   51927   167225 |   27645     476    64713   136.0 | 52.695 % |
c |       814 |   51889   166476 |   30388     809   116950   144.6 | 52.807 % |
c |      1320 |   51889   166476 |   33427    1315   178398   135.7 | 52.807 % |
c |      2079 |   51861   166209 |   36749    2071   301540   145.6 | 52.920 % |
c |      3218 |   51779   165416 |   40361    3204   523153   163.3 | 53.151 % |
c ==============================================================================
c (current CPU-time: 58.6381 s)
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3582 |   51785   165220 |   15535    3565   582715   163.5 | 53.151 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4996          
c   -- var.elim.:  2000/4996          
c   -- var.elim.:  3000/4996          
c   -- var.elim.:  4000/4996          
c   -- var.elim.:  4996/4996          
c   -- var.elim.:  149/149          
c   -- var.elim.:  61/61          
c |      3582 |   51692   164951 |      --    3565       --      -- |     --   | -83/-83
c |      3582 |   51692   164951 |   20676    3187   335930   105.4 | 53.151 % |
c |      3683 |   51692   164951 |   22744    3288   359919   109.5 | 53.431 % |
c |      3833 |   51692   164951 |   25018    3438   376860   109.6 | 53.431 % |
c |      4058 |   51692   164951 |   27520    3663   425424   116.1 | 53.431 % |
c |      4395 |   51692   164951 |   30272    4000   495562   123.9 | 53.431 % |
c |      4901 |   51692   164951 |   33300    4506   600160   133.2 | 53.431 % |
c |      5660 |   51692   164951 |   36630    5265   791773   150.4 | 53.431 % |
c |      6801 |   51584   164054 |   40209    6397  1024322   160.1 | 53.815 % |
c |      8510 |   51548   163693 |   44199    8098  1384315   170.9 | 53.960 % |
c ==============================================================================
c (current CPU-time: 76.8533 s)
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11027 |   56550   176173 |   16964   10587  1953611   184.5 | 53.960 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9622          
c   -- var.elim.:  2000/9622          
c   -- var.elim.:  3000/9622          
c   -- var.elim.:  4000/9622          
c   -- var.elim.:  5000/9622          
c   -- var.elim.:  6000/9622          
c   -- var.elim.:  7000/9622          
c   -- var.elim.:  8000/9622          
c   -- var.elim.:  9000/9622          
c   -- var.elim.:  9622/9622          
c   -- var.elim.:  1000/3601          
c   -- var.elim.:  2000/3601          
c   -- var.elim.:  3000/3601          
c   -- var.elim.:  3601/3601          
c   -- var.elim.:  200/200          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  1000/3618          
c   -- var.elim.:  2000/3618          
c   -- var.elim.:  3000/3618          
c   -- var.elim.:  3618/3618          
c   -- var.elim.:  37/37          
c |     11027 |   51506   170110 |      --   10587       --      -- |     --   | -5034/-6042
c |     11027 |   51506   170110 |   20602   10587  1953611   184.5 | 53.960 % |
c |     11127 |   51506   170110 |   22662   10687  1982390   185.5 | 64.182 % |
c |     11277 |   51482   169907 |   24917   10742  1930317   179.7 | 64.257 % |
c |     11502 |   51482   169907 |   27409   10967  1979944   180.5 | 64.257 % |
c |     11839 |   51431   169487 |   30120   11299  2061707   182.5 | 64.389 % |
c |     12345 |   51333   168711 |   33068   11797  2175614   184.4 | 64.664 % |
c |     13104 |   51333   168711 |   36375   12556  2368216   188.6 | 64.664 % |
c |     14243 |   51181   167266 |   39894   13674  2558940   187.1 | 65.115 % |
c |     15952 |   51043   166000 |   43766   15350  3054393   199.0 | 65.548 % |
c |     18514 |   50719   163036 |   47837   17844  3626038   203.2 | 66.562 % |
c |     22358 |   50318   159459 |   52204   21550  4567944   212.0 | 67.790 % |
c ==============================================================================
c (current CPU-time: 143.254 s)
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26972 |   50127   156080 |   15038   26061  5903615   226.5 | 67.790 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4951          
c   -- var.elim.:  2000/4951          
c   -- var.elim.:  3000/4951          
c   -- var.elim.:  4000/4951          
c   -- var.elim.:  4951/4951          
c   -- var.elim.:  256/256          
c |     26972 |   49868   154609 |      --   26061       --      -- |     --   | -249/-916
c |     26972 |   49868   154609 |   19947   26061  5903615   226.5 | 67.790 % |
c |     27072 |   49868   154609 |   21941   26161  5925393   226.5 | 69.358 % |
c |     27222 |   49868   154609 |   24136   26311  5967986   226.8 | 69.358 % |
c |     27448 |   49868   154609 |   26549   26537  6016942   226.7 | 69.358 % |
c |     27785 |   49868   154609 |   29204   26874  6094467   226.8 | 69.358 % |
c |     28292 |   49868   154609 |   32125   27381  6228384   227.5 | 69.358 % |
c |     29051 |   49818   154158 |   35302   25001  4022816   160.9 | 69.514 % |
c |     30190 |   49676   152876 |   38721   26098  4290004   164.4 | 69.944 % |
c ==============================================================================
c (current CPU-time: 160.582 s)
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     30951 |   51371   157671 |   15411   26859  4427959   164.9 | 69.944 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5960          
c   -- var.elim.:  2000/5960          
c   -- var.elim.:  3000/5960          
c   -- var.elim.:  4000/5960          
c   -- var.elim.:  5000/5960          
c   -- var.elim.:  5960/5960          
c   -- var.elim.:  1000/1431          
c   -- var.elim.:  1431/1431          
c |     30951 |   49723   155303 |      --   26859       --      -- |     --   | -1648/-2367
c |     30951 |   49723   155303 |   19889   26611  4358049   163.8 | 69.944 % |
c |     31052 |   49723   155303 |   21878   26712  4372262   163.7 | 70.259 % |
c |     31202 |   49723   155303 |   24065   26862  4400074   163.8 | 70.259 % |
c |     31428 |   49723   155303 |   26472   27088  4473173   165.1 | 70.259 % |
c |     31765 |   49723   155303 |   29119   27425  4561286   166.3 | 70.259 % |
c |     32271 |   49723   155303 |   32031   27931  4685661   167.8 | 70.259 % |
c |     33030 |   49697   155094 |   35216   28683  4933799   172.0 | 70.339 % |
c |     34170 |   49667   154777 |   38714   29818  5360273   179.8 | 70.431 % |
c |     35878 |   49641   154523 |   42563   31519  5792378   183.8 | 70.511 % |
c |     38440 |   49507   153266 |   46693   34015  6459210   189.9 | 70.911 % |
c |     42284 |   49346   151743 |   51196   37815  7481480   197.8 | 71.392 % |
c ==============================================================================
c (current CPU-time: 210.119 s)
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     42952 |   50113   154048 |   15033   38483  7659330   199.0 | 71.392 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5096          
c   -- var.elim.:  2000/5096          
c   -- var.elim.:  3000/5096          
c   -- var.elim.:  4000/5096          
c   -- var.elim.:  5000/5096          
c   -- var.elim.:  5096/5096          
c   -- var.elim.:  823/823          
c |     42952 |   49334   149900 |      --   38483       --      -- |     --   | -763/-1576
c |     42952 |   49334   149900 |   19733   36450  6448693   176.9 | 71.392 % |
c |     43054 |   49334   149900 |   21706   16911  2404877   142.2 | 71.440 % |
c |     43204 |   49334   149900 |   23877   17061  2433070   142.6 | 71.440 % |
c |     43429 |   49308   149662 |   26251   17282  2466154   142.7 | 71.514 % |
c |     43766 |   49308   149662 |   28876   17619  2561995   145.4 | 71.514 % |
c |     44272 |   49308   149662 |   31764   18125  2702642   149.1 | 71.514 % |
c |     45031 |   49308   149662 |   34940   18884  2856798   151.3 | 71.514 % |
c |     46170 |   49308   149662 |   38434   20023  3103939   155.0 | 71.514 % |
c |     47878 |   49308   149662 |   42278   21731  3546949   163.2 | 71.514 % |
c |     50441 |   49306   149643 |   46504   24290  4303040   177.2 | 71.520 % |
c |     54285 |   49229   148949 |   51074   28123  5367421   190.9 | 71.748 % |
c |     60051 |   49229   148949 |   56182   33889  7250249   213.9 | 71.748 % |
c |     68701 |   49056   147471 |   61583   42468  9777507   230.2 | 72.259 % |
c |     81676 |   48634   143777 |   67159   55213 13747586   249.0 | 73.541 % |
c ==============================================================================
c (current CPU-time: 450.919 s)
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     95087 |   52059   150424 |   15617   68502 17824881   260.2 | 73.541 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7166          
c   -- var.elim.:  2000/7166          
c   -- var.elim.:  3000/7166          
c   -- var.elim.:  4000/7166          
c   -- var.elim.:  5000/7166          
c   -- var.elim.:  6000/7166          
c   -- var.elim.:  7000/7166          
c   -- var.elim.:  7166/7166          
c   -- var.elim.:  1000/2429          
c   -- var.elim.:  2000/2429          
c   -- var.elim.:  2429/2429          
c   -- var.elim.:  53/53          
c |     95087 |   48355   143814 |      --   68502       --      -- |     --   | -3687/-6575
c |     95087 |   48355   143814 |   19342   68497 17824869   260.2 | 73.541 % |
c |     95188 |   48325   143573 |   21263   22103  4039196   182.7 | 76.737 % |
c |     95338 |   48325   143573 |   23389   22253  4061512   182.5 | 76.737 % |
c |     95563 |   48325   143573 |   25728   22478  4109195   182.8 | 76.737 % |
c |     95900 |   48325   143573 |   28301   22815  4175757   183.0 | 76.737 % |
c |     96406 |   48299   143375 |   31114   23299  4254390   182.6 | 76.810 % |
c |     97165 |   48210   142554 |   34162   24053  4467921   185.8 | 77.052 % |
c |     98304 |   48210   142554 |   37579   25192  4774283   189.5 | 77.052 % |
c |    100012 |   48210   142554 |   41336   26900  5361067   199.3 | 77.052 % |
c |    102575 |   48176   142220 |   45438   29452  6075565   206.3 | 77.148 % |
c |    106419 |   48152   142007 |   49957   33291  7119074   213.8 | 77.210 % |
c |    112185 |   48122   141764 |   54919   39048  8839814   226.4 | 77.289 % |
c |    120835 |   47825   139004 |   60038   47595 11433467   240.2 | 78.083 % |
c |    133809 |   47588   136775 |   65714   60504 15435915   255.1 | 78.741 % |
c |    153271 |   47241   133639 |   71759   79869 21266811   266.3 | 79.687 % |
c |    182463 |   46867   130400 |   78310   46059 11060834   240.1 | 80.717 % |
c |    226252 |   46318   125804 |   85131   89583 24382458   272.2 | 82.204 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 C744 -C743 -C742 -C741 -C740 C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 C611 -C610 -C609 -C608 -C607 -C606 C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C35#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 24352
Raw data (stat): 24352 (runsolver) R 24351 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422228733 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 4988 0 0 0 975 23 0 0 25 0 1 0 422228733 22355968 4698 4294967295 134512640 134672761 3221224560 3221222816 134621268 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5458 4698 603 41 0 5417 0
vsize: 21832
[startup+19.9997 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 5012 0 0 0 1975 23 0 0 25 0 1 0 422228733 22519808 4722 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5498 4722 603 41 0 5457 0
vsize: 21992
[startup+30.0007 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 5033 0 0 0 2975 23 0 0 25 0 1 0 422228733 22519808 4743 4294967295 134512640 134672761 3221224560 3221223056 134644260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5498 4743 603 41 0 5457 0
vsize: 21992
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 5039 0 0 0 3975 23 0 0 25 0 1 0 422228733 22519808 4749 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5498 4749 603 41 0 5457 0
vsize: 21992
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 5191 0 0 0 4975 23 0 0 25 0 1 0 422228733 23576576 4901 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5756 4901 603 41 0 5715 0
vsize: 23024
[startup+60.0005 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 6517 0 0 0 5969 29 0 0 25 0 1 0 422228733 25866240 5449 4294967295 134512640 134672761 3221224560 3221223104 134621104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6315 5449 603 41 0 6274 0
vsize: 25260
[startup+70.0005 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 6982 0 0 0 6968 30 0 0 25 0 1 0 422228733 26796032 5762 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6542 5762 603 41 0 6501 0
vsize: 26168
[startup+80.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 8858 0 0 0 7955 43 0 0 25 0 1 0 422228733 33390592 6987 4294967295 134512640 134672761 3221224560 3221223008 134643719 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8152 6987 603 41 0 8111 0
vsize: 32608
[startup+90.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 9010 0 0 0 8950 48 0 0 25 0 1 0 422228733 34459648 7139 4294967295 134512640 134672761 3221224560 3221222144 134566704 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8413 7139 603 41 0 8372 0
vsize: 33652
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 9231 0 0 0 9949 49 0 0 25 0 1 0 422228733 34308096 7208 4294967295 134512640 134672761 3221224560 3221223600 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7208 603 41 0 8335 0
vsize: 33504
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 10140 0 0 0 10948 51 0 0 25 0 1 0 422228733 38121472 8117 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9307 8117 603 41 0 9266 0
vsize: 37228
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 10773 0 0 0 11946 53 0 0 25 0 1 0 422228733 40681472 8750 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9932 8750 603 41 0 9891 0
vsize: 39728
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24352
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 11713 0 0 0 12944 55 0 0 25 0 1 0 422228733 44601344 9690 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10889 9690 603 41 0 10848 0
vsize: 43556
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 3/57 24387
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 12569 0 0 0 13940 58 0 0 25 0 1 0 422228733 48009216 10546 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11721 10546 603 41 0 11680 0
vsize: 46884
[startup+150.005 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 14251 0 0 0 14933 66 0 0 25 0 1 0 422228733 49561600 10916 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 10916 603 41 0 12059 0
vsize: 48400
[startup+160.005 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 14580 0 0 0 15932 67 0 0 25 0 1 0 422228733 50847744 11245 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12414 11245 603 41 0 12373 0
vsize: 49656
[startup+170.005 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 15871 0 0 0 16923 76 0 0 25 0 1 0 422228733 51052544 11339 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12464 11339 603 41 0 12423 0
vsize: 49856
[startup+180.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 15873 0 0 0 17922 76 0 0 25 0 1 0 422228733 51052544 11341 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12464 11341 603 41 0 12423 0
vsize: 49856
[startup+190.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 15966 0 0 0 18922 76 0 0 25 0 1 0 422228733 51572736 11434 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12591 11434 603 41 0 12550 0
vsize: 50364
[startup+200.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 16537 0 0 0 19921 77 0 0 25 0 1 0 422228733 53919744 12005 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13164 12005 603 41 0 13123 0
vsize: 52656
[startup+210.007 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 24405
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 17281 0 0 0 20920 79 0 0 25 0 1 0 422228733 56946688 12749 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13903 12749 603 41 0 13862 0
vsize: 55612
[startup+220.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 18959 0 0 0 21910 88 0 0 25 0 1 0 422228733 57532416 12913 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14046 12913 603 41 0 14005 0
vsize: 56184
[startup+230.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 18959 0 0 0 22910 88 0 0 25 0 1 0 422228733 57532416 12913 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14046 12913 603 41 0 14005 0
vsize: 56184
[startup+240.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 18959 0 0 0 23910 88 0 0 25 0 1 0 422228733 57532416 12913 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14046 12913 603 41 0 14005 0
vsize: 56184
[startup+250.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 18959 0 0 0 24910 88 0 0 25 0 1 0 422228733 57532416 12913 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14046 12913 603 41 0 14005 0
vsize: 56184
[startup+260.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 18959 0 0 0 25910 88 0 0 25 0 1 0 422228733 57532416 12913 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14046 12913 603 41 0 14005 0
vsize: 56184
[startup+270.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 18959 0 0 0 26911 88 0 0 25 0 1 0 422228733 57532416 12913 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14046 12913 603 41 0 14005 0
vsize: 56184
[startup+280.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 19479 0 0 0 27910 89 0 0 25 0 1 0 422228733 59752448 13433 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14588 13433 603 41 0 14547 0
vsize: 58352
[startup+290.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 20290 0 0 0 28909 91 0 0 25 0 1 0 422228733 63033344 14244 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15389 14244 603 41 0 15348 0
vsize: 61556
[startup+300.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 21201 0 0 0 29907 93 0 0 25 0 1 0 422228733 66768896 15155 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 15155 603 41 0 16260 0
vsize: 65204
[startup+310.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 22010 0 0 0 30905 95 0 0 25 0 1 0 422228733 70041600 15964 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17100 15964 603 41 0 17059 0
vsize: 68400
[startup+320.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 22746 0 0 0 31903 98 0 0 25 0 1 0 422228733 73019392 16700 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17827 16700 603 41 0 17786 0
vsize: 71308
[startup+330.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 23433 0 0 0 32902 99 0 0 25 0 1 0 422228733 75878400 17387 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17387 603 41 0 18484 0
vsize: 74100
[startup+340.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 23832 0 0 0 33901 100 0 0 25 0 1 0 422228733 77447168 17786 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18908 17786 603 41 0 18867 0
vsize: 75632
[startup+350.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 24363 0 0 0 34901 100 0 0 25 0 1 0 422228733 79654912 18317 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19447 18317 603 41 0 19406 0
vsize: 77788
[startup+360.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 24888 0 0 0 35900 102 0 0 25 0 1 0 422228733 81883136 18842 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19991 18842 603 41 0 19950 0
vsize: 79964
[startup+370.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 25283 0 0 0 36899 102 0 0 25 0 1 0 422228733 83472384 19237 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20379 19237 603 41 0 20338 0
vsize: 81516
[startup+380.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 25735 0 0 0 37898 104 0 0 25 0 1 0 422228733 85315584 19689 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20829 19689 603 41 0 20788 0
vsize: 83316
[startup+390.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 26396 0 0 0 38897 105 0 0 25 0 1 0 422228733 88039424 20350 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20350 603 41 0 21453 0
vsize: 85976
[startup+400.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 26909 0 0 0 39896 107 0 0 25 0 1 0 422228733 90112000 20863 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22000 20863 603 41 0 21959 0
vsize: 88000
[startup+410.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 27346 0 0 0 40895 108 0 0 25 0 1 0 422228733 91820032 21300 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22417 21301 603 41 0 22376 0
vsize: 89668
[startup+420.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 27877 0 0 0 41893 110 0 0 25 0 1 0 422228733 94040064 21831 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22959 21831 603 41 0 22918 0
vsize: 91836
[startup+430.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 28355 0 0 0 42892 110 0 0 25 0 1 0 422228733 95997952 22309 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23437 22309 603 41 0 23396 0
vsize: 93748
[startup+440.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 28739 0 0 0 43892 111 0 0 25 0 1 0 422228733 97837056 22693 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23886 22693 603 41 0 23845 0
vsize: 95544
[startup+450.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 29394 0 0 0 44891 113 0 0 25 0 1 0 422228733 100450304 23348 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24524 23348 603 41 0 24483 0
vsize: 98096
[startup+460.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31459 0 0 0 45875 127 0 0 25 0 1 0 422228733 101974016 23805 4294967295 134512640 134672761 3221224560 3221223816 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24896 23805 603 41 0 24855 0
vsize: 99584
[startup+470.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 46874 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+480.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24407
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 47874 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+490.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 48874 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+500.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 49875 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+510.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 50875 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+520.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 51875 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+530.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 52875 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+540.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 53876 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+550.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 54876 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+560.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 55876 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+570.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 56876 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+580.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 57876 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+590.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 58877 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+600.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 59877 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+610.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 60877 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+620.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31574 0 0 0 61877 128 0 0 25 0 1 0 422228733 102236160 23853 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23853 603 41 0 24919 0
vsize: 99840
[startup+630.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31575 0 0 0 62877 128 0 0 25 0 1 0 422228733 102236160 23854 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23854 603 41 0 24919 0
vsize: 99840
[startup+640.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31575 0 0 0 63878 128 0 0 25 0 1 0 422228733 102236160 23854 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23854 603 41 0 24919 0
vsize: 99840
[startup+650.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31575 0 0 0 64878 128 0 0 25 0 1 0 422228733 102236160 23854 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23854 603 41 0 24919 0
vsize: 99840
[startup+660.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31575 0 0 0 65878 128 0 0 25 0 1 0 422228733 102236160 23854 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23854 603 41 0 24919 0
vsize: 99840
[startup+670.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31575 0 0 0 66878 128 0 0 25 0 1 0 422228733 102236160 23854 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23854 603 41 0 24919 0
vsize: 99840
[startup+680.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31576 0 0 0 67878 128 0 0 25 0 1 0 422228733 102236160 23855 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 23855 603 41 0 24919 0
vsize: 99840
[startup+690.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 31807 0 0 0 68879 128 0 0 25 0 1 0 422228733 103284736 24086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25216 24086 603 41 0 25175 0
vsize: 100864
[startup+700.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 32447 0 0 0 69878 129 0 0 25 0 1 0 422228733 105897984 24726 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25854 24726 603 41 0 25813 0
vsize: 103416
[startup+710.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 33055 0 0 0 70876 130 0 0 25 0 1 0 422228733 108376064 25334 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25334 603 41 0 26418 0
vsize: 105836
[startup+720.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 33663 0 0 0 71876 131 0 0 25 0 1 0 422228733 110866432 25942 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27067 25942 603 41 0 27026 0
vsize: 108268
[startup+730.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 34050 0 0 0 72875 132 0 0 25 0 1 0 422228733 112427008 26329 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27448 26329 603 41 0 27407 0
vsize: 109792
[startup+740.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 34377 0 0 0 73874 133 0 0 25 0 1 0 422228733 113754112 26656 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27772 26656 603 41 0 27731 0
vsize: 111088
[startup+750.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 34607 0 0 0 74874 134 0 0 25 0 1 0 422228733 114683904 26886 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27999 26886 603 41 0 27958 0
vsize: 111996
[startup+760.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 34931 0 0 0 75873 134 0 0 25 0 1 0 422228733 115994624 27210 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28319 27210 603 41 0 28278 0
vsize: 113276
[startup+770.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 35259 0 0 0 76873 135 0 0 25 0 1 0 422228733 117428224 27538 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28669 27538 603 41 0 28628 0
vsize: 114676
[startup+780.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 35711 0 0 0 77872 136 0 0 25 0 1 0 422228733 119259136 27990 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29116 27990 603 41 0 29075 0
vsize: 116464
[startup+790.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 36290 0 0 0 78870 138 0 0 25 0 1 0 422228733 121581568 28569 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29683 28569 603 41 0 29642 0
vsize: 118732
[startup+800.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 36744 0 0 0 79868 140 0 0 25 0 1 0 422228733 123408384 29023 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30129 29023 603 41 0 30088 0
vsize: 120516
[startup+810.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37274 0 0 0 80867 141 0 0 25 0 1 0 422228733 125628416 29553 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30671 29553 603 41 0 30630 0
vsize: 122684
[startup+820.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 81866 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+830.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 82867 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+840.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 83867 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+850.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 84867 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+860.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 85867 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+870.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 86867 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+880.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 87867 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+890.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 88868 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+900.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 89868 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+910.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 90868 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+920.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 91868 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+930.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 92868 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+940.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 93869 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+950.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 94869 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+960.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37636 0 0 0 95869 142 0 0 25 0 1 0 422228733 126631936 29830 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29830 603 41 0 30875 0
vsize: 123664
[startup+970.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 96869 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+980.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 97870 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+990.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 98870 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 99870 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 100870 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 101870 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 102871 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 103871 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 104871 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37637 0 0 0 105871 142 0 0 25 0 1 0 422228733 126631936 29831 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29831 603 41 0 30875 0
vsize: 123664
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37638 0 0 0 106871 142 0 0 25 0 1 0 422228733 126631936 29832 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29832 603 41 0 30875 0
vsize: 123664
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37639 0 0 0 107872 142 0 0 25 0 1 0 422228733 126631936 29833 4294967295 134512640 134672761 3221224560 3221223704 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29833 603 41 0 30875 0
vsize: 123664
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37640 0 0 0 108872 142 0 0 25 0 1 0 422228733 126631936 29834 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29834 603 41 0 30875 0
vsize: 123664
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37642 0 0 0 109872 142 0 0 25 0 1 0 422228733 126631936 29836 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29836 603 41 0 30875 0
vsize: 123664
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37642 0 0 0 110872 142 0 0 25 0 1 0 422228733 126631936 29836 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29836 603 41 0 30875 0
vsize: 123664
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37642 0 0 0 111872 142 0 0 25 0 1 0 422228733 126631936 29836 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29836 603 41 0 30875 0
vsize: 123664
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37642 0 0 0 112873 142 0 0 25 0 1 0 422228733 126631936 29836 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29836 603 41 0 30875 0
vsize: 123664
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37642 0 0 0 113873 142 0 0 25 0 1 0 422228733 126631936 29836 4294967295 134512640 134672761 3221224560 3221223600 134612663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29836 603 41 0 30875 0
vsize: 123664
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 37642 0 0 0 114873 142 0 0 25 0 1 0 422228733 126631936 29836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30916 29836 603 41 0 30875 0
vsize: 123664
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 38008 0 0 0 115872 143 0 0 25 0 1 0 422228733 128241664 30202 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31309 30202 603 41 0 31268 0
vsize: 125236
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 38448 0 0 0 116871 144 0 0 25 0 1 0 422228733 129953792 30642 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31727 30642 603 41 0 31686 0
vsize: 126908
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 38749 0 0 0 117871 145 0 0 25 0 1 0 422228733 131248128 30943 4294967295 134512640 134672761 3221224560 3221223744 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32043 30943 603 41 0 32002 0
vsize: 128172
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 39175 0 0 0 118869 146 0 0 25 0 1 0 422228733 132968448 31369 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32463 31369 603 41 0 32422 0
vsize: 129852
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 24409
Raw data (stat): 24352 (minisat+) R 24351 20937 20936 0 -1 0 39676 0 0 0 119869 147 0 0 25 0 1 0 422228733 135061504 31870 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32974 31870 603 41 0 32933 0
vsize: 131896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 24409
Raw data (stat): 24352 (minisat+) Z 24351 20937 20936 0 -1 12 39677 0 0 0 119869 155 0 0 25 0 1 0 422228733 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.13
CPU time (s): 1200.25
CPU user time (s): 1198.69
CPU system time (s): 1.55476
CPU usage (%): 100.01
Max. virtual memory (Kb): 131896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####