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-3.opb
MD5SUM	3acd642471b3f4559739eef7eb2e9b58
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
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	41095
Number of constraints which are clauses	41095
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 5617

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        852304 kB
Buffers:         32164 kB
Cached:         106712 kB
SwapCached:        524 kB
Active:          49384 kB
Inactive:        92900 kB
HighTotal:      131008 kB
HighFree:        20552 kB
LowTotal:       903652 kB
LowFree:        831752 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34616 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:17:48 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4086 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41095 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 |   41095    82190 |   12328       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   41095    82190 |   16438       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.73774 s)
c ==============================================================================
c [1mFound solution: -31[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 |   77395   167462 |   23218       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24844          
c   -- var.elim.:  2000/24844          
c   -- var.elim.:  3000/24844          
c   -- var.elim.:  4000/24844          
c   -- var.elim.:  5000/24844          
c   -- var.elim.:  6000/24844          
c   -- var.elim.:  7000/24844          
c   -- var.elim.:  8000/24844          
c   -- var.elim.:  9000/24844          
c   -- var.elim.:  10000/24844          
c   -- var.elim.:  11000/24844          
c   -- var.elim.:  12000/24844          
c   -- var.elim.:  13000/24844          
c   -- var.elim.:  14000/24844          
c   -- var.elim.:  15000/24844          
c   -- var.elim.:  16000/24844          
c   -- var.elim.:  17000/24844          
c   -- var.elim.:  18000/24844          
c   -- var.elim.:  19000/24844          
c   -- var.elim.:  20000/24844          
c   -- var.elim.:  21000/24844          
c   -- var.elim.:  22000/24844          
c   -- var.elim.:  23000/24844          
c   -- var.elim.:  24000/24844          
c   -- var.elim.:  24844/24844          
c   -- var.elim.:  1000/12626          
c   -- var.elim.:  2000/12626          
c   -- var.elim.:  3000/12626          
c   -- var.elim.:  4000/12626          
c   -- var.elim.:  5000/12626          
c   -- var.elim.:  6000/12626          
c   -- var.elim.:  7000/12626          
c   -- var.elim.:  8000/12626          
c   -- var.elim.:  9000/12626          
c   -- var.elim.:  10000/12626          
c   -- var.elim.:  11000/12626          
c   -- var.elim.:  12000/12626          
c   -- var.elim.:  12626/12626          
c   -- var.elim.:  1000/2962          
c   -- var.elim.:  2000/2962          
c   -- var.elim.:  2962/2962          
c   -- var.elim.:  50/50          
c   -- var.elim.:  21/21          
c   -- subsuming                       
c   -- var.elim.:  1000/5765          
c   -- var.elim.:  2000/5765          
c   -- var.elim.:  3000/5765          
c   -- var.elim.:  4000/5765          
c   -- var.elim.:  5000/5765          
c   -- var.elim.:  5765/5765          
c   -- var.elim.:  686/686          
c |         0 |   51743   168583 |      --       0       --      -- |     --   | -25652/1122
c |         0 |   51743   168583 |   20697       0        0     nan |  0.000 % |
c |       100 |   51743   168583 |   22766     100    19093   190.9 | 52.865 % |
c |       250 |   51723   168040 |   25033     248    48782   196.7 | 52.936 % |
c |       475 |   51723   168040 |   27537     473    86345   182.5 | 52.936 % |
c |       812 |   51723   168040 |   30291     810   147493   182.1 | 52.936 % |
c |      1318 |   51695   167782 |   33302    1314   219989   167.4 | 53.040 % |
c |      2078 |   51581   166823 |   36551    2066   341255   165.2 | 53.446 % |
c |      3217 |   51581   166823 |   40206    3205   602863   188.1 | 53.446 % |
c |      4925 |   51431   165490 |   44098    4899   976976   199.4 | 54.004 % |
c |      7487 |   51330   164601 |   48413    7449  1587998   213.2 | 54.370 % |
c |     11332 |   50968   161720 |   52879   11233  2474385   220.3 | 55.613 % |
c |     17098 |   50512   157849 |   57646   16881  4070367   241.1 | 57.430 % |
c ==============================================================================
c (current CPU-time: 98.87 s)
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17418 |   52425   162689 |   15727   17194  4240180   246.6 | 57.430 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7069          
c   -- var.elim.:  2000/7069          
c   -- var.elim.:  3000/7069          
c   -- var.elim.:  4000/7069          
c   -- var.elim.:  5000/7069          
c   -- var.elim.:  6000/7069          
c   -- var.elim.:  7000/7069          
c   -- var.elim.:  7069/7069          
c   -- var.elim.:  1000/1530          
c   -- var.elim.:  1530/1530          
c   -- var.elim.:  4/4          
c |     17418 |   50449   157209 |      --   17194       --      -- |     --   | -1966/-1715
c |     17418 |   50449   157209 |   20179   17194  4240180   246.6 | 57.430 % |
c |     17518 |   50449   157209 |   22197   17294  4268368   246.8 | 63.002 % |
c |     17669 |   50449   157209 |   24417   17445  4310181   247.1 | 63.002 % |
c |     17894 |   50449   157209 |   26859   17670  4380041   247.9 | 63.001 % |
c |     18231 |   50449   157209 |   29544   18007  4472859   248.4 | 63.002 % |
c |     18737 |   50353   156386 |   32437   15095  1758843   116.5 | 63.337 % |
c |     19496 |   50317   156048 |   35655   15846  1948739   123.0 | 63.455 % |
c |     20635 |   50317   156048 |   39221   16985  2339583   137.7 | 63.455 % |
c |     22344 |   50241   155318 |   43078   18672  2822869   151.2 | 63.720 % |
c |     24906 |   50211   155028 |   47357   21206  3686024   173.8 | 63.825 % |
c |     28750 |   50155   154479 |   52035   25040  5161400   206.1 | 64.021 % |
c |     34516 |   50012   153185 |   57076   30747  7157687   232.8 | 64.508 % |
c |     43165 |   49763   151012 |   62471   39353 10196132   259.1 | 65.353 % |
c |     56140 |   49385   147353 |   68196   52164 15219381   291.8 | 66.629 % |
c |     75603 |   48867   142967 |   74228   71398 23110390   323.7 | 68.416 % |
c ==============================================================================
c (current CPU-time: 490.477 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 |     87780 |   50343   146567 |   15102   83543 28238188   338.0 | 68.416 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5936          
c   -- var.elim.:  2000/5936          
c   -- var.elim.:  3000/5936          
c   -- var.elim.:  4000/5936          
c   -- var.elim.:  5000/5936          
c   -- var.elim.:  5936/5936          
c   -- var.elim.:  1000/1491          
c   -- var.elim.:  1491/1491          
c |     87780 |   48790   143358 |      --   83543       --      -- |     --   | -1547/-2855
c |     87780 |   48790   143358 |   19516   67676 12276485   181.4 | 68.416 % |
c |     87881 |   48730   142855 |   21441   18329  2417043   131.9 | 71.231 % |
c |     88031 |   48730   142855 |   23585   18479  2450861   132.6 | 71.230 % |
c |     88256 |   48730   142855 |   25943   18704  2509697   134.2 | 71.231 % |
c |     88594 |   48730   142855 |   28538   19042  2613295   137.2 | 71.231 % |
c |     89100 |   48728   142838 |   31390   19544  2749283   140.7 | 71.237 % |
c |     89859 |   48728   142838 |   34529   20303  2956198   145.6 | 71.237 % |
c |     90998 |   48676   142457 |   37942   21434  3264118   152.3 | 71.406 % |
c |     92706 |   48650   142222 |   41714   23132  3671591   158.7 | 71.490 % |
c |     95268 |   48588   141702 |   45827   25688  4560560   177.5 | 71.691 % |
c |     99112 |   48554   141413 |   50374   29508  5867298   198.8 | 71.801 % |
c |    104878 |   48448   140532 |   55291   35258  7742606   219.6 | 72.138 % |
c |    113529 |   48352   139752 |   60699   43890 10745333   244.8 | 72.449 % |
c |    126503 |   47924   136245 |   66178   56789 14764942   260.0 | 73.804 % |
c |    145966 |   47612   133570 |   72322   76043 21826512   287.0 | 74.796 % |
c |    175158 |   47340   131304 |   79100   41492 11142911   268.6 | 75.658 % |
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 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 30639
Raw data (stat): 30639 (runsolver) R 30638 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480446407 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99963 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5015 0 0 0 980 18 0 0 25 0 1 0 480446407 22413312 4725 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5472 4725 603 41 0 5431 0
vsize: 21888
[startup+20 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5032 0 0 0 1980 18 0 0 25 0 1 0 480446407 22597632 4742 4294967295 134512640 134672761 3221224560 3221222928 134603527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5517 4742 603 41 0 5476 0
vsize: 22068
[startup+29.9997 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5037 0 0 0 2980 18 0 0 25 0 1 0 480446407 22597632 4747 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5517 4747 603 41 0 5476 0
vsize: 22068
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5058 0 0 0 3980 19 0 0 25 0 1 0 480446407 22597632 4768 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5517 4768 603 41 0 5476 0
vsize: 22068
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5210 0 0 0 4980 19 0 0 25 0 1 0 480446407 23654400 4920 4294967295 134512640 134672761 3221224560 3221223024 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5775 4920 603 41 0 5734 0
vsize: 23100
[startup+60.0009 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5325 0 0 0 5979 19 0 0 25 0 1 0 480446407 23121920 4883 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5645 4883 603 41 0 5604 0
vsize: 22580
[startup+70.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 6537 0 0 0 6977 22 0 0 25 0 1 0 480446407 27975680 6095 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6095 603 41 0 6789 0
vsize: 27320
[startup+80.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 7466 0 0 0 7975 25 0 0 25 0 1 0 480446407 31780864 7024 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7759 7024 603 41 0 7718 0
vsize: 31036
[startup+90.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 8297 0 0 0 8973 27 0 0 25 0 1 0 480446407 35209216 7855 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8596 7855 603 41 0 8555 0
vsize: 34384
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10250 0 0 0 9966 33 0 0 25 0 1 0 480446407 41537536 9317 4294967295 134512640 134672761 3221224560 3221223104 134621041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9317 603 41 0 10100 0
vsize: 40564
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10278 0 0 0 10960 38 0 0 25 0 1 0 480446407 40476672 9193 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 9193 603 41 0 9841 0
vsize: 39528
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10280 0 0 0 11961 38 0 0 25 0 1 0 480446407 40476672 9195 4294967295 134512640 134672761 3221224560 3221223600 134612646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 9195 603 41 0 9841 0
vsize: 39528
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10283 0 0 0 12961 38 0 0 25 0 1 0 480446407 40476672 9198 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 9198 603 41 0 9841 0
vsize: 39528
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 3/57 30680
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 11504 0 0 0 13958 40 0 0 25 0 1 0 480446407 45428736 10419 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11091 10419 603 41 0 11050 0
vsize: 44364
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 12521 0 0 0 14949 50 0 0 25 0 1 0 480446407 49688576 11436 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12131 11436 603 41 0 12090 0
vsize: 48524
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 13253 0 0 0 15947 52 0 0 25 0 1 0 480446407 52613120 12168 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12845 12168 603 41 0 12804 0
vsize: 51380
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 14131 0 0 0 16945 54 0 0 25 0 1 0 480446407 56381440 13046 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13765 13046 603 41 0 13724 0
vsize: 55060
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 14934 0 0 0 17943 56 0 0 25 0 1 0 480446407 59645952 13849 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14562 13849 603 41 0 14521 0
vsize: 58248
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 15686 0 0 0 18942 57 0 0 25 0 1 0 480446407 62672896 14601 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15301 14601 603 41 0 15260 0
vsize: 61204
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 16386 0 0 0 19941 58 0 0 25 0 1 0 480446407 65515520 15301 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15995 15301 603 41 0 15954 0
vsize: 63980
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 17140 0 0 0 20939 61 0 0 25 0 1 0 480446407 68620288 16055 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 16056 603 41 0 16712 0
vsize: 67012
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 18094 0 0 0 21936 64 0 0 25 0 1 0 480446407 72499200 17009 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17700 17009 603 41 0 17659 0
vsize: 70800
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 19070 0 0 0 22935 66 0 0 25 0 1 0 480446407 76496896 17985 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18676 17985 603 41 0 18635 0
vsize: 74704
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 19487 0 0 0 23934 66 0 0 25 0 1 0 480446407 78180352 18402 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19087 18402 603 41 0 19046 0
vsize: 76348
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 20215 0 0 0 24933 68 0 0 25 0 1 0 480446407 81215488 19130 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19828 19130 603 41 0 19787 0
vsize: 79312
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 20684 0 0 0 25932 69 0 0 25 0 1 0 480446407 83058688 19599 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19599 603 41 0 20237 0
vsize: 81112
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 21342 0 0 0 26930 71 0 0 25 0 1 0 480446407 85774336 20257 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20941 20257 603 41 0 20900 0
vsize: 83764
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 22150 0 0 0 27928 73 0 0 25 0 1 0 480446407 89133056 21065 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21761 21065 603 41 0 21720 0
vsize: 87044
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 22779 0 0 0 28928 73 0 0 25 0 1 0 480446407 91619328 21694 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 21694 603 41 0 22327 0
vsize: 89472
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 23558 0 0 0 29926 76 0 0 25 0 1 0 480446407 94842880 22473 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23155 22473 603 41 0 23114 0
vsize: 92620
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 24123 0 0 0 30924 77 0 0 25 0 1 0 480446407 97185792 23038 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23727 23038 603 41 0 23686 0
vsize: 94908
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 24680 0 0 0 31923 79 0 0 25 0 1 0 480446407 99409920 23595 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24270 23595 603 41 0 24229 0
vsize: 97080
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 25207 0 0 0 32922 80 0 0 25 0 1 0 480446407 101629952 24122 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24812 24122 603 41 0 24771 0
vsize: 99248
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 25883 0 0 0 33921 81 0 0 25 0 1 0 480446407 104386560 24798 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25485 24798 603 41 0 25444 0
vsize: 101940
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 26519 0 0 0 34920 83 0 0 25 0 1 0 480446407 106987520 25434 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26120 25434 603 41 0 26079 0
vsize: 104480
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 27182 0 0 0 35917 86 0 0 25 0 1 0 480446407 109940736 26097 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26841 26097 603 41 0 26800 0
vsize: 107364
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 27701 0 0 0 36916 87 0 0 25 0 1 0 480446407 112087040 26616 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27365 26616 603 41 0 27324 0
vsize: 109460
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 28215 0 0 0 37915 88 0 0 25 0 1 0 480446407 114151424 27130 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27869 27130 603 41 0 27828 0
vsize: 111476
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 28784 0 0 0 38914 89 0 0 25 0 1 0 480446407 116514816 27699 4294967295 134512640 134672761 3221224560 3221223760 134610511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28446 27699 603 41 0 28405 0
vsize: 113784
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 29056 0 0 0 39913 91 0 0 25 0 1 0 480446407 117579776 27971 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28706 27971 603 41 0 28665 0
vsize: 114824
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 29632 0 0 0 40912 92 0 0 25 0 1 0 480446407 119930880 28547 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29280 28547 603 41 0 29239 0
vsize: 117120
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 30221 0 0 0 41911 93 0 0 25 0 1 0 480446407 122294272 29136 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29857 29136 603 41 0 29816 0
vsize: 119428
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 30807 0 0 0 42909 95 0 0 25 0 1 0 480446407 124796928 29722 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30468 29722 603 41 0 30427 0
vsize: 121872
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 31500 0 0 0 43908 96 0 0 25 0 1 0 480446407 127647744 30415 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31164 30415 603 41 0 31123 0
vsize: 124656
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 32438 0 0 0 44906 98 0 0 25 0 1 0 480446407 131424256 31353 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32086 31353 603 41 0 32045 0
vsize: 128344
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 33220 0 0 0 45905 100 0 0 25 0 1 0 480446407 134664192 32135 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32877 32135 603 41 0 32836 0
vsize: 131508
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 33842 0 0 0 46904 101 0 0 25 0 1 0 480446407 137228288 32757 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33503 32757 603 41 0 33462 0
vsize: 134012
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 34116 0 0 0 47903 102 0 0 25 0 1 0 480446407 138264576 33031 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33756 33031 603 41 0 33715 0
vsize: 135024
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 34511 0 0 0 48903 102 0 0 25 0 1 0 480446407 139948032 33426 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34167 33426 603 41 0 34126 0
vsize: 136668
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 49896 109 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 50896 109 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 51896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 52896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 53896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 54896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 55896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 56897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 57897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 58897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 59897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 60897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 61897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 62898 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34081 603 41 0 34752 0
vsize: 139172
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 63898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 64898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 65898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 66898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 67898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 68898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 69898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 70898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 71898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 72899 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34082 603 41 0 34752 0
vsize: 139172
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 73899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 74899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 75899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 76899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 77899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 78899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 79900 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34083 603 41 0 34752 0
vsize: 139172
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 80900 111 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34084 603 41 0 34752 0
vsize: 139172
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 81900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34084 603 41 0 34752 0
vsize: 139172
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 82900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34084 603 41 0 34752 0
vsize: 139172
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 83900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34084 603 41 0 34752 0
vsize: 139172
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 84900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34084 603 41 0 34752 0
vsize: 139172
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 85900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 86900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 87900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 88900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223552 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 89901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 90901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 91901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 92901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 93901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223552 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 94901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 95901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 96901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 97901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 98901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 99902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 100902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 101902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 102902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 103902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 104902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 105903 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 106903 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34086 603 41 0 34752 0
vsize: 139172
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 107903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 108903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 109903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 110903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 111903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 112903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 113903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 114903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 115903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 116904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 117904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 118904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 119904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34793 34087 603 41 0 34752 0
vsize: 139172
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30696
Raw data (stat): 30639 (minisat+) Z 30638 26298 26297 0 -1 12 35649 0 0 0 119904 121 0 0 25 0 1 0 480446407 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.1
CPU time (s): 1200.26
CPU user time (s): 1199.05
CPU system time (s): 1.21681
CPU usage (%): 100.014
Max. virtual memory (Kb): 139172
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####