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-4.opb
MD5SUM	7731f50c352d2fd7b2fe148b68bfdbab
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	41605
Number of constraints which are clauses	41605
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 5619

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 00:57:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4087 boxname=wulflinc25 idbench=327 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7731f50c352d2fd7b2fe148b68bfdbab  /oldhome/oroussel/tmp/wulflinc25/normalized-frb40-19-4.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-frb40-19-4.opb /oldhome/oroussel/tmp/wulflinc25/normalized-frb40-19-4.opb
IDLAUNCH: 4087
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893304 kB
Buffers:         34396 kB
Cached:          72056 kB
SwapCached:         36 kB
Active:          49236 kB
Inactive:        60096 kB
HighTotal:      131008 kB
HighFree:        55244 kB
LowTotal:       903652 kB
LowFree:        838060 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26488 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:17:51 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4087 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41605 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 |   41605    83210 |   12481       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   41605    83210 |   16642       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.74973 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 |   77753   168122 |   23325       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/12569          
c   -- var.elim.:  2000/12569          
c   -- var.elim.:  3000/12569          
c   -- var.elim.:  4000/12569          
c   -- var.elim.:  5000/12569          
c   -- var.elim.:  6000/12569          
c   -- var.elim.:  7000/12569          
c   -- var.elim.:  8000/12569          
c   -- var.elim.:  9000/12569          
c   -- var.elim.:  10000/12569          
c   -- var.elim.:  11000/12569          
c   -- var.elim.:  12000/12569          
c   -- var.elim.:  12569/12569          
c   -- var.elim.:  1000/2558          
c   -- var.elim.:  2000/2558          
c   -- var.elim.:  2558/2558          
c   -- subsuming                       
c   -- var.elim.:  1000/4973          
c   -- var.elim.:  2000/4973          
c   -- var.elim.:  3000/4973          
c   -- var.elim.:  4000/4973          
c   -- var.elim.:  4973/4973          
c   -- var.elim.:  288/288          
c |         0 |   52229   166907 |      --       0       --      -- |     --   | -25524/-1214
c |         0 |   52229   166907 |   20891       0        0     nan |  0.000 % |
c |       101 |   52229   166907 |   22980     101    26731   264.7 | 52.847 % |
c |       251 |   52229   166907 |   25278     251    53736   214.1 | 52.847 % |
c |       477 |   52229   166907 |   27806     477    97272   203.9 | 52.847 % |
c |       814 |   52229   166907 |   30587     814   166882   205.0 | 52.847 % |
c |      1320 |   52229   166907 |   33646    1320   255446   193.5 | 52.847 % |
c |      2079 |   52157   166354 |   36959    2063   373386   181.0 | 53.111 % |
c ==============================================================================
c (current CPU-time: 56.6944 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 |      2235 |   57484   180698 |   17245    2219   400132   180.3 | 53.111 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9742          
c   -- var.elim.:  2000/9742          
c   -- var.elim.:  3000/9742          
c   -- var.elim.:  4000/9742          
c   -- var.elim.:  5000/9742          
c   -- var.elim.:  6000/9742          
c   -- var.elim.:  7000/9742          
c   -- var.elim.:  8000/9742          
c   -- var.elim.:  9000/9742          
c   -- var.elim.:  9742/9742          
c   -- var.elim.:  1000/4369          
c   -- var.elim.:  2000/4369          
c   -- var.elim.:  3000/4369          
c   -- var.elim.:  4000/4369          
c   -- var.elim.:  4369/4369          
c   -- var.elim.:  196/196          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/4178          
c   -- var.elim.:  2000/4178          
c   -- var.elim.:  3000/4178          
c   -- var.elim.:  4000/4178          
c   -- var.elim.:  4178/4178          
c   -- var.elim.:  37/37          
c |      2235 |   52278   175929 |      --    2219       --      -- |     --   | -5198/-4752
c |      2235 |   52278   175929 |   20911    2217   399720   180.3 | 53.111 % |
c |      2336 |   52217   175396 |   22975    2314   408364   176.5 | 62.730 % |
c |      2487 |   52096   173693 |   25214    2459   416224   169.3 | 63.072 % |
c |      2712 |   52045   173235 |   27708    2679   443981   165.7 | 63.212 % |
c |      3049 |   51941   172410 |   30418    3010   478726   159.0 | 63.478 % |
c |      3555 |   51941   172410 |   33460    3516   562891   160.1 | 63.478 % |
c |      4315 |   51534   168102 |   36518    4226   667509   158.0 | 64.657 % |
c |      5454 |   51286   165796 |   39976    5338   889865   166.7 | 65.437 % |
c |      7163 |   50847   161965 |   43598    6928  1167116   168.5 | 66.819 % |
c |      9725 |   50480   158567 |   47611    9402  1640052   174.4 | 67.941 % |
c ==============================================================================
c (current CPU-time: 95.0765 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 |      9938 |   52157   163348 |   15647    9615  1701535   177.0 | 67.941 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6567          
c   -- var.elim.:  2000/6567          
c   -- var.elim.:  3000/6567          
c   -- var.elim.:  4000/6567          
c   -- var.elim.:  5000/6567          
c   -- var.elim.:  6000/6567          
c   -- var.elim.:  6567/6567          
c   -- var.elim.:  1000/1535          
c   -- var.elim.:  1535/1535          
c   -- var.elim.:  32/32          
c |      9938 |   50497   160280 |      --    9615       --      -- |     --   | -1660/-3067
c |      9938 |   50497   160280 |   20198    9413  1655708   175.9 | 67.941 % |
c |     10038 |   50497   160280 |   22218    9513  1672320   175.8 | 68.577 % |
c |     10188 |   50497   160280 |   24440    9663  1712865   177.3 | 68.577 % |
c |     10413 |   50471   160013 |   26870    9882  1754843   177.6 | 68.652 % |
c |     10751 |   50441   159741 |   29540   10214  1808582   177.1 | 68.745 % |
c |     11257 |   50441   159741 |   32494   10720  1921366   179.2 | 68.746 % |
c |     12016 |   50311   158566 |   35651   11454  2063222   180.1 | 69.131 % |
c |     13156 |   50174   157336 |   39109   12569  2287621   182.0 | 69.542 % |
c |     14865 |   50085   156519 |   42944   14255  2707816   190.0 | 69.810 % |
c |     17427 |   49737   153164 |   46910   16719  3287831   196.7 | 70.868 % |
c |     21271 |   49533   151280 |   51390   20510  4195396   204.6 | 71.496 % |
c |     27037 |   49441   150512 |   56424   26239  5779521   220.3 | 71.783 % |
c |     35686 |   49186   148239 |   61746   34754  8384594   241.3 | 72.561 % |
c |     48662 |   48780   144510 |   67360   47466 12391915   261.1 | 73.768 % |
c ==============================================================================
c (current CPU-time: 235.261 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 |     49135 |   49547   146815 |   14864   47939 12555717   261.9 | 73.768 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4908          
c   -- var.elim.:  2000/4908          
c   -- var.elim.:  3000/4908          
c   -- var.elim.:  4000/4908          
c   -- var.elim.:  4908/4908          
c   -- var.elim.:  1000/1281          
c   -- var.elim.:  1281/1281          
c |     49135 |   48764   142904 |      --   47939       --      -- |     --   | -764/-1013
c |     49135 |   48764   142904 |   19505   36592  4753501   129.9 | 73.768 % |
c |     49235 |   48764   142904 |   21456   14968  1434277    95.8 | 73.900 % |
c |     49387 |   48764   142904 |   23601   15120  1466050    97.0 | 73.900 % |
c |     49612 |   48764   142904 |   25961   15345  1522610    99.2 | 73.900 % |
c |     49949 |   48764   142904 |   28558   15682  1569005   100.1 | 73.900 % |
c |     50455 |   48764   142904 |   31413   16188  1711446   105.7 | 73.900 % |
c |     51214 |   48760   142866 |   34552   16940  1871103   110.5 | 73.913 % |
c |     52353 |   48730   142589 |   37984   18071  2134097   118.1 | 74.000 % |
c |     54061 |   48710   142408 |   41765   19770  2601255   131.6 | 74.062 % |
c |     56623 |   48633   141738 |   45869   22321  3316953   148.6 | 74.286 % |
c |     60467 |   48471   140329 |   50288   26148  4362231   166.8 | 74.779 % |
c |     66233 |   48274   138552 |   55092   31860  6018321   188.9 | 75.371 % |
c |     74882 |   48154   137430 |   60451   40490  8562188   211.5 | 75.726 % |
c |     87856 |   47871   134897 |   66105   53377 12147249   227.6 | 76.580 % |
c |    107317 |   47573   132397 |   72263   72762 18144852   249.4 | 77.496 % |
c |    136509 |   47116   128522 |   78726   38242  8726670   228.2 | 78.848 % |
c |    180298 |   46736   125372 |   85900   81913 21600163   263.7 | 79.958 % |
c |    245982 |   46260   121540 |   93527   71137 18243115   256.5 | 81.379 % |
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 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 C288 -C287 -C286 -C285 -C284 C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 C1#### 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.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (runsolver) R 32391 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480458191 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 4996 0 0 0 978 19 0 0 25 0 1 0 480458191 22384640 4705 4294967295 134512640 134672761 3221224560 3221222156 134566513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4705 603 41 0 5424 0
vsize: 21860
[startup+20.0006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 5020 0 0 0 1978 19 0 0 25 0 1 0 480458191 22548480 4729 4294967295 134512640 134672761 3221224560 3221222224 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5505 4729 603 41 0 5464 0
vsize: 22020
[startup+30.0002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 5041 0 0 0 2978 19 0 0 25 0 1 0 480458191 22548480 4750 4294967295 134512640 134672761 3221224560 3221222388 134566428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5505 4750 603 41 0 5464 0
vsize: 22020
[startup+40.0006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 5047 0 0 0 3977 20 0 0 25 0 1 0 480458191 22548480 4756 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5505 4756 603 41 0 5464 0
vsize: 22020
[startup+50.0004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 5199 0 0 0 4976 20 0 0 25 0 1 0 480458191 23613440 4908 4294967295 134512640 134672761 3221224560 3221223104 134621090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5765 4908 603 41 0 5724 0
vsize: 23060
[startup+60.0013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 6659 0 0 0 5962 35 0 0 25 0 1 0 480458191 27365376 5427 4294967295 134512640 134672761 3221224560 3221222848 134565560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6681 5427 603 41 0 6640 0
vsize: 26724
[startup+70.0013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 6811 0 0 0 6958 38 0 0 25 0 1 0 480458191 28217344 5579 4294967295 134512640 134672761 3221224560 3221223272 134643250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6889 5579 603 41 0 6848 0
vsize: 27556
[startup+80.0012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 6812 0 0 0 7957 38 0 0 25 0 1 0 480458191 27365376 5428 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6681 5428 603 41 0 6640 0
vsize: 26724
[startup+90.0018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 7414 0 0 0 8956 39 0 0 25 0 1 0 480458191 29868032 6030 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7292 6030 603 41 0 7251 0
vsize: 29168
[startup+100.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 9157 0 0 0 9945 50 0 0 25 0 1 0 480458191 32571392 6735 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7952 6735 603 41 0 7911 0
vsize: 31808
[startup+110.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 9547 0 0 0 10943 52 0 0 25 0 1 0 480458191 34156544 7125 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7125 603 41 0 8298 0
vsize: 33356
[startup+120.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 10500 0 0 0 11941 54 0 0 25 0 1 0 480458191 38236160 8078 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9335 8078 603 41 0 9294 0
vsize: 37340
[startup+130.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32392
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 11340 0 0 0 12940 56 0 0 25 0 1 0 480458191 41631744 8918 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 8918 603 41 0 10123 0
vsize: 40656
[startup+140.003 s]
Raw data (loadavg): 1.07 1.00 0.92 2/56 32435
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 12369 0 0 0 13937 58 0 0 25 0 1 0 480458191 45826048 9947 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11188 9947 603 41 0 11147 0
vsize: 44752
[startup+150.033 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 13176 0 0 0 14939 60 0 0 25 0 1 0 480458191 49098752 10754 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11987 10754 603 41 0 11946 0
vsize: 47948
[startup+160.033 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 14264 0 0 0 15937 62 0 0 25 0 1 0 480458191 53530624 11842 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13069 11842 603 41 0 13028 0
vsize: 52276
[startup+170.033 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 15038 0 0 0 16934 65 0 0 25 0 1 0 480458191 56651776 12616 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13831 12616 603 41 0 13790 0
vsize: 55324
[startup+180.033 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 15705 0 0 0 17933 66 0 0 25 0 1 0 480458191 59527168 13283 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14533 13283 603 41 0 14492 0
vsize: 58132
[startup+190.033 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 16331 0 0 0 18931 68 0 0 25 0 1 0 480458191 62152704 13909 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 13909 603 41 0 15133 0
vsize: 60696
[startup+200.032 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 17033 0 0 0 19930 69 0 0 25 0 1 0 480458191 65036288 14611 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15878 14611 603 41 0 15837 0
vsize: 63512
[startup+210.033 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32445
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 17845 0 0 0 20928 72 0 0 25 0 1 0 480458191 68313088 15423 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16678 15423 603 41 0 16637 0
vsize: 66712
[startup+220.032 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 18483 0 0 0 21926 73 0 0 25 0 1 0 480458191 70926336 16061 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17316 16061 603 41 0 17275 0
vsize: 69264
[startup+230.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 19567 0 0 0 22925 75 0 0 25 0 1 0 480458191 75366400 17145 4294967295 134512640 134672761 3221224560 3221223744 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18400 17145 603 41 0 18359 0
vsize: 73600
[startup+240.033 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21671 0 0 0 23916 84 0 0 25 0 1 0 480458191 77590528 17732 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18943 17732 603 41 0 18902 0
vsize: 75772
[startup+250.033 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 24915 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+260.034 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 25916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+270.034 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 26916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+280.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 27916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223760 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+290.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 28916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+300.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 29916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+310.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 30916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+320.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 31916 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+330.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 32917 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+340.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 33917 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+350.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 34917 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223232 134621242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+360.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21740 0 0 0 35917 85 0 0 25 0 1 0 480458191 77828096 17759 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17759 603 41 0 18960 0
vsize: 76004
[startup+370.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21741 0 0 0 36917 85 0 0 25 0 1 0 480458191 77828096 17760 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17760 603 41 0 18960 0
vsize: 76004
[startup+380.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21743 0 0 0 37917 85 0 0 25 0 1 0 480458191 77828096 17762 4294967295 134512640 134672761 3221224560 3221223600 134612692 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17762 603 41 0 18960 0
vsize: 76004
[startup+390.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21745 0 0 0 38917 85 0 0 25 0 1 0 480458191 77828096 17764 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19001 17764 603 41 0 18960 0
vsize: 76004
[startup+400.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 21978 0 0 0 39917 85 0 0 25 0 1 0 480458191 78872576 17997 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19256 17997 603 41 0 19215 0
vsize: 77024
[startup+410.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 22614 0 0 0 40915 87 0 0 25 0 1 0 480458191 81383424 18633 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19869 18633 603 41 0 19828 0
vsize: 79476
[startup+420.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 23317 0 0 0 41914 89 0 0 25 0 1 0 480458191 84344832 19336 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 19336 603 41 0 20551 0
vsize: 82368
[startup+430.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 24155 0 0 0 42912 91 0 0 25 0 1 0 480458191 87744512 20174 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21422 20174 603 41 0 21381 0
vsize: 85688
[startup+440.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 24710 0 0 0 43910 93 0 0 25 0 1 0 480458191 89985024 20729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21969 20729 603 41 0 21928 0
vsize: 87876
[startup+450.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 25318 0 0 0 44909 94 0 0 25 0 1 0 480458191 92479488 21337 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22578 21337 603 41 0 22537 0
vsize: 90312
[startup+460.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 25710 0 0 0 45908 95 0 0 25 0 1 0 480458191 94334976 21729 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23031 21729 603 41 0 22990 0
vsize: 92124
[startup+470.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 26351 0 0 0 46907 97 0 0 25 0 1 0 480458191 96956416 22370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23671 22370 603 41 0 23630 0
vsize: 94684
[startup+480.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32447
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 26691 0 0 0 47906 98 0 0 25 0 1 0 480458191 98398208 22710 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24023 22710 603 41 0 23982 0
vsize: 96092
[startup+490.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 27340 0 0 0 48905 99 0 0 25 0 1 0 480458191 100995072 23359 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24657 23359 603 41 0 24616 0
vsize: 98628
[startup+500.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 27783 0 0 0 49904 100 0 0 25 0 1 0 480458191 102817792 23802 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25102 23802 603 41 0 25061 0
vsize: 100408
[startup+510.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 28205 0 0 0 50904 101 0 0 25 0 1 0 480458191 104497152 24224 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25512 24224 603 41 0 25471 0
vsize: 102048
[startup+520.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 28685 0 0 0 51903 102 0 0 25 0 1 0 480458191 106446848 24704 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25988 24704 603 41 0 25947 0
vsize: 103952
[startup+530.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 29122 0 0 0 52901 104 0 0 25 0 1 0 480458191 108310528 25141 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26443 25141 603 41 0 26402 0
vsize: 105772
[startup+540.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 29566 0 0 0 53900 105 0 0 25 0 1 0 480458191 110104576 25585 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26881 25585 603 41 0 26840 0
vsize: 107524
[startup+550.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 30045 0 0 0 54898 107 0 0 25 0 1 0 480458191 112070656 26064 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27361 26064 603 41 0 27320 0
vsize: 109444
[startup+560.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 30672 0 0 0 55897 109 0 0 25 0 1 0 480458191 114634752 26691 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27987 26691 603 41 0 27946 0
vsize: 111948
[startup+570.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 31219 0 0 0 56895 111 0 0 25 0 1 0 480458191 116883456 27238 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28536 27238 603 41 0 28495 0
vsize: 114144
[startup+580.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 31966 0 0 0 57894 112 0 0 25 0 1 0 480458191 119857152 27985 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29262 27985 603 41 0 29221 0
vsize: 117048
[startup+590.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 58894 112 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+600.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 59894 112 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+610.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 60894 112 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+620.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 61894 112 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+630.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 62895 112 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+640.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 63895 112 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+650.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 64894 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+660.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 65894 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+670.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 66895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+680.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 67895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223696 134614688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+690.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 68895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223552 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+700.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 69895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+710.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 70895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+720.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 71895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+730.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 72895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+740.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32170 0 0 0 73895 113 0 0 25 0 1 0 480458191 120213504 28105 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28105 603 41 0 29308 0
vsize: 117396
[startup+750.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 74896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+760.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 75896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+770.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 76896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+780.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 77896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+790.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 78896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223704 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+800.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 79896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+810.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 80896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223592 134603663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+820.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 81896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223712 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 82896 113 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+840.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 83897 114 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+850.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 84897 114 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+860.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 85897 114 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+870.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32171 0 0 0 86897 114 0 0 25 0 1 0 480458191 120213504 28106 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28106 603 41 0 29308 0
vsize: 117396
[startup+880.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32384 0 0 0 87897 114 0 0 25 0 1 0 480458191 121110528 28319 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29568 28319 603 41 0 29527 0
vsize: 118272
[startup+890.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 32842 0 0 0 88895 116 0 0 25 0 1 0 480458191 123076608 28777 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30048 28777 603 41 0 30007 0
vsize: 120192
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 33433 0 0 0 89894 117 0 0 25 0 1 0 480458191 125419520 29368 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30620 29368 603 41 0 30579 0
vsize: 122480
[startup+910.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 33902 0 0 0 90893 118 0 0 25 0 1 0 480458191 127377408 29837 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31098 29837 603 41 0 31057 0
vsize: 124392
[startup+920.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 34378 0 0 0 91891 120 0 0 25 0 1 0 480458191 129302528 30313 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31568 30313 603 41 0 31527 0
vsize: 126272
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 34691 0 0 0 92891 121 0 0 25 0 1 0 480458191 130617344 30626 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31889 30626 603 41 0 31848 0
vsize: 127556
[startup+940.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 35090 0 0 0 93890 122 0 0 25 0 1 0 480458191 132182016 31025 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32271 31025 603 41 0 32230 0
vsize: 129084
[startup+950.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 35591 0 0 0 94889 123 0 0 25 0 1 0 480458191 134266880 31526 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32780 31526 603 41 0 32739 0
vsize: 131120
[startup+960.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 36063 0 0 0 95888 125 0 0 25 0 1 0 480458191 136237056 31998 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33261 31998 603 41 0 33220 0
vsize: 133044
[startup+970.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 36230 0 0 0 96887 125 0 0 25 0 1 0 480458191 136884224 32165 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33419 32165 603 41 0 33378 0
vsize: 133676
[startup+980.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 36618 0 0 0 97886 127 0 0 25 0 1 0 480458191 138461184 32553 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33804 32553 603 41 0 33763 0
vsize: 135216
[startup+990.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37048 0 0 0 98885 128 0 0 25 0 1 0 480458191 140283904 32983 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34249 32983 603 41 0 34208 0
vsize: 136996
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 99885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 100885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 101885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 102885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 103885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 104885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 105885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 106885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 107885 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 108886 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 109886 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 110886 129 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 111886 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 112886 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 113886 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 114886 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 115886 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 116887 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 117887 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 118887 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32449
Raw data (stat): 32392 (minisat+) R 32391 28099 28098 0 -1 0 37216 0 0 0 119887 130 0 0 25 0 1 0 480458191 140668928 33053 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34343 33053 603 41 0 34302 0
vsize: 137372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 32449
Raw data (stat): 32392 (minisat+) Z 32391 28099 28098 0 -1 12 37217 0 0 0 119887 137 0 0 25 0 1 0 480458191 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.26
CPU user time (s): 1198.88
CPU system time (s): 1.37979
CPU usage (%): 100.012
Max. virtual memory (Kb): 137372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####