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/submitted/manquinho/primes-dimacs-cnf/normalized-ii8e1.opb
MD5SUM	979ebd144bbd2b562b23479b90a02c66
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	343
Optimality of the best value was proved	NO
Number of terms in the objective function	1040
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	1040
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1040
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	1040
Total number of constraints	3656
Number of constraints which are clauses	3656
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	10
Trace number 6273

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 04:05:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4687 boxname=wulflinc5 idbench=175 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  979ebd144bbd2b562b23479b90a02c66  /oldhome/oroussel/tmp/wulflinc5/normalized-ii8e1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-ii8e1.opb /oldhome/oroussel/tmp/wulflinc5/normalized-ii8e1.opb
IDLAUNCH: 4687
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        894324 kB
Buffers:         35000 kB
Cached:          83700 kB
SwapCached:       2272 kB
Active:          56084 kB
Inactive:        67740 kB
HighTotal:      131008 kB
HighFree:        43400 kB
LowTotal:       903652 kB
LowFree:        850924 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10856 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:25:43 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4687 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3656 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 |    3656     8440 |    1218       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 474[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:56938     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        16 |  138118   322824 |   46039      16      122     7.6 |  0.000 % |
c |       116 |  138079   322737 |   50642     115     1410    12.3 |  0.046 % |
c |       266 |  133895   313079 |   55707     184     2165    11.8 |  2.794 % |
c |       491 |  124439   291410 |   61277     291     3481    12.0 |  9.032 % |
c |       828 |  116589   273300 |   67405     520     7496    14.4 | 14.418 % |
c ==============================================================================
c [1mFound solution: 469[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 |       829 |  116881   274044 |   38960     521     7517    14.4 | 14.418 % |
c ==============================================================================
c [1mFound solution: 468[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 |       830 |  116631   273466 |   38877     522     7593    14.5 | 14.418 % |
c |       930 |  113533   266320 |   42764     563     7971    14.2 | 16.683 % |
c |      1080 |  112171   263179 |   47041     690     8624    12.5 | 17.619 % |
c |      1306 |  111210   260962 |   51745     812    10816    13.3 | 18.280 % |
c |      1643 |   98559   231679 |   56919     962    12725    13.2 | 26.971 % |
c |      2149 |   84758   199759 |   62611    1201    16028    13.3 | 36.606 % |
c |      2908 |   84758   199759 |   68872    1960    27759    14.2 | 36.606 % |
c |      4048 |   72228   170741 |   75760    2889    39087    13.5 | 45.372 % |
c ==============================================================================
c [1mFound solution: 467[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 |      4797 |   69738   164992 |   23246    3561    47291    13.3 | 45.372 % |
c |      4899 |   69135   163597 |   25570    3647    47649    13.1 | 47.561 % |
c |      5050 |   68657   162483 |   28127    3783    49859    13.2 | 47.912 % |
c |      5275 |   67987   160926 |   30940    3970    51269    12.9 | 48.389 % |
c |      5612 |   67482   159758 |   34034    4292    55628    13.0 | 48.738 % |
c |      6118 |   64471   152731 |   37437    4701    58689    12.5 | 50.897 % |
c |      6878 |   63363   150150 |   41181    5395    68480    12.7 | 51.705 % |
c |      8017 |   62813   148888 |   45299    6507    85328    13.1 | 52.062 % |
c ==============================================================================
c [1mFound solution: 453[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 |      9278 |   61858   146762 |   20619    7736   105352    13.6 | 52.062 % |
c |      9378 |   60994   144752 |   22680    7774   106217    13.7 | 53.463 % |
c |      9528 |   60800   144303 |   24948    7904   106963    13.5 | 53.583 % |
c |      9754 |   60675   144015 |   27443    8122   109569    13.5 | 53.669 % |
c ==============================================================================
c [1mFound solution: 452[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 |      9802 |   60558   143738 |   20186    8170   110415    13.5 | 53.669 % |
c |      9902 |   60200   142915 |   22204    8247   110759    13.4 | 53.987 % |
c |     10052 |   60168   142843 |   24425    8397   111981    13.3 | 53.987 % |
c ==============================================================================
c [1mFound solution: 451[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 |     10230 |   60237   143025 |   20079    8575   115313    13.4 | 53.987 % |
c |     10330 |   60237   143025 |   22086    8675   116025    13.4 | 53.970 % |
c |     10481 |   59978   142425 |   24295    8814   117754    13.4 | 54.151 % |
c |     10706 |   59805   142026 |   26725    9026   120080    13.3 | 54.267 % |
c ==============================================================================
c [1mFound solution: 450[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 |     11004 |   59751   141884 |   19917    9324   123062    13.2 | 54.267 % |
c |     11105 |   59751   141884 |   21908    9425   123915    13.1 | 54.291 % |
c |     11255 |   59630   141607 |   24099    9571   124724    13.0 | 54.367 % |
c |     11480 |   59630   141607 |   26509    9796   128398    13.1 | 54.367 % |
c |     11817 |   59630   141607 |   29160   10133   137246    13.5 | 54.367 % |
c |     12323 |   58957   140045 |   32076   10609   141082    13.3 | 54.854 % |
c |     13083 |   58826   139743 |   35284   11356   226155    19.9 | 54.943 % |
c ==============================================================================
c [1mFound solution: 449[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 |     13714 |   58948   140061 |   19649   11987   256436    21.4 | 54.943 % |
c |     13814 |   58948   140061 |   21613   12087   257375    21.3 | 54.909 % |
c |     13965 |   58948   140061 |   23775   12238   259216    21.2 | 54.909 % |
c |     14191 |   58948   140061 |   26152   12464   262361    21.0 | 54.909 % |
c |     14530 |   58948   140061 |   28768   12803   285919    22.3 | 54.909 % |
c |     15036 |   58705   139495 |   31644   13263   289248    21.8 | 55.090 % |
c |     15795 |   58705   139495 |   34809   14022   300153    21.4 | 55.090 % |
c |     16934 |   58563   139168 |   38290   15157   323613    21.4 | 55.188 % |
c ==============================================================================
c [1mFound solution: 448[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 |     17398 |   58346   138651 |   19448   15483   319200    20.6 | 55.188 % |
c |     17500 |   58346   138651 |   21392   15585   322368    20.7 | 55.332 % |
c |     17651 |   58346   138651 |   23532   15736   323285    20.5 | 55.332 % |
c |     17877 |   58346   138651 |   25885   15962   329729    20.7 | 55.332 % |
c |     18214 |   58346   138651 |   28473   16299   335385    20.6 | 55.332 % |
c |     18720 |   58229   138372 |   31321   16800   349342    20.8 | 55.430 % |
c ==============================================================================
c [1mFound solution: 444[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 |     19471 |   58214   138364 |   19404   17491   354933    20.3 | 55.430 % |
c |     19571 |   58214   138364 |   21344   17591   356046    20.2 | 55.498 % |
c |     19722 |   58214   138364 |   23478   17742   356857    20.1 | 55.498 % |
c |     19947 |   58214   138364 |   25826   17967   361987    20.1 | 55.498 % |
c |     20284 |   58214   138364 |   28409   18304   374970    20.5 | 55.498 % |
c |     20790 |   58157   138234 |   31250   18809   382891    20.4 | 55.535 % |
c |     21549 |   58157   138234 |   34375   19568   418496    21.4 | 55.535 % |
c ==============================================================================
c [1mFound solution: 443[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 |     22119 |   58226   138416 |   19408   20138   435739    21.6 | 55.535 % |
c ==============================================================================
c [1mFound solution: 442[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 |     22130 |   58163   138236 |   19387   20094   430738    21.4 | 55.535 % |
c |     22231 |   58163   138236 |   21325   20195   432554    21.4 | 55.548 % |
c |     22382 |   58015   137891 |   23458   20333   435793    21.4 | 55.659 % |
c |     22608 |   57932   137696 |   25804   20549   440837    21.5 | 55.725 % |
c |     22945 |   57663   137074 |   28384   20833   450653    21.6 | 55.914 % |
c |     23451 |   57663   137074 |   31222   21339   461750    21.6 | 55.914 % |
c |     24210 |   57663   137074 |   34345   22098   473155    21.4 | 55.914 % |
c ==============================================================================
c [1mFound solution: 441[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 |     24695 |   57561   136872 |   19187   21110   454695    21.5 | 55.914 % |
c |     24795 |   57561   136872 |   21105   21210   455633    21.5 | 56.036 % |
c |     24946 |   57561   136872 |   23216   21361   458254    21.5 | 56.036 % |
c |     25173 |   57387   136468 |   25537   21535   460518    21.4 | 56.158 % |
c |     25512 |   57387   136468 |   28091   21874   469149    21.4 | 56.158 % |
c |     26020 |   57075   135740 |   30900   22281   476391    21.4 | 56.393 % |
c |     26780 |   56885   135307 |   33990   22145   474538    21.4 | 56.512 % |
c |     27919 |   56885   135307 |   37390   23284   511027    21.9 | 56.512 % |
c |     29628 |   56885   135307 |   41129   24993   546404    21.9 | 56.512 % |
c |     32190 |   56794   135094 |   45241   27532   637994    23.2 | 56.582 % |
c ==============================================================================
c [1mFound solution: 437[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 |     35757 |   56582   134637 |   18860   30955   734418    23.7 | 56.582 % |
c |     35859 |   56582   134637 |   20746   31057   735052    23.7 | 56.810 % |
c |     36009 |   56417   134255 |   22820   31140   736703    23.7 | 56.927 % |
c |     36234 |   56386   134181 |   25102   31364   738214    23.5 | 56.951 % |
c |     36574 |   56297   133977 |   27612   31702   740509    23.4 | 57.010 % |
c |     37080 |   55693   132572 |   30374   32102   755607    23.5 | 57.442 % |
c |     37839 |   55673   132526 |   33411   32859   772154    23.5 | 57.456 % |
c |     38982 |   55510   132149 |   36752   33964   792781    23.3 | 57.571 % |
c ==============================================================================
c [1mFound solution: 436[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 |     39746 |   55401   131871 |   18467   34620   794634    23.0 | 57.571 % |
c |     39846 |   55401   131871 |   20313   34720   796554    22.9 | 57.636 % |
c |     39996 |   55401   131871 |   22345   34870   799145    22.9 | 57.636 % |
c |     40222 |   55401   131871 |   24579   35096   802383    22.9 | 57.636 % |
c ==============================================================================
c [1mFound solution: 435[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 |     40546 |   55468   132047 |   18489   35420   813987    23.0 | 57.636 % |
c |     40646 |   55468   132047 |   20337   35520   815654    23.0 | 57.617 % |
c |     40797 |   55468   132047 |   22371   35671   817399    22.9 | 57.617 % |
c |     41023 |   55468   132047 |   24608   35897   827821    23.1 | 57.617 % |
c |     41360 |   55468   132047 |   27069   36234   844155    23.3 | 57.617 % |
c |     41866 |   55373   131831 |   29776   36629   848352    23.2 | 57.676 % |
c ==============================================================================
c [1mFound solution: 433[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 |     42257 |   55484   132119 |   18494   37020   861101    23.3 | 57.676 % |
c |     42357 |   55484   132119 |   20343   37120   864013    23.3 | 57.644 % |
c |     42508 |   55395   131911 |   22377   37266   865668    23.2 | 57.707 % |
c |     42734 |   55395   131911 |   24615   37492   871276    23.2 | 57.707 % |
c |     43071 |   55395   131911 |   27077   37829   875627    23.1 | 57.707 % |
c |     43577 |   55324   131751 |   29784   38334   886442    23.1 | 57.748 % |
c |     44338 |   55324   131751 |   32763   39095   897769    23.0 | 57.748 % |
c |     45477 |   55324   131751 |   36039   40234   933270    23.2 | 57.748 % |
c |     47185 |   55324   131751 |   39643   41942  1039252    24.8 | 57.748 % |
c ==============================================================================
c [1mFound solution: 432[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 |     49495 |   55124   131236 |   18374   43765  1075694    24.6 | 57.748 % |
c |     49595 |   55124   131236 |   20211   43865  1076889    24.6 | 57.885 % |
c |     49745 |   55124   131236 |   22232   44015  1081882    24.6 | 57.885 % |
c |     49972 |   55124   131236 |   24455   44242  1090656    24.7 | 57.885 % |
c |     50310 |   55026   131010 |   26901   44572  1093389    24.5 | 57.952 % |
c |     50817 |   55026   131010 |   29591   45079  1108118    24.6 | 57.952 % |
c |     51576 |   55026   131010 |   32550   45838  1144412    25.0 | 57.952 % |
c |     52715 |   55026   131010 |   35805   46977  1238694    26.4 | 57.952 % |
c ==============================================================================
c [1mFound solution: 431[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 |     53232 |   55093   131186 |   18364   47494  1257976    26.5 | 57.952 % |
c |     53332 |   55093   131186 |   20200   19750   481110    24.4 | 57.934 % |
c |     53482 |   55093   131186 |   22220   19900   484183    24.3 | 57.934 % |
c |     53708 |   55093   131186 |   24442   20126   490160    24.4 | 57.934 % |
c |     54045 |   55093   131186 |   26886   20463   495312    24.2 | 57.934 % |
c |     54551 |   55093   131186 |   29575   20969   501778    23.9 | 57.934 % |
c |     55310 |   55093   131186 |   32532   21728   536621    24.7 | 57.934 % |
c |     56451 |   55093   131186 |   35786   22869   584333    25.6 | 57.934 % |
c ==============================================================================
c [1mFound solution: 430[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 |     56597 |   55007   130951 |   18335   22988   586792    25.5 | 57.934 % |
c |     56698 |   55007   130951 |   20168   23089   587931    25.5 | 57.970 % |
c |     56848 |   55007   130951 |   22185   23239   589140    25.4 | 57.970 % |
c |     57074 |   55007   130951 |   24403   23465   591208    25.2 | 57.970 % |
c |     57411 |   55007   130951 |   26844   23802   598971    25.2 | 57.970 % |
c ==============================================================================
c [1mFound solution: 429[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 |     57840 |   55109   131215 |   18369   24231   608920    25.1 | 57.970 % |
c |     57940 |   55109   131215 |   20205   24331   613540    25.2 | 57.941 % |
c |     58092 |   55109   131215 |   22226   24483   614832    25.1 | 57.941 % |
c |     58317 |   55109   131215 |   24449   24708   622096    25.2 | 57.941 % |
c |     58656 |   55109   131215 |   26894   25047   628009    25.1 | 57.941 % |
c ==============================================================================
c [1mFound solution: 425[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 |     58928 |   55190   131436 |   18396   25313   631982    25.0 | 57.941 % |
c |     59028 |   55190   131436 |   20235   25413   632912    24.9 | 57.952 % |
c |     59178 |   55182   131418 |   22259   25557   636437    24.9 | 57.957 % |
c |     59403 |   55182   131418 |   24485   25782   644964    25.0 | 57.957 % |
c |     59742 |   55182   131418 |   26933   26121   651379    24.9 | 57.957 % |
c |     60249 |   55182   131418 |   29626   26628   665014    25.0 | 57.957 % |
c |     61009 |   55156   131357 |   32589   27384   676971    24.7 | 57.976 % |
c ==============================================================================
c [1mFound solution: 423[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 |     61228 |   55223   131533 |   18407   27603   681518    24.7 | 57.976 % |
c |     61328 |   55223   131533 |   20247   27703   684155    24.7 | 57.958 % |
c |     61479 |   55223   131533 |   22272   27854   685215    24.6 | 57.958 % |
c |     61704 |   55223   131533 |   24499   28079   688362    24.5 | 57.958 % |
c |     62041 |   55032   131087 |   26949   28395   696931    24.5 | 58.101 % |
c |     62547 |   55032   131087 |   29644   28901   707763    24.5 | 58.101 % |
c |     63307 |   55032   131087 |   32609   29661   746615    25.2 | 58.101 % |
c |     64446 |   55032   131087 |   35870   30800   767660    24.9 | 58.101 % |
c ==============================================================================
c [1mFound solution: 421[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 |     65351 |   55134   131351 |   18378   31705   826052    26.1 | 58.101 % |
c |     65451 |   55134   131351 |   20215   31805   826960    26.0 | 58.071 % |
c |     65601 |   54842   130670 |   22237   31262   821418    26.3 | 58.279 % |
c |     65826 |   54842   130670 |   24461   31487   824071    26.2 | 58.279 % |
c |     66163 |   54842   130670 |   26907   31824   832975    26.2 | 58.279 % |
c |     66669 |   54842   130670 |   29597   32330   872796    27.0 | 58.279 % |
c |     67428 |   54842   130670 |   32557   33089   883820    26.7 | 58.279 % |
c |     68571 |   54525   129922 |   35813   34210   906539    26.5 | 58.498 % |
c ==============================================================================
c [1mFound solution: 399[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 |     69825 |   55067   131229 |   18355   35464   940261    26.5 | 58.498 % |
c |     69928 |   55067   131229 |   20190   35567   941047    26.5 | 58.322 % |
c |     70079 |   54903   130850 |   22209   35716   946628    26.5 | 58.436 % |
c |     70304 |   54903   130850 |   24430   35941   963451    26.8 | 58.436 % |
c |     70641 |   54903   130850 |   26873   36278   979008    27.0 | 58.436 % |
c |     71147 |   54903   130850 |   29560   36784   998651    27.1 | 58.436 % |
c ==============================================================================
c [1mFound solution: 398[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 |     71808 |   54824   130639 |   18274   37433  1024116    27.4 | 58.436 % |
c |     71908 |   54824   130639 |   20101   37533  1031145    27.5 | 58.470 % |
c |     72058 |   54740   130442 |   22111   37628  1033603    27.5 | 58.530 % |
c ==============================================================================
c [1mFound solution: 397[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 |     72206 |   54836   130691 |   18278   37776  1037253    27.5 | 58.530 % |
c |     72307 |   54779   130560 |   20105   37875  1039084    27.4 | 58.543 % |
c |     72459 |   54639   130238 |   22116   37977  1042398    27.4 | 58.638 % |
c |     72684 |   54453   129812 |   24328   38183  1046963    27.4 | 58.760 % |
c |     73021 |   54453   129812 |   26760   38520  1053713    27.4 | 58.760 % |
c |     73527 |   54391   129669 |   29436   38964  1072243    27.5 | 58.801 % |
c |     74286 |   54391   129669 |   32380   39723  1121703    28.2 | 58.801 % |
c |     75425 |   54391   129669 |   35618   40862  1145142    28.0 | 58.801 % |
c |     77133 |   54387   129660 |   39180   42569  1205969    28.3 | 58.803 % |
c |     79695 |   54387   129660 |   43098   45131  1465464    32.5 | 58.803 % |
c |     83540 |   54303   129465 |   47408   48974  1612496    32.9 | 58.859 % |
c |     89306 |   54167   129150 |   52149   54655  1870566    34.2 | 58.954 % |
c ==============================================================================
c [1mFound solution: 395[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 |     89567 |   54235   129327 |   18078   54916  1879160    34.2 | 58.954 % |
c |     89667 |   54235   129327 |   19885   22064   690212    31.3 | 58.933 % |
c |     89817 |   54235   129327 |   21874   22214   694376    31.3 | 58.933 % |
c |     90043 |   53962   128691 |   24061   22433   697283    31.1 | 59.129 % |
c |     90380 |   53962   128691 |   26467   22770   703174    30.9 | 59.129 % |
c |     90887 |   53962   128691 |   29114   23277   723824    31.1 | 59.129 % |
c |     91646 |   53962   128691 |   32026   24036   746277    31.0 | 59.129 % |
c |     92785 |   53962   128691 |   35228   25175   810229    32.2 | 59.129 % |
c |     94494 |   53962   128691 |   38751   26884   893776    33.2 | 59.129 % |
c |     97058 |   53502   127624 |   42626   29325  1028663    35.1 | 59.448 % |
c |    100903 |   53502   127624 |   46889   33170  1443156    43.5 | 59.448 % |
c ==============================================================================
c [1mFound solution: 392[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 |    102207 |   53321   127160 |   17773   34224  1571198    45.9 | 59.448 % |
c |    102307 |   53321   127160 |   19550   34324  1572900    45.8 | 59.571 % |
c |    102457 |   53321   127160 |   21505   34474  1576618    45.7 | 59.571 % |
c |    102682 |   53321   127160 |   23655   34699  1590651    45.8 | 59.571 % |
c |    103019 |   53263   127025 |   26021   35029  1604255    45.8 | 59.683 % |
c |    103525 |   52966   126331 |   28623   35510  1643039    46.3 | 59.823 % |
c |    104284 |   52966   126331 |   31485   36269  1749276    48.2 | 59.823 % |
c |    105424 |   52966   126331 |   34634   37409  1794657    48.0 | 59.823 % |
c |    107133 |   52966   126331 |   38098   39118  1869384    47.8 | 59.823 % |
c ==============================================================================
c [1mFound solution: 391[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 |    107998 |   53024   126481 |   17674   39983  1909277    47.8 | 59.823 % |
c |    108098 |   53024   126481 |   19441   40083  1912087    47.7 | 59.806 % |
c |    108250 |   53024   126481 |   21385   40235  1914748    47.6 | 59.806 % |
c |    108475 |   53024   126481 |   23524   40460  1928824    47.7 | 59.806 % |
c |    108815 |   53024   126481 |   25876   40800  1937853    47.5 | 59.806 % |
c |    109321 |   53024   126481 |   28464   41306  1972223    47.7 | 59.806 % |
c |    110081 |   53024   126481 |   31310   42066  2008878    47.8 | 59.806 % |
c |    111220 |   53024   126481 |   34441   43205  2054716    47.6 | 59.806 % |
c |    112928 |   53024   126481 |   37885   44913  2150068    47.9 | 59.806 % |
c |    115491 |   53024   126481 |   41674   47476  2336613    49.2 | 59.806 % |
c |    119337 |   53024   126481 |   45841   51322  3172972    61.8 | 59.806 % |
c ==============================================================================
c [1mFound solution: 387[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 |    120233 |   53130   126749 |   17710   52218  3214371    61.6 | 59.806 % |
c |    120333 |   53130   126749 |   19481   22955  1343612    58.5 | 59.785 % |
c |    120484 |   53096   126671 |   21429   22979  1346137    58.6 | 59.806 % |
c |    120710 |   53096   126671 |   23572   23205  1352940    58.3 | 59.806 % |
c |    121047 |   53096   126671 |   25929   23542  1362460    57.9 | 59.806 % |
c |    121553 |   53096   126671 |   28522   24048  1391843    57.9 | 59.806 % |
c |    122312 |   53096   126671 |   31374   24807  1414227    57.0 | 59.806 % |
c |    123451 |   53096   126671 |   34511   25946  1500160    57.8 | 59.806 % |
c |    125160 |   53096   126671 |   37962   27655  1569798    56.8 | 59.806 % |
c |    127722 |   53096   126671 |   41759   30217  1659676    54.9 | 59.806 % |
c ==============================================================================
c [1mFound solution: 386[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 |    129602 |   53012   126448 |   17670   32097  1735795    54.1 | 59.806 % |
c |    129703 |   53012   126448 |   19437   32198  1737801    54.0 | 59.842 % |
c |    129853 |   53012   126448 |   21380   32348  1739600    53.8 | 59.842 % |
c |    130078 |   53012   126448 |   23518   32573  1758908    54.0 | 59.842 % |
c |    130415 |   53012   126448 |   25870   32910  1767014    53.7 | 59.842 % |
c |    130921 |   53012   126448 |   28457   33416  1778011    53.2 | 59.842 % |
c |    131681 |   52927   126253 |   31303   34175  1825203    53.4 | 59.898 % |
c |    132822 |   52911   126213 |   34433   35315  1901575    53.8 | 59.915 % |
c |    134532 |   52911   126213 |   37877   37025  1997722    54.0 | 59.915 % |
c |    137094 |   52911   126213 |   41664   39587  2172163    54.9 | 59.915 % |
c |    140939 |   52911   126213 |   45831   43432  2407350    55.4 | 59.915 % |
c ==============================================================================
c [1mFound solution: 385[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 |    145735 |   52806   125987 |   17602   48221  2619092    54.3 | 59.915 % |
c |    145835 |   52806   125987 |   19362   23203   702614    30.3 | 60.010 % |
c |    145985 |   52806   125987 |   21298   23353   706014    30.2 | 60.010 % |
c |    146212 |   52806   125987 |   23428   23580   713242    30.2 | 60.010 % |
c |    146550 |   52806   125987 |   25771   23918   726339    30.4 | 60.010 % |
c |    147056 |   52806   125987 |   28348   24424   742527    30.4 | 60.010 % |
c |    147815 |   52806   125987 |   31183   25183   767688    30.5 | 60.010 % |
c |    148954 |   52806   125987 |   34301   26322   787456    29.9 | 60.010 % |
c |    150662 |   52806   125987 |   37731   28030   929651    33.2 | 60.010 % |
c |    153224 |   52806   125987 |   41504   30592  1101605    36.0 | 60.010 % |
c |    157068 |   52806   125987 |   45655   34436  1729482    50.2 | 60.010 % |
c |    162835 |   52806   125987 |   50220   40203  2287408    56.9 | 60.010 % |
c |    171486 |   52806   125987 |   55242   48854  4501838    92.1 | 60.010 % |
c |    184460 |   52806   125987 |   60766   61828  5894807    95.3 | 60.010 % |
c |    203921 |   52806   125987 |   66843   81289  7133338    87.8 | 60.010 % |
c ==============================================================================
c [1mFound solution: 384[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 |    228199 |   52365   124877 |   17455   21102  2950215   139.8 | 60.010 % |
c |    228299 |   52365   124877 |   19200   21202  2952021   139.2 | 60.293 % |
c |    228449 |   52365   124877 |   21120   21352  2958624   138.6 | 60.293 % |
c |    228674 |   52365   124877 |   23232   21577  2971024   137.7 | 60.293 % |
c |    229011 |   52365   124877 |   25555   21914  2975769   135.8 | 60.293 % |
c |    229522 |   52365   124877 |   28111   22425  2982227   133.0 | 60.293 % |
c |    230281 |   52365   124877 |   30922   23184  3024901   130.5 | 60.293 % |
c |    231421 |   52365   124877 |   34014   24324  3047739   125.3 | 60.293 % |
c ==============================================================================
c [1mFound solution: 383[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 |    232583 |   52422   125024 |   17474   25486  3083857   121.0 | 60.293 % |
c |    232683 |   52422   125024 |   19221   25586  3085557   120.6 | 60.276 % |
c |    232834 |   52422   125024 |   21143   25737  3090075   120.1 | 60.276 % |
c |    233059 |   52422   125024 |   23257   25962  3092906   119.1 | 60.276 % |
c |    233396 |   52422   125024 |   25583   26299  3096814   117.8 | 60.276 % |
c |    233902 |   52422   125024 |   28142   26805  3104042   115.8 | 60.276 % |
c |    234661 |   52422   125024 |   30956   27564  3120811   113.2 | 60.276 % |
c |    235800 |   52422   125024 |   34051   28703  3155609   109.9 | 60.276 % |
c |    237508 |   52422   125024 |   37457   30411  3285079   108.0 | 60.276 % |
c |    240070 |   52356   124868 |   41202   32957  3368763   102.2 | 60.328 % |
c |    243914 |   52291   124720 |   45323   36796  3601189    97.9 | 60.371 % |
c ==============================================================================
c [1mFound solution: 382[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 |    249200 |   51887   123719 |   17295   41809  3896215    93.2 | 60.371 % |
c |    249300 |   51887   123719 |   19024   41909  3898427    93.0 | 60.634 % |
c |    249452 |   51853   123642 |   20926   42059  3900218    92.7 | 60.658 % |
c |    249677 |   51823   123572 |   23019   42277  3902136    92.3 | 60.679 % |
c |    250014 |   51823   123572 |   25321   42614  3910680    91.8 | 60.679 % |
c |    250520 |   51823   123572 |   27853   43120  3928389    91.1 | 60.679 % |
c |    251279 |   51823   123572 |   30639   43879  3958204    90.2 | 60.679 % |
c |    252418 |   51823   123572 |   33703   45018  3994711    88.7 | 60.679 % |
c |    254129 |   51763   123431 |   37073   46704  4054559    86.8 | 60.724 % |
c |    256692 |   51763   123431 |   40780   49267  4190756    85.1 | 60.724 % |
c |    260537 |   51506   122837 |   44858   52663  4516221    85.8 | 60.900 % |
c |    266304 |   51506   122837 |   49344   58430  4894888    83.8 | 60.900 % |
c |    274954 |   51506   122837 |   54279   67080  5568885    83.0 | 60.900 % |
c |    287928 |   51506   122837 |   59707   80054  7200542    89.9 | 60.900 % |
c |    307389 |   51506   122837 |   65677   24926  2404222    96.5 | 60.900 % |
c ==============================================================================
c [1mFound solution: 381[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 |    308363 |   51567   122994 |   17189   25900  2465006    95.2 | 60.900 % |
c |    308464 |   51567   122994 |   18907   26001  2470191    95.0 | 60.892 % |
c |    308614 |   51567   122994 |   20798   26151  2478996    94.8 | 60.892 % |
c |    308839 |   51567   122994 |   22878   26376  2493704    94.5 | 60.892 % |
c |    309176 |   51567   122994 |   25166   26713  2505579    93.8 | 60.892 % |
c |    309682 |   51567   122994 |   27683   27219  2537948    93.2 | 60.892 % |
c |    310441 |   51567   122994 |   30451   27978  2646998    94.6 | 60.892 % |
c |    311584 |   51567   122994 |   33496   29121  2671848    91.7 | 60.892 % |
c |    313293 |   51567   122994 |   36846   30830  2742395    89.0 | 60.892 % |
c |    315856 |   51567   122994 |   40530   33393  2805529    84.0 | 60.892 % |
c ==============================================================================
c [1mFound solution: 380[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 |    317254 |   51422   122628 |   17140   34773  2846286    81.9 | 60.892 % |
c |    317354 |   51422   122628 |   18854   34873  2848133    81.7 | 60.979 % |
c |    317506 |   51422   122628 |   20739   35025  2851911    81.4 | 60.979 % |
c |    317732 |   51422   122628 |   22813   35251  2859718    81.1 | 60.979 % |
c |    318069 |   51422   122628 |   25094   35588  2869911    80.6 | 60.979 % |
c |    318575 |   51422   122628 |   27604   36094  2877645    79.7 | 60.979 % |
c |    319335 |   51422   122628 |   30364   36854  2920600    79.2 | 60.979 % |
c |    320474 |   51422   122628 |   33401   37993  2961503    77.9 | 60.979 % |
c |    322184 |   51422   122628 |   36741   39703  3066663    77.2 | 60.979 % |
c |    324746 |   51422   122628 |   40415   42265  3370120    79.7 | 60.979 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 -x11 x12 x13 -x14 x15 -x16 -x17 x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 -x61 x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 -x93 x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 -x125 x126 x127 -x128 x129 -x130 x131 -x132 -x133 x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 -x145 x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 -x189 x190 x191 -x192 x193 -x194 x195 -x196 -x197 x198 x199 -x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 -x209 x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 -x229 x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 -x241 x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 -x259 -x260 x261 -x262 x263 -x264 x265 -x266 -x267 x268 x269 -x270 x271 -x272 -x273 x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 -x293 x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 -x305 x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 x359 -x360 -x361 x362 x363 -x364 -x365 -x366 -x367 -x368 -x369 x370 -x371 -x372 -x373 x374 -x375 x376 -x377 x378 -x379 x380 -x381 x382 -x383 x384 -x385 x386 -x387 x388 -x389 -x390 -x391 x392 -x393 -x394 x395 -x396 -x397 x398 -x399 -x400 -x401 x402 -x403 -x404 -x405 -x406 x407 -x408 -x409 x410 -x411 -x412 -x413 x414 -x415 x416 -x417 x418 -x419 x420 -x421 x422 -x423 x424 -x425 x426 -x427 x428 x429 -x430 -x431 x432 -x433 -x434 -x435 -x436 -x437 x438 -x439 -x440 -x441 x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 x450 x451 -x452 -x453 x454 -x455 x456 -x457 x458 -x459 x460 -x461 x462 -x463 x464 -x465 x466 -x467 x468 -x469 -x470 -x471 x472 -x473 -x474 x475 -x476 -x477 x478 -x479 -x480 x481 -x482 -x483 x484 -x485 x486 -x487 x488 -x489 x490 -x491 x492 -x493 x494 -x495 x496 -x497 x498 -x499 x500 -x501 x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 x510 x511 -x512 -x513 x514 -x515 x516 -x517 x518 -x519 x520 -x521 x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 x530 x531 -x532 -x533 x534 -x535 x536 -x537 x538 -x539 x540 -x541 x542 -x543 -x544 x545 -x546 -x547 -x548 -x549 x550 -x551 -x552 -x553 x554 -x555 x556 -x557 x558 -x559 x560 -x561 -x562 x563 -x564 -x565 -x566 -x567 -x568 -x569 x570 -x571 -x572 -x573 x574 -x575 x576 -x577 x578 -x579 x580 -x581 x582 -x583 -x584 -x585 -x586 x587 -x588 -x589 x590 -x591 -x592 -x593 x594 -x595 x596 -x597 x598 -x599 x600 -x601 x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 x610 x611 -x612 -x613 x614 -x615 x616 -x617 x618 -x619 x620 -x621 x622 -x623 x624 -x625 x626 -x627 x628 x629 -x630 -x631 x632 -x633 -x634 -x635 -x636 -x637 x638 -x639 -x640 -x641 x642 x643 -x644 -x645 -x646 -x647 -x648 -x649 x650 -x651 -x652 -x653 x654 -x655 x656 -x657 x658 -x659 x660 -x661 -x662 -x663 x664 -x665 x666 -x667 x668 -x669 -x670 -x671 x672 -x673 x674 -x675 -x676 -x677 x678 x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 x690 -x691 x692 -x693 x694 -x695 x696 x697 -x698 -x699 x700 -x701 -x702 x703 -x704 -x705 -x706 -x707 -x708 -x709 x710 -x711 -x712 -x713 x714 -x715 x716 -x717 x718 -x719 x720 -x721 x722 -x723 -x724 x725 -x726 -x727 -x728 -x729 x730 -x731 -x732 -x733 x734 -x735 x736 -x737 x738 -x739 x740 -x741 x742 -x743 x#### 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.92 0.96 0.91 2/54 29425
Raw data (stat): 29425 (runsolver) R 29424 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423354898 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4288 0 0 0 987 11 0 0 25 0 1 0 423354898 20066304 4115 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4899 4115 603 41 0 4858 0
vsize: 19596
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4398 0 0 0 1985 12 0 0 25 0 1 0 423354898 20832256 4225 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5086 4225 603 41 0 5045 0
vsize: 20344
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4398 0 0 0 2985 12 0 0 25 0 1 0 423354898 20832256 4225 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5086 4225 603 41 0 5045 0
vsize: 20344
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4413 0 0 0 3984 12 0 0 25 0 1 0 423354898 20832256 4240 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5086 4240 603 41 0 5045 0
vsize: 20344
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4475 0 0 0 4984 12 0 0 25 0 1 0 423354898 21114880 4302 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5155 4302 603 41 0 5114 0
vsize: 20620
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4664 0 0 0 5983 14 0 0 25 0 1 0 423354898 21897216 4491 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5346 4491 603 41 0 5305 0
vsize: 21384
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4782 0 0 0 6983 14 0 0 25 0 1 0 423354898 22433792 4609 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5477 4609 603 41 0 5436 0
vsize: 21908
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4862 0 0 0 7982 14 0 0 25 0 1 0 423354898 22683648 4689 4294967295 134512640 134672761 3221224576 3221223680 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5538 4689 603 41 0 5497 0
vsize: 22152
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5081 0 0 0 8982 15 0 0 25 0 1 0 423354898 23621632 4908 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5767 4908 603 41 0 5726 0
vsize: 23068
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5225 0 0 0 9982 16 0 0 25 0 1 0 423354898 24350720 5052 4294967295 134512640 134672761 3221224576 3221223776 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5945 5052 603 41 0 5904 0
vsize: 23780
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5345 0 0 0 10982 16 0 0 25 0 1 0 423354898 24752128 5172 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5172 603 41 0 6002 0
vsize: 24172
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5539 0 0 0 11981 16 0 0 25 0 1 0 423354898 25559040 5366 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6240 5366 603 41 0 6199 0
vsize: 24960
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5691 0 0 0 12981 17 0 0 25 0 1 0 423354898 26185728 5518 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6393 5518 603 41 0 6352 0
vsize: 25572
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5845 0 0 0 13980 18 0 0 25 0 1 0 423354898 26722304 5672 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6524 5672 603 41 0 6483 0
vsize: 26096
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5847 0 0 0 14980 18 0 0 25 0 1 0 423354898 26722304 5674 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6524 5674 603 41 0 6483 0
vsize: 26096
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5847 0 0 0 15980 18 0 0 25 0 1 0 423354898 26722304 5674 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6524 5674 603 41 0 6483 0
vsize: 26096
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5848 0 0 0 16980 18 0 0 25 0 1 0 423354898 26722304 5675 4294967295 134512640 134672761 3221224576 3221223876 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6524 5675 603 41 0 6483 0
vsize: 26096
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5849 0 0 0 17980 18 0 0 25 0 1 0 423354898 26722304 5676 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6524 5676 603 41 0 6483 0
vsize: 26096
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5897 0 0 0 18980 18 0 0 25 0 1 0 423354898 26984448 5724 4294967295 134512640 134672761 3221224576 3221223592 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6588 5724 603 41 0 6547 0
vsize: 26352
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6182 0 0 0 19980 19 0 0 25 0 1 0 423354898 28184576 6009 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6881 6009 603 41 0 6840 0
vsize: 27524
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6340 0 0 0 20980 20 0 0 25 0 1 0 423354898 28725248 6167 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7013 6167 603 41 0 6972 0
vsize: 28052
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6512 0 0 0 21979 20 0 0 25 0 1 0 423354898 29528064 6339 4294967295 134512640 134672761 3221224576 3221223760 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6339 603 41 0 7168 0
vsize: 28836
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 22979 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7305 6461 603 41 0 7264 0
vsize: 29220
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 23979 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223760 134559532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7305 6461 603 41 0 7264 0
vsize: 29220
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 24979 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7305 6461 603 41 0 7264 0
vsize: 29220
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 25980 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7305 6461 603 41 0 7264 0
vsize: 29220
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 26980 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7305 6461 603 41 0 7264 0
vsize: 29220
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6685 0 0 0 27980 21 0 0 25 0 1 0 423354898 30187520 6512 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7370 6512 603 41 0 7329 0
vsize: 29480
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6839 0 0 0 28980 21 0 0 25 0 1 0 423354898 30855168 6666 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6666 603 41 0 7492 0
vsize: 30132
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 7049 0 0 0 29979 22 0 0 25 0 1 0 423354898 31657984 6876 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6876 603 41 0 7688 0
vsize: 30916
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 7278 0 0 0 30978 23 0 0 25 0 1 0 423354898 32595968 7105 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7958 7105 603 41 0 7917 0
vsize: 31832
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 7662 0 0 0 31977 24 0 0 25 0 1 0 423354898 34193408 7489 4294967295 134512640 134672761 3221224576 3221223680 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8348 7489 603 41 0 8307 0
vsize: 33392
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8036 0 0 0 32976 25 0 0 25 0 1 0 423354898 35667968 7863 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8708 7863 603 41 0 8667 0
vsize: 34832
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 33976 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223680 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 34976 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 35977 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 36977 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 37977 26 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 38977 26 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 39977 26 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7899 603 41 0 8700 0
vsize: 34964
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 40978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 41978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 42978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 43978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 44978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 45978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 46978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 47979 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223680 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8741 7901 603 41 0 8700 0
vsize: 34964
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8242 0 0 0 48978 26 0 0 25 0 1 0 423354898 36597760 8069 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8935 8069 603 41 0 8894 0
vsize: 35740
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8580 0 0 0 49977 27 0 0 25 0 1 0 423354898 37924864 8407 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9259 8407 603 41 0 9218 0
vsize: 37036
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8982 0 0 0 50977 28 0 0 25 0 1 0 423354898 39522304 8809 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9649 8809 603 41 0 9608 0
vsize: 38596
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 9418 0 0 0 51976 29 0 0 25 0 1 0 423354898 41377792 9245 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9245 603 41 0 10061 0
vsize: 40408
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 9675 0 0 0 52975 30 0 0 25 0 1 0 423354898 42450944 9502 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10364 9502 603 41 0 10323 0
vsize: 41456
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 9956 0 0 0 53975 31 0 0 25 0 1 0 423354898 43528192 9783 4294967295 134512640 134672761 3221224576 3221223712 134560613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10627 9783 603 41 0 10586 0
vsize: 42508
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10232 0 0 0 54974 32 0 0 25 0 1 0 423354898 44728320 10059 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10920 10059 603 41 0 10879 0
vsize: 43680
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10464 0 0 0 55973 32 0 0 25 0 1 0 423354898 45662208 10291 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11148 10291 603 41 0 11107 0
vsize: 44592
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10728 0 0 0 56973 33 0 0 25 0 1 0 423354898 46731264 10555 4294967295 134512640 134672761 3221224576 3221223680 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11409 10555 603 41 0 11368 0
vsize: 45636
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10961 0 0 0 57972 34 0 0 25 0 1 0 423354898 47661056 10788 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11636 10788 603 41 0 11595 0
vsize: 46544
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11100 0 0 0 58971 35 0 0 25 0 1 0 423354898 48197632 10927 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11767 10927 603 41 0 11726 0
vsize: 47068
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11264 0 0 0 59971 35 0 0 25 0 1 0 423354898 49123328 11091 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11993 11091 603 41 0 11952 0
vsize: 47972
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11420 0 0 0 60971 36 0 0 25 0 1 0 423354898 49786880 11247 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12155 11247 603 41 0 12114 0
vsize: 48620
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11605 0 0 0 61971 36 0 0 25 0 1 0 423354898 50450432 11432 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12317 11432 603 41 0 12276 0
vsize: 49268
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11779 0 0 0 62970 37 0 0 25 0 1 0 423354898 51245056 11606 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11606 603 41 0 12470 0
vsize: 50044
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11954 0 0 0 63970 37 0 0 25 0 1 0 423354898 51908608 11781 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12673 11781 603 41 0 12632 0
vsize: 50692
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12114 0 0 0 64970 37 0 0 25 0 1 0 423354898 52609024 11941 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12844 11941 603 41 0 12803 0
vsize: 51376
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12287 0 0 0 65970 38 0 0 25 0 1 0 423354898 53272576 12114 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13006 12114 603 41 0 12965 0
vsize: 52024
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12440 0 0 0 66969 38 0 0 25 0 1 0 423354898 53936128 12267 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13168 12267 603 41 0 13127 0
vsize: 52672
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12500 0 0 0 67969 39 0 0 25 0 1 0 423354898 54202368 12327 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13233 12327 603 41 0 13192 0
vsize: 52932
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12584 0 0 0 68969 39 0 0 25 0 1 0 423354898 54468608 12411 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13298 12411 603 41 0 13257 0
vsize: 53192
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12976 0 0 0 69968 40 0 0 25 0 1 0 423354898 56074240 12803 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13690 12803 603 41 0 13649 0
vsize: 54760
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 13403 0 0 0 70968 41 0 0 25 0 1 0 423354898 57815040 13230 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14115 13230 603 41 0 14074 0
vsize: 56460
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 13864 0 0 0 71966 43 0 0 25 0 1 0 423354898 59695104 13691 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14574 13691 603 41 0 14533 0
vsize: 58296
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 14282 0 0 0 72965 44 0 0 25 0 1 0 423354898 61435904 14109 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14999 14109 603 41 0 14958 0
vsize: 59996
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 14718 0 0 0 73964 46 0 0 25 0 1 0 423354898 63180800 14545 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15425 14545 603 41 0 15384 0
vsize: 61700
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 15125 0 0 0 74962 47 0 0 25 0 1 0 423354898 64794624 14952 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15819 14952 603 41 0 15778 0
vsize: 63276
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 15543 0 0 0 75961 49 0 0 25 0 1 0 423354898 66531328 15370 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16243 15370 603 41 0 16202 0
vsize: 64972
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 15932 0 0 0 76959 50 0 0 25 0 1 0 423354898 68128768 15759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16633 15759 603 41 0 16592 0
vsize: 66532
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 77959 51 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 78958 51 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223740 134564518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 79957 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223728 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 80957 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 81958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 82958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223720 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 83958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 84958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 85958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 86958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 87958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 88959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 89959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 90959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 91959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 92959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+940.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 93960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 94960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223760 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 95960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 96960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 97960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 98961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 99961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 100961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 101961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 102961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 103961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 104962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 105962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 106962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 107962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 108962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223748 134559060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 109963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 110963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 111963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 112963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 113963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223632 134565048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 114963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 115963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 116963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 117963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 118963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29425
Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 119964 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 16039 603 41 0 16886 0
vsize: 67708
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29425
Raw data (stat): 29425 (minisat+) Z 29424 24215 24214 0 -1 12 16215 0 0 0 119964 55 0 0 25 0 1 0 423354898 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.64
CPU system time (s): 0.556915
CPU usage (%): 100.011
Max. virtual memory (Kb): 67708
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####