PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 04:42:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4840 boxname=wulflinc8 idbench=328 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  38d41fdbe49543e8928c5210e4323f00  /oldhome/oroussel/tmp/wulflinc8/normalized-frb40-19-5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-frb40-19-5.opb /oldhome/oroussel/tmp/wulflinc8/normalized-frb40-19-5.opb
IDLAUNCH: 4840
/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:        873528 kB
Buffers:         37756 kB
Cached:         101848 kB
SwapCached:          0 kB
Active:          77928 kB
Inactive:        66348 kB
HighTotal:      131008 kB
HighFree:        23492 kB
LowTotal:       903652 kB
LowFree:        850036 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11460 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:02:48 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4840 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41619 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 |   41619    83238 |   13873       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  114248   253263 |   38082       0        0     nan |  0.000 % |
c |       100 |  113419   251385 |   41890      83      521     6.3 |  1.027 % |
c |       250 |  113050   250549 |   46079     229     2608    11.4 |  1.363 % |
c |       475 |  111143   246193 |   50687     389     3518     9.0 |  3.673 % |
c |       812 |  108603   240380 |   55755     648     6606    10.2 |  6.723 % |
c ==============================================================================
c [1mFound solution: -28[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 |      1012 |  106344   235178 |   35448     780     7266     9.3 |  6.723 % |
c |      1113 |  105178   232503 |   38992     845     7690     9.1 | 11.083 % |
c |      1263 |  103477   228572 |   42892     933     8717     9.3 | 13.186 % |
c |      1488 |  100183   220935 |   47181    1044     9541     9.1 | 17.454 % |
c |      1825 |   98252   216473 |   51899    1320    12202     9.2 | 19.900 % |
c |      2331 |   93988   206592 |   57089    1677    15664     9.3 | 25.478 % |
c ==============================================================================
c [1mFound solution: -29[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 |      2810 |   91027   199789 |   30342    1996    18261     9.1 | 25.478 % |
c |      2910 |   90754   199161 |   33376    2088    19112     9.2 | 29.856 % |
c |      3060 |   89546   196334 |   36713    2131    19858     9.3 | 31.545 % |
c |      3285 |   89546   196334 |   40385    2356    21433     9.1 | 31.545 % |
c |      3623 |   85726   187499 |   44423    2547    23058     9.1 | 36.454 % |
c |      4129 |   82529   180082 |   48866    2905    26348     9.1 | 40.664 % |
c |      4888 |   77674   168778 |   53752    3393    35017    10.3 | 47.087 % |
c |      6027 |   70695   152386 |   59127    3940    40474    10.3 | 56.573 % |
c |      7735 |   62629   133482 |   65040    4697    50303    10.7 | 67.744 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8684 |   59926   127049 |   19975    5329    58012    10.9 | 67.744 % |
c |      8784 |   59717   126548 |   21972    5399    58896    10.9 | 71.774 % |
c |      8934 |   58834   124460 |   24169    5359    59700    11.1 | 73.035 % |
c |      9159 |   58810   124405 |   26586    5572    65704    11.8 | 73.063 % |
c |      9497 |   57937   122355 |   29245    5596    66758    11.9 | 74.319 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9678 |   58071   122709 |   19357    5775    75106    13.0 | 74.319 % |
c |      9779 |   57952   122433 |   21292    5858    75518    12.9 | 74.462 % |
c |      9930 |   57561   121520 |   23421    5917    76276    12.9 | 75.009 % |
c |     10155 |   57507   121393 |   25764    6126    79204    12.9 | 75.086 % |
c |     10493 |   57229   120745 |   28340    6381    83253    13.0 | 75.467 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10588 |   57021   120244 |   19007    6377    80832    12.7 | 75.467 % |
c |     10688 |   56416   118826 |   20907    6375    80737    12.7 | 76.607 % |
c |     10838 |   56273   118489 |   22998    6469    84482    13.1 | 76.820 % |
c |     11063 |   56112   118112 |   25298    6638    95072    14.3 | 77.046 % |
c |     11400 |   56015   117884 |   27828    6958   100616    14.5 | 77.186 % |
c |     11906 |   54512   114370 |   30610    7049   109304    15.5 | 79.285 % |
c |     12665 |   54094   113376 |   33672    7646   133226    17.4 | 79.880 % |
c |     13804 |   54066   113310 |   37039    8761   269338    30.7 | 79.920 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13904 |   53977   113117 |   17992    8839   270483    30.6 | 79.920 % |
c |     14006 |   53626   112292 |   19791    8825   271119    30.7 | 80.553 % |
c |     14156 |   53626   112292 |   21770    8975   274848    30.6 | 80.553 % |
c |     14381 |   53340   111614 |   23947    9083   276558    30.4 | 80.959 % |
c |     14718 |   53073   110984 |   26342    9300   291976    31.4 | 81.341 % |
c |     15224 |   53073   110984 |   28976    9806   306959    31.3 | 81.341 % |
c |     15983 |   52995   110800 |   31873   10501   332445    31.7 | 81.453 % |
c |     17122 |   52834   110421 |   35061   11592   384963    33.2 | 81.670 % |
c |     18830 |   52399   109396 |   38567   13016   532809    40.9 | 82.297 % |
c |     21392 |   52014   108497 |   42424   15235   727929    47.8 | 82.835 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23086 |   51961   108345 |   17320   16882   892046    52.8 | 82.835 % |
c |     23186 |   51639   107591 |   19052   16815   891648    53.0 | 83.346 % |
c |     23336 |   51631   107572 |   20957   16959   897926    52.9 | 83.358 % |
c |     23561 |   51627   107563 |   23052   17181   913929    53.2 | 83.362 % |
c |     23898 |   51627   107563 |   25358   17518   931032    53.1 | 83.362 % |
c |     24404 |   51576   107443 |   27894   18013   962074    53.4 | 83.438 % |
c |     25163 |   51220   106609 |   30683   18598  1034018    55.6 | 83.944 % |
c |     26302 |   51220   106609 |   33751   19737  1127263    57.1 | 83.944 % |
c |     28010 |   51220   106609 |   37126   21445  1269282    59.2 | 83.944 % |
c |     30575 |   51063   106239 |   40839   23865  1499687    62.8 | 84.177 % |
c |     34422 |   51063   106239 |   44923   27712  1968592    71.0 | 84.177 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39501 |   51108   106355 |   17036   32768  2492600    76.1 | 84.177 % |
c |     39601 |   51108   106355 |   18739   32868  2499508    76.0 | 84.190 % |
c |     39751 |   50935   105947 |   20613   32769  2504409    76.4 | 84.442 % |
c |     39977 |   50935   105947 |   22674   32995  2509913    76.1 | 84.442 % |
c |     40314 |   50919   105909 |   24942   33314  2519183    75.6 | 84.466 % |
c |     40821 |   50919   105909 |   27436   33821  2550251    75.4 | 84.466 % |
c |     41580 |   50919   105909 |   30180   34580  2616677    75.7 | 84.466 % |
c |     42719 |   50788   105600 |   33198   35480  2696682    76.0 | 84.658 % |
c |     44427 |   50361   104591 |   36518   36788  2850320    77.5 | 85.258 % |
c |     46990 |   50361   104591 |   40169   39351  3071874    78.1 | 85.258 % |
c |     50834 |   50355   104577 |   44186   43193  3349224    77.5 | 85.266 % |
c |     56600 |   50339   104540 |   48605   48908  3855600    78.8 | 85.286 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59116 |   50310   104455 |   16770   51310  4121623    80.3 | 85.286 % |
c |     59216 |   50310   104455 |   18447   17862  1088071    60.9 | 85.323 % |
c |     59367 |   50310   104455 |   20291   18013  1095272    60.8 | 85.323 % |
c |     59594 |   50310   104455 |   22320   18240  1111088    60.9 | 85.323 % |
c |     59931 |   50310   104455 |   24552   18577  1128881    60.8 | 85.323 % |
c |     60438 |   50310   104455 |   27008   19084  1170627    61.3 | 85.323 % |
c |     61197 |   50310   104455 |   29709   19843  1228709    61.9 | 85.323 % |
c |     62336 |   50288   104403 |   32679   20967  1337417    63.8 | 85.355 % |
c |     64044 |   50288   104403 |   35947   22675  1473387    65.0 | 85.355 % |
c |     66606 |   50288   104403 |   39542   25237  1630287    64.6 | 85.355 % |
c |     70450 |   50194   104183 |   43497   29068  1991929    68.5 | 85.491 % |
c |     76216 |   50184   104160 |   47846   34820  2451276    70.4 | 85.503 % |
c |     84865 |   50160   104104 |   52631   43460  3215274    74.0 | 85.535 % |
c |     97839 |   50144   104067 |   57894   56422  4185181    74.2 | 85.555 % |
c |    117301 |   50138   104053 |   63684   75881  5887550    77.6 | 85.563 % |
c |    146496 |   50120   104011 |   70052   37073  2543119    68.6 | 85.587 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    180389 |   50160   104109 |   16720   70966  4407132    62.1 | 85.587 % |
c |    180489 |   50160   104109 |   18392   18866   656634    34.8 | 85.551 % |
c |    180639 |   50160   104109 |   20231   19016   666724    35.1 | 85.551 % |
c |    180865 |   50160   104109 |   22254   19242   680375    35.4 | 85.551 % |
c |    181202 |   50160   104109 |   24479   19579   699513    35.7 | 85.551 % |
c |    181708 |   50160   104109 |   26927   20085   731828    36.4 | 85.551 % |
c |    182468 |   50160   104109 |   29620   20845   781374    37.5 | 85.551 % |
c |    183607 |   50160   104109 |   32582   21984   859673    39.1 | 85.551 % |
c |    185315 |   50150   104086 |   35840   23686   967002    40.8 | 85.563 % |
c |    187878 |   50150   104086 |   39424   26249  1206035    45.9 | 85.563 % |
c |    191722 |   50150   104086 |   43367   30093  1512890    50.3 | 85.563 % |
c |    197488 |   50150   104086 |   47704   35859  1937635    54.0 | 85.563 % |
c |    206137 |   50140   104063 |   52474   44498  2550675    57.3 | 85.575 % |
c |    219111 |   50042   103831 |   57721   57447  3871085    67.4 | 85.719 % |
c |    238572 |   50042   103831 |   63494   76908  5526315    71.9 | 85.719 % |
c |    267764 |   49922   103548 |   69843   40014  1738239    43.4 | 85.899 % |
c |    311554 |   49922   103548 |   76827   83804  3486731    41.6 | 85.899 % |
c ==============================================================================
c [1mFound solution: -38[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 |    352547 |   49883   103433 |   16627   46715  1468423    31.4 | 85.899 % |
c |    352647 |   49883   103433 |   18289   19372   512918    26.5 | 85.948 % |
c |    352797 |   49883   103433 |   20118   19522   516594    26.5 | 85.948 % |
c |    353022 |   49883   103433 |   22130   19747   522950    26.5 | 85.948 % |
c |    353359 |   49883   103433 |   24343   20084   532706    26.5 | 85.948 % |
c |    353865 |   49883   103433 |   26777   20590   548672    26.6 | 85.948 % |
c |    354624 |   49883   103433 |   29455   21349   570868    26.7 | 85.948 % |
c |    355765 |   49883   103433 |   32401   22490   602676    26.8 | 85.948 % |
c |    357473 |   49883   103433 |   35641   24198   676840    28.0 | 85.948 % |
c |    360036 |   49859   103376 |   39205   26755   797257    29.8 | 85.984 % |
c |    363883 |   49859   103376 |   43126   30602  1038171    33.9 | 85.984 % |
c |    369650 |   49859   103376 |   47438   36369  1379264    37.9 | 85.984 % |
c |    378299 |   49853   103362 |   52182   45014  1962461    43.6 | 85.992 % |
c |    391273 |   49853   103362 |   57400   57988  3002937    51.8 | 85.992 % |
c |    410735 |   49853   103362 |   63141   77450  3726766    48.1 | 85.992 % |
c |    439927 |   49829   103305 |   69455   40973  1719354    42.0 | 86.028 % |
c |    483716 |   49829   103305 |   76400   84762  3624993    42.8 | 86.028 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 C137 -C136 -C135 -C134 -C133 -C132 -C131 C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 C83 -C82 -C81 -C80 -C79 -C78 -C77 C76 -C75 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 1884
Raw data (stat): 1884 (runsolver) R 1883 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 410012501 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 3110 0 0 0 989 9 0 0 25 0 1 0 410012501 15036416 3088 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3671 3088 603 41 0 3630 0
vsize: 14684
[startup+20.0019 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 3111 0 0 0 1988 9 0 0 25 0 1 0 410012501 15036416 3089 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3671 3089 603 41 0 3630 0
vsize: 14684
[startup+30.002 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 3111 0 0 0 2988 9 0 0 25 0 1 0 410012501 15036416 3089 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3671 3089 603 41 0 3630 0
vsize: 14684
[startup+40.0028 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 3325 0 0 0 3988 9 0 0 25 0 1 0 410012501 15974400 3303 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3900 3303 603 41 0 3859 0
vsize: 15600
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 3944 0 0 0 4986 11 0 0 25 0 1 0 410012501 18563072 3922 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4532 3922 603 41 0 4491 0
vsize: 18128
[startup+60.0036 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 4528 0 0 0 5984 13 0 0 25 0 1 0 410012501 20930560 4506 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5110 4506 603 41 0 5069 0
vsize: 20440
[startup+70.0041 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 5193 0 0 0 6980 16 0 0 25 0 1 0 410012501 23617536 5171 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5766 5171 603 41 0 5725 0
vsize: 23064
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 5744 0 0 0 7979 18 0 0 25 0 1 0 410012501 26009600 5722 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6350 5722 603 41 0 6309 0
vsize: 25400
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 6127 0 0 0 8978 19 0 0 25 0 1 0 410012501 27627520 6105 4294967295 134512640 134672761 3221224560 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6745 6105 603 41 0 6704 0
vsize: 26980
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 6593 0 0 0 9977 20 0 0 25 0 1 0 410012501 29487104 6571 4294967295 134512640 134672761 3221224560 3221223696 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7199 6571 603 41 0 7158 0
vsize: 28796
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 6981 0 0 0 10977 21 0 0 25 0 1 0 410012501 31092736 6959 4294967295 134512640 134672761 3221224560 3221223744 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7591 6959 603 41 0 7550 0
vsize: 30364
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7438 0 0 0 11976 22 0 0 25 0 1 0 410012501 32829440 7416 4294967295 134512640 134672761 3221224560 3221223664 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7416 603 41 0 7974 0
vsize: 32060
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7554 0 0 0 12976 22 0 0 25 0 1 0 410012501 33316864 7532 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7532 603 41 0 8093 0
vsize: 32536
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7554 0 0 0 13976 22 0 0 25 0 1 0 410012501 33316864 7532 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7532 603 41 0 8093 0
vsize: 32536
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7554 0 0 0 14976 22 0 0 25 0 1 0 410012501 33316864 7532 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7532 603 41 0 8093 0
vsize: 32536
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7554 0 0 0 15976 22 0 0 25 0 1 0 410012501 33316864 7532 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7532 603 41 0 8093 0
vsize: 32536
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7554 0 0 0 16976 22 0 0 25 0 1 0 410012501 33316864 7532 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7532 603 41 0 8093 0
vsize: 32536
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7554 0 0 0 17976 22 0 0 25 0 1 0 410012501 33316864 7532 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7532 603 41 0 8093 0
vsize: 32536
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7555 0 0 0 18977 22 0 0 25 0 1 0 410012501 33316864 7533 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 7533 603 41 0 8093 0
vsize: 32536
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 7789 0 0 0 19976 23 0 0 25 0 1 0 410012501 34250752 7767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8362 7767 603 41 0 8321 0
vsize: 33448
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 8118 0 0 0 20975 24 0 0 25 0 1 0 410012501 35581952 8096 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8687 8096 603 41 0 8646 0
vsize: 34748
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 8394 0 0 0 21974 25 0 0 25 0 1 0 410012501 36786176 8372 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8372 603 41 0 8940 0
vsize: 35924
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 8762 0 0 0 22973 26 0 0 25 0 1 0 410012501 38510592 8740 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9402 8740 603 41 0 9361 0
vsize: 37608
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 9101 0 0 0 23972 28 0 0 25 0 1 0 410012501 39841792 9079 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9727 9079 603 41 0 9686 0
vsize: 38908
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 9427 0 0 0 24972 28 0 0 25 0 1 0 410012501 41168896 9405 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10051 9405 603 41 0 10010 0
vsize: 40204
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 9757 0 0 0 25971 29 0 0 25 0 1 0 410012501 42504192 9735 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10377 9735 603 41 0 10336 0
vsize: 41508
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10058 0 0 0 26970 30 0 0 25 0 1 0 410012501 43843584 10036 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10704 10036 603 41 0 10663 0
vsize: 42816
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10312 0 0 0 27970 30 0 0 25 0 1 0 410012501 44777472 10290 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10932 10290 603 41 0 10891 0
vsize: 43728
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10566 0 0 0 28970 31 0 0 25 0 1 0 410012501 45838336 10544 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11191 10544 603 41 0 11150 0
vsize: 44764
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10597 0 0 0 29970 31 0 0 25 0 1 0 410012501 45973504 10575 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10575 603 41 0 11183 0
vsize: 44896
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10597 0 0 0 30970 31 0 0 25 0 1 0 410012501 45973504 10575 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10575 603 41 0 11183 0
vsize: 44896
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10597 0 0 0 31971 31 0 0 25 0 1 0 410012501 45973504 10575 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10575 603 41 0 11183 0
vsize: 44896
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 32971 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 33971 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 34971 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 35971 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 36972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 37972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 38972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 39972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 40972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 41973 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 42973 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 43973 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 44972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 45972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10598 0 0 0 46972 31 0 0 25 0 1 0 410012501 45973504 10576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10576 603 41 0 11183 0
vsize: 44896
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10599 0 0 0 47972 31 0 0 25 0 1 0 410012501 45973504 10577 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10577 603 41 0 11183 0
vsize: 44896
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10599 0 0 0 48973 31 0 0 25 0 1 0 410012501 45973504 10577 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10577 603 41 0 11183 0
vsize: 44896
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10600 0 0 0 49973 31 0 0 25 0 1 0 410012501 45973504 10578 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10578 603 41 0 11183 0
vsize: 44896
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 50973 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 51973 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 52973 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 53974 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 54974 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 55974 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 56974 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 57974 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 58974 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 59975 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 60975 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 61975 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 62975 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 63975 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 64976 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223696 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 65976 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 66976 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 67976 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 68977 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 69977 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10601 0 0 0 70977 31 0 0 25 0 1 0 410012501 45973504 10579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10579 603 41 0 11183 0
vsize: 44896
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10602 0 0 0 71977 31 0 0 25 0 1 0 410012501 45973504 10580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10580 603 41 0 11183 0
vsize: 44896
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10602 0 0 0 72977 31 0 0 25 0 1 0 410012501 45973504 10580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10580 603 41 0 11183 0
vsize: 44896
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10602 0 0 0 73977 31 0 0 25 0 1 0 410012501 45973504 10580 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10580 603 41 0 11183 0
vsize: 44896
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10602 0 0 0 74977 31 0 0 25 0 1 0 410012501 45973504 10580 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10580 603 41 0 11183 0
vsize: 44896
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10604 0 0 0 75977 31 0 0 25 0 1 0 410012501 45973504 10582 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10582 603 41 0 11183 0
vsize: 44896
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10606 0 0 0 76978 31 0 0 25 0 1 0 410012501 45973504 10584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10584 603 41 0 11183 0
vsize: 44896
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10609 0 0 0 77978 31 0 0 25 0 1 0 410012501 45973504 10587 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10587 603 41 0 11183 0
vsize: 44896
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10611 0 0 0 78978 31 0 0 25 0 1 0 410012501 45973504 10589 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10589 603 41 0 11183 0
vsize: 44896
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 79978 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 80978 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 81979 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 82979 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 83979 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 84979 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 85979 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 86979 31 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223744 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 87979 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 88978 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 89978 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+910.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 90978 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 91978 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 92978 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 93979 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 94979 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 95979 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 96979 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 97980 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 98980 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 99980 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 100980 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 101980 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1884
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 102981 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1885
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 103981 32 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1050.04 s]
Raw data (loadavg): 1.07 0.99 0.91 2/58 1927
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 104978 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1060.04 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 1937
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 105978 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1070.04 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 1937
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 106979 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1080.04 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 1937
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 107979 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1090.04 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 1937
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 108979 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1100.04 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 1937
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 109979 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1110.04 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 1937
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 110979 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1120.04 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 111980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1130.04 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 112980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1140.04 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 113980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1150.04 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 114980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1160.04 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 115980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1170.04 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 116980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1180.04 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 117980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1190.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 118980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
[startup+1200.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1939
Raw data (stat): 1884 (minisat+) R 1883 26667 26666 0 -1 0 10614 0 0 0 119980 34 0 0 25 0 1 0 410012501 45973504 10592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10592 603 41 0 11183 0
vsize: 44896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 1939
Raw data (stat): 1884 (minisat+) Z 1883 26667 26666 0 -1 12 10617 0 0 0 119981 36 0 0 25 0 1 0 410012501 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.18
CPU user time (s): 1199.81
CPU system time (s): 0.366944
CPU usage (%): 100.009
Max. virtual memory (Kb): 44896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####