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 5031

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 21:32:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2921 boxname=wulflinc12 idbench=325 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  270e069f649d19b0da4e4d23c0e1ebfc  /oldhome/oroussel/tmp/wulflinc12/normalized-frb40-19-2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-frb40-19-2.opb
IDLAUNCH: 2921
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        918792 kB
Buffers:         34692 kB
Cached:          61784 kB
SwapCached:         16 kB
Active:          60152 kB
Inactive:        39216 kB
HighTotal:      131008 kB
HighFree:        65296 kB
LowTotal:       903652 kB
LowFree:        853496 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11020 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:52:09 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 2921 7 1200.19 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.84 0.94 0.90 2/54 28254
Raw data (stat): 28254 (runsolver) R 28253 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420989841 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.99966 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 2943 0 0 0 988 9 0 0 25 0 1 0 420989841 14635008 2921 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3573 2921 603 41 0 3532 0
vsize: 14292
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 2943 0 0 0 1988 9 0 0 25 0 1 0 420989841 14635008 2921 4294967295 134512640 134672761 3221224624 3221223788 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3573 2921 603 41 0 3532 0
vsize: 14292
[startup+30.0006 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 3026 0 0 0 2987 10 0 0 25 0 1 0 420989841 14962688 3004 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3004 603 41 0 3612 0
vsize: 14612
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 3280 0 0 0 3986 11 0 0 25 0 1 0 420989841 15978496 3258 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3258 603 41 0 3860 0
vsize: 15604
[startup+50.0009 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 3716 0 0 0 4985 12 0 0 25 0 1 0 420989841 17870848 3694 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4363 3694 603 41 0 4322 0
vsize: 17452
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 4330 0 0 0 5984 14 0 0 25 0 1 0 420989841 20377600 4308 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4975 4308 603 41 0 4934 0
vsize: 19900
[startup+70.0016 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 4985 0 0 0 6982 15 0 0 25 0 1 0 420989841 23060480 4963 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5630 4963 603 41 0 5589 0
vsize: 22520
[startup+80.0014 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 5449 0 0 0 7980 17 0 0 25 0 1 0 420989841 25067520 5427 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6120 5427 603 41 0 6079 0
vsize: 24480
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 5940 0 0 0 8978 19 0 0 25 0 1 0 420989841 27074560 5918 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6610 5918 603 41 0 6569 0
vsize: 26440
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 6231 0 0 0 9977 20 0 0 25 0 1 0 420989841 28221440 6209 4294967295 134512640 134672761 3221224624 3221223808 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6890 6209 603 41 0 6849 0
vsize: 27560
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 6231 0 0 0 10977 20 0 0 25 0 1 0 420989841 28221440 6209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6890 6209 603 41 0 6849 0
vsize: 27560
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 6231 0 0 0 11978 20 0 0 25 0 1 0 420989841 28221440 6209 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6890 6209 603 41 0 6849 0
vsize: 27560
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 6231 0 0 0 12978 20 0 0 25 0 1 0 420989841 28221440 6209 4294967295 134512640 134672761 3221224624 3221223728 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6890 6209 603 41 0 6849 0
vsize: 27560
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 6458 0 0 0 13977 21 0 0 25 0 1 0 420989841 29147136 6436 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7116 6436 603 41 0 7075 0
vsize: 28464
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 6955 0 0 0 14975 23 0 0 25 0 1 0 420989841 31158272 6933 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7607 6933 603 41 0 7566 0
vsize: 30428
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 7336 0 0 0 15974 25 0 0 25 0 1 0 420989841 32751616 7314 4294967295 134512640 134672761 3221224624 3221223808 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7996 7314 603 41 0 7955 0
vsize: 31984
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 7709 0 0 0 16972 26 0 0 25 0 1 0 420989841 34217984 7687 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8354 7687 603 41 0 8313 0
vsize: 33416
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8050 0 0 0 17972 27 0 0 25 0 1 0 420989841 35700736 8028 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8716 8028 603 41 0 8675 0
vsize: 34864
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8392 0 0 0 18971 28 0 0 25 0 1 0 420989841 37023744 8370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9039 8370 603 41 0 8998 0
vsize: 36156
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8828 0 0 0 19969 30 0 0 25 0 1 0 420989841 38756352 8806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9462 8806 603 41 0 9421 0
vsize: 37848
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 20969 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 21969 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 22969 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 23969 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 24969 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 25969 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 26970 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 27970 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134561159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 28970 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8973 0 0 0 29970 31 0 0 25 0 1 0 420989841 39366656 8951 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8951 603 41 0 9570 0
vsize: 38444
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 30970 31 0 0 25 0 1 0 420989841 39366656 8952 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8952 603 41 0 9570 0
vsize: 38444
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 31970 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 32970 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 33971 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 34971 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 35971 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 36971 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 37971 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 38971 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 39972 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8974 0 0 0 40972 31 0 0 25 0 1 0 420989841 39362560 8952 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8952 603 41 0 9569 0
vsize: 38440
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8975 0 0 0 41972 31 0 0 25 0 1 0 420989841 39362560 8953 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9610 8953 603 41 0 9569 0
vsize: 38440
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 8979 0 0 0 42972 31 0 0 25 0 1 0 420989841 39624704 8957 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9674 8957 603 41 0 9633 0
vsize: 38696
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9069 0 0 0 43972 31 0 0 25 0 1 0 420989841 40022016 9047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9771 9047 603 41 0 9730 0
vsize: 39084
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 44972 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 45972 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 46972 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223796 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 47972 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 48973 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 49973 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 50973 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 51973 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 52973 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 53974 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 54974 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 55974 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9291 0 0 0 56974 32 0 0 25 0 1 0 420989841 40960000 9269 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10000 9269 603 41 0 9959 0
vsize: 40000
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9323 0 0 0 57974 32 0 0 25 0 1 0 420989841 41091072 9301 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10032 9301 603 41 0 9991 0
vsize: 40128
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9462 0 0 0 58974 32 0 0 25 0 1 0 420989841 41619456 9440 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10161 9440 603 41 0 10120 0
vsize: 40644
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9579 0 0 0 59974 33 0 0 25 0 1 0 420989841 42147840 9557 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10290 9557 603 41 0 10249 0
vsize: 41160
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9736 0 0 0 60973 33 0 0 25 0 1 0 420989841 42803200 9714 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10450 9714 603 41 0 10409 0
vsize: 41800
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 9953 0 0 0 61973 34 0 0 25 0 1 0 420989841 43597824 9931 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10644 9931 603 41 0 10603 0
vsize: 42576
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10062 0 0 0 62973 34 0 0 25 0 1 0 420989841 44027904 10040 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10749 10040 603 41 0 10708 0
vsize: 42996
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10062 0 0 0 63973 34 0 0 25 0 1 0 420989841 44027904 10040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10749 10040 603 41 0 10708 0
vsize: 42996
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10062 0 0 0 64973 34 0 0 25 0 1 0 420989841 44027904 10040 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10749 10040 603 41 0 10708 0
vsize: 42996
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10062 0 0 0 65972 35 0 0 25 0 1 0 420989841 44027904 10040 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10749 10040 603 41 0 10708 0
vsize: 42996
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10074 0 0 0 66971 35 0 0 25 0 1 0 420989841 44175360 10052 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10052 603 41 0 10744 0
vsize: 43140
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10075 0 0 0 67971 35 0 0 25 0 1 0 420989841 44175360 10053 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10053 603 41 0 10744 0
vsize: 43140
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10075 0 0 0 68971 35 0 0 25 0 1 0 420989841 44175360 10053 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10053 603 41 0 10744 0
vsize: 43140
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10075 0 0 0 69971 35 0 0 25 0 1 0 420989841 44175360 10053 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10053 603 41 0 10744 0
vsize: 43140
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10076 0 0 0 70972 35 0 0 25 0 1 0 420989841 44175360 10054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10054 603 41 0 10744 0
vsize: 43140
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10076 0 0 0 71972 35 0 0 25 0 1 0 420989841 44175360 10054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10054 603 41 0 10744 0
vsize: 43140
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10076 0 0 0 72972 35 0 0 25 0 1 0 420989841 44175360 10054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10054 603 41 0 10744 0
vsize: 43140
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10076 0 0 0 73972 35 0 0 25 0 1 0 420989841 44175360 10054 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10054 603 41 0 10744 0
vsize: 43140
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10076 0 0 0 74972 35 0 0 25 0 1 0 420989841 44175360 10054 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10054 603 41 0 10744 0
vsize: 43140
[startup+760.015 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10088 0 0 0 75973 35 0 0 25 0 1 0 420989841 44175360 10066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10066 603 41 0 10744 0
vsize: 43140
[startup+770.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10088 0 0 0 76973 35 0 0 25 0 1 0 420989841 44175360 10066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10066 603 41 0 10744 0
vsize: 43140
[startup+780.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10088 0 0 0 77973 35 0 0 25 0 1 0 420989841 44175360 10066 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10066 603 41 0 10744 0
vsize: 43140
[startup+790.017 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10098 0 0 0 78973 35 0 0 25 0 1 0 420989841 44339200 10076 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10076 603 41 0 10784 0
vsize: 43300
[startup+800.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10099 0 0 0 79973 35 0 0 25 0 1 0 420989841 44339200 10077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10077 603 41 0 10784 0
vsize: 43300
[startup+810.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10102 0 0 0 80974 35 0 0 25 0 1 0 420989841 44339200 10080 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10080 603 41 0 10784 0
vsize: 43300
[startup+820.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10106 0 0 0 81974 35 0 0 25 0 1 0 420989841 44339200 10084 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10084 603 41 0 10784 0
vsize: 43300
[startup+830.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 82974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+840.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 83974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+850.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 84973 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+860.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 85974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+870.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 86974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+880.018 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 87974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+890.019 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 88974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+900.019 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 89974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+910.019 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 90974 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+920.021 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10107 0 0 0 91975 35 0 0 25 0 1 0 420989841 44339200 10085 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10085 603 41 0 10784 0
vsize: 43300
[startup+930.021 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10117 0 0 0 92975 35 0 0 25 0 1 0 420989841 44339200 10095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10095 603 41 0 10784 0
vsize: 43300
[startup+940.022 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10118 0 0 0 93975 35 0 0 25 0 1 0 420989841 44339200 10096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10096 603 41 0 10784 0
vsize: 43300
[startup+950.023 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10119 0 0 0 94975 35 0 0 25 0 1 0 420989841 44339200 10097 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10097 603 41 0 10784 0
vsize: 43300
[startup+960.023 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10119 0 0 0 95976 35 0 0 25 0 1 0 420989841 44339200 10097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10097 603 41 0 10784 0
vsize: 43300
[startup+970.024 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10119 0 0 0 96976 35 0 0 25 0 1 0 420989841 44339200 10097 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10097 603 41 0 10784 0
vsize: 43300
[startup+980.024 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10119 0 0 0 97976 35 0 0 25 0 1 0 420989841 44339200 10097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10097 603 41 0 10784 0
vsize: 43300
[startup+990.025 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10119 0 0 0 98976 35 0 0 25 0 1 0 420989841 44339200 10097 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10097 603 41 0 10784 0
vsize: 43300
[startup+1000.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10129 0 0 0 99976 35 0 0 25 0 1 0 420989841 44339200 10107 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10107 603 41 0 10784 0
vsize: 43300
[startup+1010.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10129 0 0 0 100977 35 0 0 25 0 1 0 420989841 44339200 10107 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10107 603 41 0 10784 0
vsize: 43300
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10130 0 0 0 101977 35 0 0 25 0 1 0 420989841 44339200 10108 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10825 10108 603 41 0 10784 0
vsize: 43300
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10152 0 0 0 102977 35 0 0 25 0 1 0 420989841 44535808 10130 4294967295 134512640 134672761 3221224624 3221223792 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10130 603 41 0 10832 0
vsize: 43492
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10154 0 0 0 103977 35 0 0 25 0 1 0 420989841 44535808 10132 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10132 603 41 0 10832 0
vsize: 43492
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10158 0 0 0 104977 35 0 0 25 0 1 0 420989841 44535808 10136 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10136 603 41 0 10832 0
vsize: 43492
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10161 0 0 0 105978 35 0 0 25 0 1 0 420989841 44535808 10139 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10139 603 41 0 10832 0
vsize: 43492
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 106978 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 107978 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 108978 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 109978 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 110979 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 111979 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 112978 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 113979 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10162 0 0 0 114979 35 0 0 25 0 1 0 420989841 44535808 10140 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10140 603 41 0 10832 0
vsize: 43492
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10163 0 0 0 115979 35 0 0 25 0 1 0 420989841 44535808 10141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10141 603 41 0 10832 0
vsize: 43492
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10164 0 0 0 116979 36 0 0 25 0 1 0 420989841 44535808 10142 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10142 603 41 0 10832 0
vsize: 43492
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10164 0 0 0 117979 36 0 0 25 0 1 0 420989841 44535808 10142 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10142 603 41 0 10832 0
vsize: 43492
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10164 0 0 0 118980 36 0 0 25 0 1 0 420989841 44535808 10142 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10873 10142 603 41 0 10832 0
vsize: 43492
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28254
Raw data (stat): 28254 (minisat+) R 28253 25285 25284 0 -1 0 10182 0 0 0 119980 36 0 0 25 0 1 0 420989841 44732416 10160 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10921 10160 603 41 0 10880 0
vsize: 43684
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 28254
Raw data (stat): 28254 (minisat+) Z 28253 25285 25284 0 -1 12 10185 0 0 0 119980 38 0 0 25 0 1 0 420989841 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.06
CPU time (s): 1200.19
CPU user time (s): 1199.81
CPU system time (s): 0.382941
CPU usage (%): 100.011
Max. virtual memory (Kb): 43684
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####