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/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	c8b965306fec2c21edee64824d12f378
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 21394

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        199560 kB
Buffers:         34528 kB
Cached:         771932 kB
SwapCached:         20 kB
Active:         198176 kB
Inactive:       610960 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        199308 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            20312 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:59:51 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 13517 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> Adder-cost: 304   maxlim: 3240959   bits: 23/22
c ---[   8]---> Adder-cost: 314   maxlim: 3453951   bits: 23/22
c ---[   6]---> Adder-cost: 348   maxlim: 3482623   bits: 23/22
c ---[   4]---> Adder-cost: 318   maxlim: 3294207   bits: 23/22
c ---[   2]---> Adder-cost: 312   maxlim: 3286015   bits: 23/22
c ---[   0]---> Adder-cost: 314   maxlim: 3289087   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12820    45524 |    4273       0        0     nan |  0.000 % |
c |       100 |   12820    45524 |    4700     100      594     5.9 | 14.261 % |
c ==============================================================================
c [1mFound solution: 4615168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 110   maxlim: 7775   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       141 |   13530    48047 |    4510     141     1027     7.3 | 14.261 % |
c |       241 |   13530    48047 |    4961     241    10551    43.8 | 13.848 % |
c |       391 |   13530    48047 |    5457     391    26628    68.1 | 13.848 % |
c ==============================================================================
c [1mFound solution: 4451328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7935   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |   13531    48054 |    4510     543    37699    69.4 | 13.848 % |
c |       643 |   13531    48054 |    4961     643    51023    79.4 | 13.884 % |
c ==============================================================================
c [1mFound solution: 4440064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7946   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       697 |   13554    48177 |    4518     696    53533    76.9 | 13.884 % |
c |       798 |   13554    48177 |    4969     797    61190    76.8 | 14.005 % |
c ==============================================================================
c [1mFound solution: 4252672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8129   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       821 |   13561    48224 |    4520     820    62616    76.4 | 14.005 % |
c ==============================================================================
c [1mFound solution: 4208640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8172   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       831 |   13571    48296 |    4523     830    63428    76.4 | 14.005 % |
c ==============================================================================
c [1mFound solution: 3886080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8487   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       833 |   13546    48127 |    4515     832    63542    76.4 | 14.005 % |
c ==============================================================================
c [1mFound solution: 3854336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8518   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       917 |   13550    48170 |    4516     916    70229    76.7 | 14.005 % |
c |      1019 |   13550    48170 |    4967    1018    80774    79.3 | 14.666 % |
c |      1170 |   13550    48170 |    5464    1169    94999    81.3 | 14.666 % |
c |      1395 |   13550    48170 |    6010    1394   107700    77.3 | 14.666 % |
c ==============================================================================
c [1mFound solution: 3727360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8642   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1604 |   13541    48162 |    4513    1601   110127    68.8 | 14.666 % |
c ==============================================================================
c [1mFound solution: 3437568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8925   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1650 |   13552    48237 |    4517    1647   111474    67.7 | 14.666 % |
c |      1751 |   13552    48237 |    4968    1748   115080    65.8 | 15.118 % |
c |      1903 |   13536    48185 |    5465    1898   125446    66.1 | 15.200 % |
c |      2128 |   13536    48185 |    6012    2123   136831    64.5 | 15.200 % |
c |      2467 |   13536    48185 |    6613    2462   158186    64.3 | 15.200 % |
c |      2974 |   13530    48167 |    7274    2968   179281    60.4 | 15.242 % |
c |      3733 |   13530    48167 |    8002    3727   252187    67.7 | 15.242 % |
c ==============================================================================
c [1mFound solution: 3383296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8978   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4363 |   13528    48183 |    4509    4356   299872    68.8 | 15.242 % |
c |      4463 |   13528    48183 |    4959    4456   306852    68.9 | 15.410 % |
c |      4613 |   13528    48183 |    5455    4606   320504    69.6 | 15.410 % |
c |      4838 |   13528    48183 |    6001    4831   328970    68.1 | 15.410 % |
c |      5175 |   13528    48183 |    6601    5168   348729    67.5 | 15.410 % |
c |      5681 |   13528    48183 |    7261    5674   397146    70.0 | 15.410 % |
c ==============================================================================
c [1mFound solution: 1483776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10833   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5719 |   13509    48008 |    4503    5712   397801    69.6 | 15.410 % |
c |      5819 |   13494    47955 |    4953    2954   175354    59.4 | 15.688 % |
c |      5969 |   13494    47955 |    5448    3104   181479    58.5 | 15.688 % |
c |      6194 |   13485    47926 |    5993    3328   188021    56.5 | 15.770 % |
c |      6531 |   13476    47897 |    6592    3664   212311    57.9 | 15.852 % |
c |      7039 |   13476    47897 |    7252    4172   246404    59.1 | 15.852 % |
c |      7798 |   13476    47897 |    7977    4931   292836    59.4 | 15.852 % |
c |      8937 |   13476    47897 |    8775    6070   352287    58.0 | 15.852 % |
c ==============================================================================
c [1mFound solution: 927744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4   maxlim: 5232   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9673 |   13411    47683 |    4470    6327   303187    47.9 | 15.852 % |
c |      9773 |   13384    47590 |    4917    3249   122154    37.6 | 16.680 % |
c |      9923 |   13384    47590 |    5408    3399   128458    37.8 | 16.680 % |
c |     10151 |   13384    47590 |    5949    3627   132423    36.5 | 16.680 % |
c |     10488 |   13364    47508 |    6544    3961   144082    36.4 | 16.844 % |
c |     10997 |   13364    47508 |    7198    4470   167186    37.4 | 16.844 % |
c |     11756 |   13364    47508 |    7918    5229   211751    40.5 | 16.844 % |
c |     12895 |   13364    47508 |    8710    6368   264424    41.5 | 16.844 % |
c |     14604 |   13364    47508 |    9581    8077   327632    40.6 | 16.844 % |
c |     17168 |   13364    47508 |   10540    5402   170299    31.5 | 16.844 % |
c |     21013 |   13356    47482 |   11594    9246   322961    34.9 | 16.885 % |
c |     26779 |   13356    47482 |   12753    8878   354009    39.9 | 16.885 % |
c ==============================================================================
c [1mFound solution: 903168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5256   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27249 |   13355    47491 |    4451    9347   366285    39.2 | 16.885 % |
c |     27349 |   13355    47491 |    4896    4774   154490    32.4 | 17.013 % |
c |     27499 |   13355    47491 |    5385    4924   158418    32.2 | 17.013 % |
c |     27725 |   13355    47491 |    5924    5150   165179    32.1 | 17.013 % |
c |     28062 |   13355    47491 |    6516    5487   177942    32.4 | 17.013 % |
c |     28568 |   13355    47491 |    7168    5993   214401    35.8 | 17.013 % |
c |     29328 |   13355    47491 |    7885    6753   237395    35.2 | 17.013 % |
c |     30467 |   13355    47491 |    8673    7892   276790    35.1 | 17.013 % |
c |     32175 |   13355    47491 |    9541    4859   147414    30.3 | 17.013 % |
c |     34737 |   13355    47491 |   10495    7421   288843    38.9 | 17.013 % |
c |     38581 |   13355    47491 |   11544    5669   168162    29.7 | 17.013 % |
c |     44347 |   13355    47491 |   12699   11435   459721    40.2 | 17.013 % |
c |     52997 |   13355    47491 |   13969   13287   578129    43.5 | 17.013 % |
c |     65971 |   13355    47491 |   15366   11480   521835    45.5 | 17.013 % |
c |     85433 |   13347    47465 |   16902   14916   611237    41.0 | 17.054 % |
c ==============================================================================
c [1mFound solution: 882688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5276   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87954 |   13347    47486 |    4449   17436   712189    40.8 | 17.054 % |
c |     88054 |   13347    47486 |    4893    4459   127533    28.6 | 17.243 % |
c |     88204 |   13347    47486 |    5383    4609   131398    28.5 | 17.243 % |
c |     88429 |   13347    47486 |    5921    4834   140062    29.0 | 17.243 % |
c |     88767 |   13347    47486 |    6513    5172   147960    28.6 | 17.243 % |
c |     89274 |   13347    47486 |    7165    5679   164313    28.9 | 17.243 % |
c |     90033 |   13347    47486 |    7881    6438   189471    29.4 | 17.243 % |
c |     91173 |   13347    47486 |    8669    7578   231147    30.5 | 17.243 % |
c |     92881 |   13347    47486 |    9536    9286   299139    32.2 | 17.243 % |
c |     95444 |   13347    47486 |   10490    6595   232398    35.2 | 17.243 % |
c |     99290 |   13347    47486 |   11539   10441   370636    35.5 | 17.243 % |
c |    105056 |   13347    47486 |   12693   10042   474029    47.2 | 17.243 % |
c ==============================================================================
c [1mFound solution: 858112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5300   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113494 |   13344    47495 |    4448   11758   493407    42.0 | 17.243 % |
c |    113595 |   13344    47495 |    4892    3041    90912    29.9 | 17.411 % |
c |    113746 |   13344    47495 |    5382    3192    95378    29.9 | 17.411 % |
c |    113971 |   13344    47495 |    5920    3417    99422    29.1 | 17.411 % |
c |    114309 |   13344    47495 |    6512    3755   109697    29.2 | 17.411 % |
c |    114818 |   13344    47495 |    7163    4264   126350    29.6 | 17.411 % |
c |    115577 |   13344    47495 |    7879    5023   155249    30.9 | 17.411 % |
c |    116717 |   13344    47495 |    8667    6163   186944    30.3 | 17.411 % |
c |    118428 |   13344    47495 |    9534    7874   256826    32.6 | 17.411 % |
c |    120991 |   13344    47495 |   10488    5237   154424    29.5 | 17.411 % |
c |    124836 |   13344    47495 |   11536    9082   295207    32.5 | 17.411 % |
c |    130602 |   13344    47495 |   12690    8760   316223    36.1 | 17.411 % |
c |    139251 |   13344    47495 |   13959   10694   416323    38.9 | 17.411 % |
c ==============================================================================
c [1mFound solution: 804864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5352   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139760 |   13352    47531 |    4450   11203   429990    38.4 | 17.411 % |
c |    139860 |   13352    47531 |    4895    2901    69400    23.9 | 17.516 % |
c |    140011 |   13352    47531 |    5384    3052    73400    24.0 | 17.516 % |
c |    140237 |   13352    47531 |    5922    3278    79590    24.3 | 17.516 % |
c |    140574 |   13352    47531 |    6515    3615    87691    24.3 | 17.516 % |
c |    141080 |   13352    47531 |    7166    4121   103617    25.1 | 17.516 % |
c |    141839 |   13352    47531 |    7883    4880   129239    26.5 | 17.516 % |
c |    142981 |   13352    47531 |    8671    6022   159801    26.5 | 17.516 % |
c |    144689 |   13352    47531 |    9538    7730   219162    28.4 | 17.516 % |
c |    147254 |   13352    47531 |   10492    5167   175302    33.9 | 17.516 % |
c |    151098 |   13352    47531 |   11542    9011   310621    34.5 | 17.516 % |
c |    156864 |   13352    47531 |   12696    8600   309753    36.0 | 17.516 % |
c |    165513 |   13344    47505 |   13966   10520   383759    36.5 | 17.557 % |
c |    178487 |   13336    47479 |   15362    8719   325619    37.3 | 17.597 % |
c |    197952 |   13336    47479 |   16898   11995   546454    45.6 | 17.597 % |
c ==============================================================================
c [1mFound solution: 777216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5379   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225463 |   13339    47493 |    4446   12756   758258    59.4 | 17.597 % |
c |    225563 |   13339    47493 |    4890    3289   125236    38.1 | 17.657 % |
c |    225714 |   13339    47493 |    5379    3440   130923    38.1 | 17.657 % |
c |    225941 |   13339    47493 |    5917    3667   138975    37.9 | 17.657 % |
c |    226278 |   13339    47493 |    6509    4004   148650    37.1 | 17.657 % |
c |    226784 |   13339    47493 |    7160    4510   169570    37.6 | 17.657 % |
c |    227544 |   13339    47493 |    7876    5270   196710    37.3 | 17.657 % |
c |    228685 |   13339    47493 |    8663    6411   241027    37.6 | 17.657 % |
c |    230393 |   13339    47493 |    9530    8119   305665    37.6 | 17.657 % |
c |    232955 |   13339    47493 |   10483    5482   186331    34.0 | 17.657 % |
c |    236799 |   13339    47493 |   11531    9326   341455    36.6 | 17.657 % |
c |    242566 |   13339    47493 |   12684    9040   301421    33.3 | 17.657 % |
c |    251215 |   13339    47493 |   13953   10994   518003    47.1 | 17.657 % |
c |    264191 |   13339    47493 |   15348    9237   371491    40.2 | 17.657 % |
c |    283653 |   13339    47493 |   16883   12634   507143    40.1 | 17.657 % |
c |    312846 |   13339    47493 |   18572   15231   683793    44.9 | 17.657 % |
c ==============================================================================
c [1mFound solution: 686080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5468   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    319011 |   13349    47537 |    4449   11744   568430    48.4 | 17.657 % |
c |    319112 |   13349    47537 |    4893    3037   106777    35.2 | 17.787 % |
c |    319262 |   13349    47537 |    5383    3187   108078    33.9 | 17.787 % |
c |    319487 |   13349    47537 |    5921    3412   111411    32.7 | 17.787 % |
c |    319824 |   13349    47537 |    6513    3749   117788    31.4 | 17.787 % |
c |    320333 |   13349    47537 |    7165    4258   126307    29.7 | 17.787 % |
c |    321092 |   13349    47537 |    7881    5017   139976    27.9 | 17.787 % |
c |    322231 |   13349    47537 |    8669    6156   175471    28.5 | 17.787 % |
c |    323940 |   13349    47537 |    9536    7865   249752    31.8 | 17.787 % |
c |    326502 |   13349    47537 |   10490    5264   176857    33.6 | 17.787 % |
c |    330348 |   13349    47537 |   11539    9110   329613    36.2 | 17.787 % |
c |    336115 |   13349    47537 |   12693    8801   313362    35.6 | 17.787 % |
c |    344765 |   13349    47537 |   13962   10757   436205    40.6 | 17.787 % |
c |    357739 |   13349    47537 |   15359    8973   349043    38.9 | 17.787 % |
c |    377200 |   13349    47537 |   16895   12379   488048    39.4 | 17.787 % |
c |    406392 |   13349    47537 |   18584   15136   610751    40.4 | 17.787 % |
c |    450182 |   13349    47537 |   20443   11000   456954    41.5 | 17.787 % |
c |    515867 |   13349    47537 |   22487   12981   594905    45.8 | 17.787 % |
c |    614393 |   13349    47537 |   24736   18384   763506    41.5 | 17.787 % |
c |    762182 |   13349    47537 |   27209   12886   488584    37.9 | 17.787 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 13504
Raw data (stat): 13504 (runsolver) R 13503 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549108246 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99979 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1038 0 0 0 996 2 0 0 25 0 1 0 549108246 5865472 1016 4294967295 134512640 134672761 3221224528 3221223792 134562178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1016 603 41 0 1391 0
vsize: 5728
[startup+20.0015 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1132 0 0 0 1995 2 0 0 25 0 1 0 549108246 6303744 1110 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1539 1110 603 41 0 1498 0
vsize: 6156
[startup+30.0018 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1205 0 0 0 2994 3 0 0 25 0 1 0 549108246 6574080 1183 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1605 1183 603 41 0 1564 0
vsize: 6420
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1352 0 0 0 3993 3 0 0 25 0 1 0 549108246 7241728 1330 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1330 603 41 0 1727 0
vsize: 7072
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1467 0 0 0 4993 4 0 0 25 0 1 0 549108246 7647232 1445 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1867 1445 603 41 0 1826 0
vsize: 7468
[startup+60.0016 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1467 0 0 0 5993 4 0 0 25 0 1 0 549108246 7647232 1445 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1867 1445 603 41 0 1826 0
vsize: 7468
[startup+70.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1572 0 0 0 6993 4 0 0 25 0 1 0 549108246 8048640 1550 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1550 603 41 0 1924 0
vsize: 7860
[startup+80.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1574 0 0 0 7993 4 0 0 25 0 1 0 549108246 8048640 1552 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1552 603 41 0 1924 0
vsize: 7860
[startup+90.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1617 0 0 0 8993 4 0 0 25 0 1 0 549108246 8286208 1595 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1595 603 41 0 1982 0
vsize: 8092
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1617 0 0 0 9993 4 0 0 25 0 1 0 549108246 8286208 1595 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1595 603 41 0 1982 0
vsize: 8092
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1618 0 0 0 10993 4 0 0 25 0 1 0 549108246 8286208 1596 4294967295 134512640 134672761 3221224528 3221223712 134558678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+120.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1618 0 0 0 11993 4 0 0 25 0 1 0 549108246 8286208 1596 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+130.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1618 0 0 0 12993 5 0 0 25 0 1 0 549108246 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+140.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1618 0 0 0 13993 5 0 0 25 0 1 0 549108246 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+150.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1618 0 0 0 14994 5 0 0 25 0 1 0 549108246 8286208 1596 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1618 0 0 0 15993 5 0 0 25 0 1 0 549108246 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1734 0 0 0 16993 6 0 0 25 0 1 0 549108246 8814592 1712 4294967295 134512640 134672761 3221224528 3221223652 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2152 1712 603 41 0 2111 0
vsize: 8608
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1846 0 0 0 17993 6 0 0 25 0 1 0 549108246 9216000 1824 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1824 603 41 0 2209 0
vsize: 9000
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 1960 0 0 0 18992 7 0 0 25 0 1 0 549108246 9744384 1938 4294967295 134512640 134672761 3221224528 3221223664 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2379 1938 603 41 0 2338 0
vsize: 9516
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2033 0 0 0 19992 7 0 0 25 0 1 0 549108246 10010624 2011 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 2011 603 41 0 2403 0
vsize: 9776
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2144 0 0 0 20991 8 0 0 25 0 1 0 549108246 10534912 2122 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2122 603 41 0 2531 0
vsize: 10288
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 21991 8 0 0 25 0 1 0 549108246 10665984 2154 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2604 2154 603 41 0 2563 0
vsize: 10416
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 22992 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 23993 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+250.018 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 24993 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+260.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 25993 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+270.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 26994 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223744 134558226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+280.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 27994 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+290.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 28994 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+300.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 29994 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+310.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 30994 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+320.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2176 0 0 0 31994 8 0 0 25 0 1 0 549108246 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+330.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 32994 8 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+340.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 33994 8 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+350.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 34994 8 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+360.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 35995 9 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+370.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 36995 9 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+380.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 37995 9 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+390.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 38995 9 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+400.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 39995 9 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+410.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2190 0 0 0 40996 9 0 0 25 0 1 0 549108246 10657792 2168 4294967295 134512640 134672761 3221224528 3221223712 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+420.022 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2195 0 0 0 41996 9 0 0 25 0 1 0 549108246 10657792 2173 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2173 603 41 0 2561 0
vsize: 10408
[startup+430.022 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2213 0 0 0 42996 9 0 0 25 0 1 0 549108246 10805248 2191 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2638 2191 603 41 0 2597 0
vsize: 10552
[startup+440.022 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2301 0 0 0 43996 9 0 0 25 0 1 0 549108246 11075584 2279 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2704 2279 603 41 0 2663 0
vsize: 10816
[startup+450.022 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2307 0 0 0 44996 9 0 0 25 0 1 0 549108246 11218944 2285 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2739 2285 603 41 0 2698 0
vsize: 10956
[startup+460.023 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2320 0 0 0 45996 9 0 0 25 0 1 0 549108246 11218944 2298 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2739 2298 603 41 0 2698 0
vsize: 10956
[startup+470.023 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2323 0 0 0 46996 9 0 0 25 0 1 0 549108246 11218944 2301 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2739 2301 603 41 0 2698 0
vsize: 10956
[startup+480.022 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2414 0 0 0 47996 9 0 0 25 0 1 0 549108246 11616256 2392 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2836 2392 603 41 0 2795 0
vsize: 11344
[startup+490.022 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2484 0 0 0 48996 10 0 0 25 0 1 0 549108246 11882496 2462 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2901 2462 603 41 0 2860 0
vsize: 11604
[startup+500.023 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2518 0 0 0 49996 10 0 0 25 0 1 0 549108246 12017664 2496 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2934 2496 603 41 0 2893 0
vsize: 11736
[startup+510.022 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2588 0 0 0 50996 10 0 0 25 0 1 0 549108246 12279808 2566 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2998 2566 603 41 0 2957 0
vsize: 11992
[startup+520.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2593 0 0 0 51997 10 0 0 25 0 1 0 549108246 12279808 2571 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2998 2571 603 41 0 2957 0
vsize: 11992
[startup+530.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2605 0 0 0 52997 10 0 0 25 0 1 0 549108246 12414976 2583 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3031 2583 603 41 0 2990 0
vsize: 12124
[startup+540.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2611 0 0 0 53997 10 0 0 25 0 1 0 549108246 12414976 2589 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3031 2589 603 41 0 2990 0
vsize: 12124
[startup+550.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2614 0 0 0 54997 10 0 0 25 0 1 0 549108246 12414976 2592 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3031 2592 603 41 0 2990 0
vsize: 12124
[startup+560.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2638 0 0 0 55997 10 0 0 25 0 1 0 549108246 12546048 2616 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2616 603 41 0 3022 0
vsize: 12252
[startup+570.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2645 0 0 0 56997 10 0 0 25 0 1 0 549108246 12546048 2623 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2623 603 41 0 3022 0
vsize: 12252
[startup+580.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2651 0 0 0 57998 10 0 0 25 0 1 0 549108246 12546048 2629 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2629 603 41 0 3022 0
vsize: 12252
[startup+590.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2663 0 0 0 58998 10 0 0 25 0 1 0 549108246 12693504 2641 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3099 2641 603 41 0 3058 0
vsize: 12396
[startup+600.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2667 0 0 0 59998 10 0 0 25 0 1 0 549108246 12693504 2645 4294967295 134512640 134672761 3221224528 3221223712 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3099 2645 603 41 0 3058 0
vsize: 12396
[startup+610.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2687 0 0 0 60998 10 0 0 25 0 1 0 549108246 12828672 2665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3132 2665 603 41 0 3091 0
vsize: 12528
[startup+620.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2703 0 0 0 61998 10 0 0 25 0 1 0 549108246 12828672 2681 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3132 2681 603 41 0 3091 0
vsize: 12528
[startup+630.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2754 0 0 0 62999 10 0 0 25 0 1 0 549108246 13094912 2732 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3197 2732 603 41 0 3156 0
vsize: 12788
[startup+640.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2764 0 0 0 63999 10 0 0 25 0 1 0 549108246 13094912 2742 4294967295 134512640 134672761 3221224528 3221223696 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3197 2742 603 41 0 3156 0
vsize: 12788
[startup+650.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2768 0 0 0 64999 10 0 0 25 0 1 0 549108246 13094912 2746 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3197 2746 603 41 0 3156 0
vsize: 12788
[startup+660.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2791 0 0 0 65999 10 0 0 25 0 1 0 549108246 13234176 2769 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2769 603 41 0 3190 0
vsize: 12924
[startup+670.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2792 0 0 0 66999 10 0 0 25 0 1 0 549108246 13234176 2770 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2770 603 41 0 3190 0
vsize: 12924
[startup+680.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2797 0 0 0 67999 10 0 0 25 0 1 0 549108246 13234176 2775 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2775 603 41 0 3190 0
vsize: 12924
[startup+690.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2797 0 0 0 68999 10 0 0 25 0 1 0 549108246 13234176 2775 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2775 603 41 0 3190 0
vsize: 12924
[startup+700.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2803 0 0 0 69999 10 0 0 25 0 1 0 549108246 13234176 2781 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2781 603 41 0 3190 0
vsize: 12924
[startup+710.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2804 0 0 0 70999 10 0 0 25 0 1 0 549108246 13234176 2782 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2782 603 41 0 3190 0
vsize: 12924
[startup+720.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2806 0 0 0 71999 11 0 0 25 0 1 0 549108246 13234176 2784 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2784 603 41 0 3190 0
vsize: 12924
[startup+730.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2806 0 0 0 72999 11 0 0 25 0 1 0 549108246 13234176 2784 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2784 603 41 0 3190 0
vsize: 12924
[startup+740.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2811 0 0 0 73999 11 0 0 25 0 1 0 549108246 13398016 2789 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2789 603 41 0 3230 0
vsize: 13084
[startup+750.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2811 0 0 0 74999 11 0 0 25 0 1 0 549108246 13398016 2789 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2789 603 41 0 3230 0
vsize: 13084
[startup+760.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2812 0 0 0 75999 11 0 0 25 0 1 0 549108246 13398016 2790 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2790 603 41 0 3230 0
vsize: 13084
[startup+770.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2907 0 0 0 76999 11 0 0 25 0 1 0 549108246 13668352 2885 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3337 2885 603 41 0 3296 0
vsize: 13348
[startup+780.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2914 0 0 0 77999 11 0 0 25 0 1 0 549108246 13807616 2892 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3371 2892 603 41 0 3330 0
vsize: 13484
[startup+790.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2932 0 0 0 78999 11 0 0 25 0 1 0 549108246 13807616 2910 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3371 2910 603 41 0 3330 0
vsize: 13484
[startup+800.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2943 0 0 0 80000 11 0 0 25 0 1 0 549108246 13963264 2921 4294967295 134512640 134672761 3221224528 3221223712 134559199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3409 2921 603 41 0 3368 0
vsize: 13636
[startup+810.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2943 0 0 0 81000 11 0 0 25 0 1 0 549108246 13963264 2921 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3409 2921 603 41 0 3368 0
vsize: 13636
[startup+820.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2948 0 0 0 82000 11 0 0 25 0 1 0 549108246 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+830.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2948 0 0 0 83000 11 0 0 25 0 1 0 549108246 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+840.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2948 0 0 0 84000 11 0 0 25 0 1 0 549108246 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+850.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 2948 0 0 0 85001 11 0 0 25 0 1 0 549108246 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+860.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3010 0 0 0 86000 12 0 0 25 0 1 0 549108246 14229504 2988 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3474 2988 603 41 0 3433 0
vsize: 13896
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3023 0 0 0 87001 12 0 0 25 0 1 0 549108246 14229504 3001 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3474 3001 603 41 0 3433 0
vsize: 13896
[startup+880.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3034 0 0 0 88001 12 0 0 25 0 1 0 549108246 14372864 3012 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3012 603 41 0 3468 0
vsize: 14036
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3040 0 0 0 89001 12 0 0 25 0 1 0 549108246 14372864 3018 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3018 603 41 0 3468 0
vsize: 14036
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3041 0 0 0 90001 12 0 0 25 0 1 0 549108246 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3019 603 41 0 3468 0
vsize: 14036
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3041 0 0 0 91001 12 0 0 25 0 1 0 549108246 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3019 603 41 0 3468 0
vsize: 14036
[startup+920.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3041 0 0 0 92001 12 0 0 25 0 1 0 549108246 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3019 603 41 0 3468 0
vsize: 14036
[startup+930.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3043 0 0 0 93001 12 0 0 25 0 1 0 549108246 14372864 3021 4294967295 134512640 134672761 3221224528 3221223664 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3021 603 41 0 3468 0
vsize: 14036
[startup+940.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3043 0 0 0 94002 12 0 0 25 0 1 0 549108246 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3021 603 41 0 3468 0
vsize: 14036
[startup+950.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3043 0 0 0 95002 12 0 0 25 0 1 0 549108246 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3021 603 41 0 3468 0
vsize: 14036
[startup+960.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3047 0 0 0 96002 12 0 0 25 0 1 0 549108246 14372864 3025 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3025 603 41 0 3468 0
vsize: 14036
[startup+970.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3062 0 0 0 97002 12 0 0 25 0 1 0 549108246 14372864 3040 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3040 603 41 0 3468 0
vsize: 14036
[startup+980.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3063 0 0 0 98002 12 0 0 25 0 1 0 549108246 14372864 3041 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3041 603 41 0 3468 0
vsize: 14036
[startup+990.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3072 0 0 0 99002 12 0 0 25 0 1 0 549108246 14520320 3050 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3050 603 41 0 3504 0
vsize: 14180
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3085 0 0 0 100003 12 0 0 25 0 1 0 549108246 14520320 3063 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3063 603 41 0 3504 0
vsize: 14180
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3086 0 0 0 101003 12 0 0 25 0 1 0 549108246 14520320 3064 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3064 603 41 0 3504 0
vsize: 14180
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3093 0 0 0 102003 12 0 0 25 0 1 0 549108246 14520320 3071 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3071 603 41 0 3504 0
vsize: 14180
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3094 0 0 0 103003 12 0 0 25 0 1 0 549108246 14520320 3072 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3072 603 41 0 3504 0
vsize: 14180
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3107 0 0 0 104003 12 0 0 25 0 1 0 549108246 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 3085 603 41 0 3539 0
vsize: 14320
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3107 0 0 0 105004 12 0 0 25 0 1 0 549108246 14663680 3085 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 3085 603 41 0 3539 0
vsize: 14320
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3107 0 0 0 106004 12 0 0 25 0 1 0 549108246 14663680 3085 4294967295 134512640 134672761 3221224528 3221223712 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 3085 603 41 0 3539 0
vsize: 14320
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3107 0 0 0 107004 12 0 0 25 0 1 0 549108246 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 3085 603 41 0 3539 0
vsize: 14320
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3113 0 0 0 108004 12 0 0 25 0 1 0 549108246 14663680 3091 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 3091 603 41 0 3539 0
vsize: 14320
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3153 0 0 0 109004 12 0 0 25 0 1 0 549108246 14794752 3131 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3612 3131 603 41 0 3571 0
vsize: 14448
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3166 0 0 0 110004 12 0 0 25 0 1 0 549108246 14942208 3144 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3144 603 41 0 3607 0
vsize: 14592
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3185 0 0 0 111005 12 0 0 25 0 1 0 549108246 14942208 3163 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3163 603 41 0 3607 0
vsize: 14592
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3186 0 0 0 112005 12 0 0 25 0 1 0 549108246 14942208 3164 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3164 603 41 0 3607 0
vsize: 14592
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3193 0 0 0 113005 12 0 0 25 0 1 0 549108246 15089664 3171 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3684 3171 603 41 0 3643 0
vsize: 14736
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3203 0 0 0 114005 12 0 0 25 0 1 0 549108246 15089664 3181 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3684 3181 603 41 0 3643 0
vsize: 14736
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3213 0 0 0 115006 12 0 0 25 0 1 0 549108246 15089664 3191 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3684 3191 603 41 0 3643 0
vsize: 14736
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3215 0 0 0 116006 12 0 0 25 0 1 0 549108246 15089664 3193 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3684 3193 603 41 0 3643 0
vsize: 14736
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3217 0 0 0 117006 12 0 0 25 0 1 0 549108246 15089664 3195 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3684 3195 603 41 0 3643 0
vsize: 14736
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3226 0 0 0 118006 12 0 0 25 0 1 0 549108246 15253504 3204 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3724 3204 603 41 0 3683 0
vsize: 14896
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3227 0 0 0 119006 12 0 0 25 0 1 0 549108246 15253504 3205 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3724 3205 603 41 0 3683 0
vsize: 14896
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 13504
Raw data (stat): 13504 (minisat+) R 13503 26298 26297 0 -1 0 3237 0 0 0 120006 12 0 0 25 0 1 0 549108246 15253504 3215 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3724 3215 603 41 0 3683 0
vsize: 14896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 13504
Raw data (stat): 13504 (minisat+) Z 13503 26298 26297 0 -1 12 3240 0 0 0 120007 13 0 0 25 0 1 0 549108246 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.04
CPU time (s): 1200.2
CPU user time (s): 1200.07
CPU system time (s): 0.133979
CPU usage (%): 100.013
Max. virtual memory (Kb): 14896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####