PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        842836 kB
Buffers:         41136 kB
Cached:         126280 kB
SwapCached:          0 kB
Active:         111664 kB
Inactive:        58864 kB
HighTotal:      131008 kB
HighFree:        12040 kB
LowTotal:       903652 kB
LowFree:        830796 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15724 kB
Committed_AS:    92784 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:11:32 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4461 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41263 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41263    82526 |   13754       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77411   167438 |   25803       0        0     nan |  0.000 % |
c |       100 |   77197   167004 |   28383      85     1743    20.5 |  0.449 % |
c |       250 |   76777   166128 |   31221     216     3076    14.2 |  1.370 % |
c |       475 |   75681   163748 |   34343     367     7270    19.8 |  3.965 % |
c |       812 |   74772   161767 |   37778     638    10625    16.7 |  6.213 % |
c |      1318 |   72216   156098 |   41555     971    15210    15.7 | 12.362 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1358 |   71957   155524 |   23985    1000    15644    15.6 | 12.362 % |
c |      1458 |   71484   154445 |   26383    1077    16216    15.1 | 14.235 % |
c |      1609 |   70637   152550 |   29021    1185    17694    14.9 | 16.491 % |
c |      1834 |   69903   150904 |   31924    1355    19103    14.1 | 18.302 % |
c |      2171 |   68629   148052 |   35116    1633    21862    13.4 | 21.386 % |
c |      2677 |   66555   143323 |   38628    2003    25849    12.9 | 26.681 % |
c |      3436 |   63907   137250 |   42490    2573    35121    13.6 | 33.519 % |
c |      4575 |   60641   129717 |   46739    3414    45806    13.4 | 42.032 % |
c |      6284 |   58132   123765 |   51413    4758    70644    14.8 | 48.684 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6893 |   57499   122346 |   19166    5251    79403    15.1 | 48.684 % |
c |      6993 |   57374   122059 |   21082    5340    80419    15.1 | 50.986 % |
c |      7143 |   57174   121601 |   23190    5476    83135    15.2 | 51.497 % |
c |      7368 |   57124   121493 |   25509    5691    90616    15.9 | 51.614 % |
c |      7705 |   56450   119888 |   28060    5895    93895    15.9 | 53.460 % |
c |      8211 |   55724   118204 |   30867    6317   101819    16.1 | 55.371 % |
c |      8970 |   54430   115147 |   33953    6865   120056    17.5 | 58.891 % |
c |     10109 |   53229   112295 |   37349    7784   156050    20.0 | 62.178 % |
c |     11817 |   51998   109354 |   41084    9200   202992    22.1 | 65.558 % |
c |     14379 |   50235   105114 |   45192   10981   295829    26.9 | 70.406 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15965 |   49478   103359 |   16492   12311   371372    30.2 | 70.406 % |
c |     16066 |   49478   103359 |   18141   12412   374678    30.2 | 72.440 % |
c |     16216 |   49424   103225 |   19955   12525   376566    30.1 | 72.597 % |
c |     16441 |   49285   102876 |   21950   12651   381138    30.1 | 72.991 % |
c |     16778 |   49212   102697 |   24145   12924   395334    30.6 | 73.204 % |
c |     17285 |   49156   102561 |   26560   13400   438885    32.8 | 73.360 % |
c |     18044 |   48324   100548 |   29216   13832   461348    33.4 | 75.707 % |
c |     19183 |   48201   100261 |   32138   14905   550058    36.9 | 76.033 % |
c |     20891 |   47874    99472 |   35352   16285   636889    39.1 | 76.957 % |
c |     23453 |   47628    98870 |   38887   18649   839926    45.0 | 77.656 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25038 |   47524    98566 |   15841   20184   980752    48.6 | 77.656 % |
c |     25139 |   47524    98566 |   17425   20285   983661    48.5 | 77.940 % |
c |     25289 |   47524    98566 |   19167   20435   990976    48.5 | 77.939 % |
c |     25514 |   47524    98566 |   21084   20660  1005617    48.7 | 77.939 % |
c |     25851 |   47524    98566 |   23192   20997  1026282    48.9 | 77.939 % |
c |     26358 |   47524    98566 |   25512   21504  1055909    49.1 | 77.940 % |
c |     27118 |   47524    98566 |   28063   22264  1120991    50.3 | 77.939 % |
c |     28258 |   47202    97772 |   30869   23237  1219781    52.5 | 78.852 % |
c |     29966 |   47191    97747 |   33956   24941  1366171    54.8 | 78.880 % |
c |     32528 |   47072    97453 |   37352   27423  1611937    58.8 | 79.221 % |
c |     36372 |   47072    97453 |   41087   31267  2099445    67.1 | 79.221 % |
c |     42138 |   46746    96661 |   45196   36763  2600401    70.7 | 80.142 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46022 |   46748    96684 |   15582   40621  3011087    74.1 | 80.142 % |
c |     46122 |   46748    96684 |   17140   18203  1211729    66.6 | 80.221 % |
c |     46272 |   46748    96684 |   18854   18353  1218705    66.4 | 80.221 % |
c |     46497 |   46714    96607 |   20739   18539  1230555    66.4 | 80.297 % |
c |     46834 |   46703    96582 |   22813   18867  1250274    66.3 | 80.325 % |
c |     47340 |   46651    96453 |   25094   19368  1284175    66.3 | 80.473 % |
c |     48100 |   46472    96017 |   27604   20063  1320976    65.8 | 80.974 % |
c |     49239 |   46437    95936 |   30364   21181  1424831    67.3 | 81.066 % |
c |     50947 |   46434    95929 |   33401   22886  1532403    67.0 | 81.074 % |
c |     53509 |   46389    95814 |   36741   25444  1762687    69.3 | 81.214 % |
c |     57353 |   46351    95720 |   40415   29177  2121672    72.7 | 81.326 % |
c |     63119 |   46102    95119 |   44457   34489  2610152    75.7 | 82.030 % |
c |     71769 |   46087    95084 |   48902   43071  3470985    80.6 | 82.070 % |
c |     84743 |   46022    94925 |   53793   55928  4763761    85.2 | 82.259 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91656 |   46006    94872 |   15335   62707  5469040    87.2 | 82.259 % |
c |     91756 |   46006    94872 |   16868   20099  1258236    62.6 | 82.312 % |
c |     91906 |   46004    94868 |   18555   20247  1269896    62.7 | 82.316 % |
c |     92131 |   45981    94815 |   20410   20467  1286191    62.8 | 82.376 % |
c |     92469 |   45978    94808 |   22451   20801  1325256    63.7 | 82.384 % |
c |     92975 |   45956    94754 |   24697   21154  1350045    63.8 | 82.448 % |
c |     93735 |   45891    94586 |   27166   21886  1408143    64.3 | 82.640 % |
c |     94874 |   45891    94586 |   29883   23025  1506974    65.4 | 82.640 % |
c |     96582 |   45850    94484 |   32871   24718  1656829    67.0 | 82.756 % |
c |     99144 |   45850    94484 |   36159   27280  1890855    69.3 | 82.756 % |
c |    102988 |   45767    94285 |   39775   31063  2199681    70.8 | 82.989 % |
c |    108754 |   45767    94285 |   43752   36829  2758646    74.9 | 82.988 % |
c |    117404 |   45755    94257 |   48127   45475  3584527    78.8 | 83.021 % |
c |    130378 |   45713    94155 |   52940   58391  4806838    82.3 | 83.141 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136420 |   45733    94207 |   15244   64433  5331404    82.7 | 83.141 % |
c |    136520 |   45733    94207 |   16768   20826  1132496    54.4 | 83.107 % |
c |    136670 |   45733    94207 |   18445   20976  1139985    54.3 | 83.107 % |
c |    136895 |   45733    94207 |   20289   21201  1153537    54.4 | 83.107 % |
c |    137232 |   45733    94207 |   22318   21538  1169510    54.3 | 83.107 % |
c |    137738 |   45733    94207 |   24550   22044  1213136    55.0 | 83.107 % |
c |    138497 |   45733    94207 |   27005   22803  1266674    55.5 | 83.108 % |
c |    139636 |   45733    94207 |   29706   23942  1351252    56.4 | 83.107 % |
c |    141344 |   45733    94207 |   32676   25650  1504180    58.6 | 83.107 % |
c |    143906 |   45733    94207 |   35944   28212  1667932    59.1 | 83.107 % |
c |    147751 |   45733    94207 |   39539   32057  2014186    62.8 | 83.107 % |
c |    153517 |   45733    94207 |   43492   37823  2552526    67.5 | 83.107 % |
c |    162166 |   45681    94069 |   47842   46460  3249653    69.9 | 83.271 % |
c |    175140 |   45681    94069 |   52626   59434  4360949    73.4 | 83.271 % |
c |    194601 |   45651    93995 |   57889   24662  1331831    54.0 | 83.359 % |
c |    223793 |   45636    93958 |   63677   53847  4465405    82.9 | 83.403 % |
c |    267582 |   45636    93958 |   70045   31596  1238437    39.2 | 83.403 % |
c |    333266 |   45616    93912 |   77050   24572   866247    35.3 | 83.455 % |
c |    431792 |   45563    93787 |   84755   42419  1615243    38.1 | 83.599 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 C631 -C630 -C629 -C628 -C627 C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 C480 -C479 -C478 -C477 -C476 C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 C231 -C230 -C229 -C228 C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C7#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/56 21051
Raw data (stat): 21051 (runsolver) R 21050 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 366054611 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 2903 0 0 0 991 8 0 0 25 0 1 0 366054611 14454784 2881 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 2881 603 41 0 3488 0
vsize: 14116
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 2903 0 0 0 1991 8 0 0 25 0 1 0 366054611 14454784 2881 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 2881 603 41 0 3488 0
vsize: 14116
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 2995 0 0 0 2991 8 0 0 25 0 1 0 366054611 14848000 2973 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3625 2973 603 41 0 3584 0
vsize: 14500
[startup+40.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 3245 0 0 0 3990 9 0 0 25 0 1 0 366054611 15859712 3223 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3872 3223 603 41 0 3831 0
vsize: 15488
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 3692 0 0 0 4989 10 0 0 25 0 1 0 366054611 17883136 3670 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3670 603 41 0 4325 0
vsize: 17464
[startup+60.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 4316 0 0 0 5988 12 0 0 25 0 1 0 366054611 20398080 4294 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4294 603 41 0 4939 0
vsize: 19920
[startup+70.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 4978 0 0 0 6986 14 0 0 25 0 1 0 366054611 23089152 4956 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5637 4956 603 41 0 5596 0
vsize: 22548
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 5439 0 0 0 7984 16 0 0 25 0 1 0 366054611 25088000 5417 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6125 5417 603 41 0 6084 0
vsize: 24500
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 5932 0 0 0 8983 17 0 0 25 0 1 0 366054611 27086848 5910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6613 5910 603 41 0 6572 0
vsize: 26452
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 6191 0 0 0 9982 18 0 0 25 0 1 0 366054611 28106752 6169 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6862 6169 603 41 0 6821 0
vsize: 27448
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 6191 0 0 0 10982 18 0 0 25 0 1 0 366054611 28106752 6169 4294967295 134512640 134672761 3221224560 3221223744 134559397 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6862 6169 603 41 0 6821 0
vsize: 27448
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 6191 0 0 0 11981 18 0 0 25 0 1 0 366054611 28106752 6169 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6862 6169 603 41 0 6821 0
vsize: 27448
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 6191 0 0 0 12981 19 0 0 25 0 1 0 366054611 28106752 6169 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6862 6169 603 41 0 6821 0
vsize: 27448
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 6455 0 0 0 13980 20 0 0 25 0 1 0 366054611 29175808 6433 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7123 6433 603 41 0 7082 0
vsize: 28492
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 6953 0 0 0 14979 21 0 0 25 0 1 0 366054611 31182848 6931 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 6931 603 41 0 7572 0
vsize: 30452
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 7341 0 0 0 15978 22 0 0 25 0 1 0 366054611 32772096 7319 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8001 7319 603 41 0 7960 0
vsize: 32004
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 7712 0 0 0 16978 23 0 0 25 0 1 0 366054611 34230272 7690 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8357 7690 603 41 0 8316 0
vsize: 33428
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8064 0 0 0 17977 23 0 0 25 0 1 0 366054611 35700736 8042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8716 8042 603 41 0 8675 0
vsize: 34864
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8423 0 0 0 18976 25 0 0 25 0 1 0 366054611 37167104 8401 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8401 603 41 0 9033 0
vsize: 36296
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8865 0 0 0 19975 26 0 0 25 0 1 0 366054611 38912000 8843 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9500 8843 603 41 0 9459 0
vsize: 38000
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 20975 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 21975 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 22975 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 23976 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 24976 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 25976 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 26976 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21051
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 27976 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 28976 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8933 0 0 0 29977 26 0 0 25 0 1 0 366054611 39178240 8911 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8911 603 41 0 9524 0
vsize: 38260
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 30977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 31977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 32977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 33977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 34977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 35977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 36977 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 37978 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 38978 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 39978 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8934 0 0 0 40978 26 0 0 25 0 1 0 366054611 39178240 8912 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9565 8912 603 41 0 9524 0
vsize: 38260
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8937 0 0 0 41978 26 0 0 25 0 1 0 366054611 39440384 8915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9629 8915 603 41 0 9588 0
vsize: 38516
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 8964 0 0 0 42979 26 0 0 25 0 1 0 366054611 39571456 8942 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9661 8942 603 41 0 9620 0
vsize: 38644
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9196 0 0 0 43978 27 0 0 25 0 1 0 366054611 40505344 9174 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9889 9174 603 41 0 9848 0
vsize: 39556
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 44978 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223684 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 45978 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 46978 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 47978 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 48979 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 49979 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21053
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 50979 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21106
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 51979 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21106
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 52979 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21106
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 53979 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21106
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 54980 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223744 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21106
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9262 0 0 0 55980 27 0 0 25 0 1 0 366054611 40767488 9240 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9953 9240 603 41 0 9912 0
vsize: 39812
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21106
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9287 0 0 0 56980 27 0 0 25 0 1 0 366054611 40898560 9265 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9985 9265 603 41 0 9944 0
vsize: 39940
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21110
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9431 0 0 0 57980 27 0 0 25 0 1 0 366054611 41426944 9409 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10114 9409 603 41 0 10073 0
vsize: 40456
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9553 0 0 0 58980 28 0 0 25 0 1 0 366054611 41959424 9531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10244 9531 603 41 0 10203 0
vsize: 40976
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9715 0 0 0 59980 28 0 0 25 0 1 0 366054611 42639360 9693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9693 603 41 0 10369 0
vsize: 41640
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 9938 0 0 0 60979 28 0 0 25 0 1 0 366054611 43565056 9916 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10636 9916 603 41 0 10595 0
vsize: 42544
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10033 0 0 0 61979 29 0 0 25 0 1 0 366054611 43962368 10011 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10733 10011 603 41 0 10692 0
vsize: 42932
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10033 0 0 0 62979 29 0 0 25 0 1 0 366054611 43962368 10011 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10733 10011 603 41 0 10692 0
vsize: 42932
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10033 0 0 0 63980 29 0 0 25 0 1 0 366054611 43962368 10011 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10011 603 41 0 10692 0
vsize: 42932
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10033 0 0 0 64980 29 0 0 25 0 1 0 366054611 43962368 10011 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10011 603 41 0 10692 0
vsize: 42932
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10038 0 0 0 65980 29 0 0 25 0 1 0 366054611 43962368 10016 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10016 603 41 0 10692 0
vsize: 42932
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10038 0 0 0 66980 29 0 0 25 0 1 0 366054611 43962368 10016 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10016 603 41 0 10692 0
vsize: 42932
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10038 0 0 0 67980 29 0 0 25 0 1 0 366054611 43962368 10016 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10016 603 41 0 10692 0
vsize: 42932
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10038 0 0 0 68980 29 0 0 25 0 1 0 366054611 43962368 10016 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10016 603 41 0 10692 0
vsize: 42932
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10039 0 0 0 69980 29 0 0 25 0 1 0 366054611 43962368 10017 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10017 603 41 0 10692 0
vsize: 42932
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10039 0 0 0 70980 29 0 0 25 0 1 0 366054611 43962368 10017 4294967295 134512640 134672761 3221224560 3221223744 134558664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10017 603 41 0 10692 0
vsize: 42932
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10040 0 0 0 71980 30 0 0 25 0 1 0 366054611 43962368 10018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10018 603 41 0 10692 0
vsize: 42932
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10040 0 0 0 72980 30 0 0 25 0 1 0 366054611 43962368 10018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10018 603 41 0 10692 0
vsize: 42932
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10040 0 0 0 73980 30 0 0 25 0 1 0 366054611 43962368 10018 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10018 603 41 0 10692 0
vsize: 42932
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10045 0 0 0 74980 30 0 0 25 0 1 0 366054611 43962368 10023 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10023 603 41 0 10692 0
vsize: 42932
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10045 0 0 0 75980 30 0 0 25 0 1 0 366054611 43962368 10023 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10023 603 41 0 10692 0
vsize: 42932
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10045 0 0 0 76980 30 0 0 25 0 1 0 366054611 43962368 10023 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10023 603 41 0 10692 0
vsize: 42932
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10055 0 0 0 77980 30 0 0 25 0 1 0 366054611 44158976 10033 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10033 603 41 0 10740 0
vsize: 43124
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10056 0 0 0 78980 30 0 0 25 0 1 0 366054611 44158976 10034 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10034 603 41 0 10740 0
vsize: 43124
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10059 0 0 0 79980 30 0 0 25 0 1 0 366054611 44158976 10037 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10037 603 41 0 10740 0
vsize: 43124
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10061 0 0 0 80980 30 0 0 25 0 1 0 366054611 44158976 10039 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10039 603 41 0 10740 0
vsize: 43124
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 81980 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 82980 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 83980 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 84980 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 85980 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 86980 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21112
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 87981 31 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 88981 32 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 89981 32 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10062 0 0 0 90981 32 0 0 25 0 1 0 366054611 44158976 10040 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10040 603 41 0 10740 0
vsize: 43124
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10072 0 0 0 91981 32 0 0 25 0 1 0 366054611 44158976 10050 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10050 603 41 0 10740 0
vsize: 43124
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10072 0 0 0 92981 32 0 0 25 0 1 0 366054611 44158976 10050 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10050 603 41 0 10740 0
vsize: 43124
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10073 0 0 0 93981 32 0 0 25 0 1 0 366054611 44158976 10051 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10051 603 41 0 10740 0
vsize: 43124
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10073 0 0 0 94981 32 0 0 25 0 1 0 366054611 44158976 10051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10051 603 41 0 10740 0
vsize: 43124
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10073 0 0 0 95981 32 0 0 25 0 1 0 366054611 44158976 10051 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10051 603 41 0 10740 0
vsize: 43124
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10073 0 0 0 96981 33 0 0 25 0 1 0 366054611 44158976 10051 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10051 603 41 0 10740 0
vsize: 43124
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10073 0 0 0 97981 33 0 0 25 0 1 0 366054611 44158976 10051 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10051 603 41 0 10740 0
vsize: 43124
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10082 0 0 0 98981 33 0 0 25 0 1 0 366054611 44158976 10060 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10060 603 41 0 10740 0
vsize: 43124
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10082 0 0 0 99981 33 0 0 25 0 1 0 366054611 44158976 10060 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10781 10060 603 41 0 10740 0
vsize: 43124
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10099 0 0 0 100980 33 0 0 25 0 1 0 366054611 44355584 10077 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10077 603 41 0 10788 0
vsize: 43316
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10106 0 0 0 101980 33 0 0 25 0 1 0 366054611 44355584 10084 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10084 603 41 0 10788 0
vsize: 43316
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10108 0 0 0 102981 33 0 0 25 0 1 0 366054611 44355584 10086 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10086 603 41 0 10788 0
vsize: 43316
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10112 0 0 0 103981 33 0 0 25 0 1 0 366054611 44355584 10090 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10090 603 41 0 10788 0
vsize: 43316
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 104981 33 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 105981 33 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 106981 33 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 107981 33 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 108982 33 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 109982 33 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 110982 34 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 111982 34 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10115 0 0 0 112982 34 0 0 25 0 1 0 366054611 44355584 10093 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10093 603 41 0 10788 0
vsize: 43316
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10116 0 0 0 113982 34 0 0 25 0 1 0 366054611 44355584 10094 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10094 603 41 0 10788 0
vsize: 43316
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10116 0 0 0 114982 34 0 0 25 0 1 0 366054611 44355584 10094 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10094 603 41 0 10788 0
vsize: 43316
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10116 0 0 0 115982 34 0 0 25 0 1 0 366054611 44355584 10094 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10094 603 41 0 10788 0
vsize: 43316
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10116 0 0 0 116982 34 0 0 25 0 1 0 366054611 44355584 10094 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10094 603 41 0 10788 0
vsize: 43316
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21114
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10116 0 0 0 117982 34 0 0 25 0 1 0 366054611 44355584 10094 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10094 603 41 0 10788 0
vsize: 43316
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21116
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10133 0 0 0 118982 35 0 0 25 0 1 0 366054611 44548096 10111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10876 10111 603 41 0 10835 0
vsize: 43504
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21116
Raw data (stat): 21051 (minisat+) R 21050 12452 12451 0 -1 0 10133 0 0 0 119982 35 0 0 25 0 1 0 366054611 44548096 10111 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10876 10111 603 41 0 10835 0
vsize: 43504
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 21116
Raw data (stat): 21051 (minisat+) Z 21050 12452 12451 0 -1 12 10136 0 0 0 119982 37 0 0 25 0 1 0 366054611 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.2
CPU user time (s): 1199.82
CPU system time (s): 0.374943
CPU usage (%): 100.012
Max. virtual memory (Kb): 43504
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####