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/miplib2003/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	10386fd19d9976c249ce2be861b38a70
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.12
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 21789

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-22 00:57:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12646 boxname=wulflinc11 idbench=973 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10386fd19d9976c249ce2be861b38a70  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 12646
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        246400 kB
Buffers:         36172 kB
Cached:         730392 kB
SwapCached:          0 kB
Active:         382132 kB
Inactive:       387172 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        246148 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            13264 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:17:42 (client local time) WITH STATUS 10 IN 1200.53 SECONDS
stats: 12646 7 1200.53 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.75 0.86 0.87 2/54 15287
Raw data (stat): 15287 (runsolver) R 15286 32461 32460 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 491353053 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.79 0.86 0.87 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1038 0 0 0 996 2 0 0 25 0 1 0 491353053 5865472 1016 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1432 1016 603 41 0 1391 0
vsize: 5728
[startup+20.0145 s]
Raw data (loadavg): 0.82 0.86 0.87 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1132 0 0 0 1996 3 0 0 25 0 1 0 491353053 6303744 1110 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1110 603 41 0 1498 0
vsize: 6156
[startup+30.0152 s]
Raw data (loadavg): 0.85 0.87 0.87 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1205 0 0 0 2996 3 0 0 25 0 1 0 491353053 6574080 1183 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1605 1183 603 41 0 1564 0
vsize: 6420
[startup+40.0161 s]
Raw data (loadavg): 0.87 0.87 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1343 0 0 0 3995 4 0 0 25 0 1 0 491353053 7110656 1321 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1736 1321 603 41 0 1695 0
vsize: 6944
[startup+50.0282 s]
Raw data (loadavg): 0.89 0.87 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1467 0 0 0 4996 4 0 0 25 0 1 0 491353053 7647232 1445 4294967295 134512640 134672761 3221224528 3221223712 134559599 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.0357 s]
Raw data (loadavg): 0.91 0.88 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1467 0 0 0 5996 5 0 0 25 0 1 0 491353053 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.0497 s]
Raw data (loadavg): 0.92 0.88 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1572 0 0 0 6997 6 0 0 25 0 1 0 491353053 8048640 1550 4294967295 134512640 134672761 3221224528 3221223632 134559841 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.0548 s]
Raw data (loadavg): 0.93 0.89 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1574 0 0 0 7997 6 0 0 25 0 1 0 491353053 8048640 1552 4294967295 134512640 134672761 3221224528 3221223696 134560869 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.0551 s]
Raw data (loadavg): 0.94 0.89 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1617 0 0 0 8996 7 0 0 25 0 1 0 491353053 8286208 1595 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.055 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1617 0 0 0 9996 7 0 0 25 0 1 0 491353053 8286208 1595 4294967295 134512640 134672761 3221224528 3221223696 134561193 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.065 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 10997 7 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223664 134560667 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.065 s]
Raw data (loadavg): 0.96 0.90 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 11997 8 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223632 134560289 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.181 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 13008 8 0 0 25 0 1 0 491353053 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+140.298 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 15287
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 14019 8 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560858 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.324 s]
Raw data (loadavg): 1.06 0.92 0.89 2/56 15295
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 15019 11 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+160.341 s]
Raw data (loadavg): 1.20 0.96 0.90 3/58 15332
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 16020 11 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2023 1596 603 41 0 1982 0
vsize: 8092
[startup+170.361 s]
Raw data (loadavg): 1.32 0.99 0.91 2/54 15340
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1734 0 0 0 17023 11 0 0 25 0 1 0 491353053 8814592 1712 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2152 1712 603 41 0 2111 0
vsize: 8608
[startup+180.361 s]
Raw data (loadavg): 1.27 0.99 0.91 2/54 15340
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1846 0 0 0 18022 11 0 0 25 0 1 0 491353053 9216000 1824 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2250 1824 603 41 0 2209 0
vsize: 9000
[startup+190.361 s]
Raw data (loadavg): 1.23 0.99 0.91 2/54 15340
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1960 0 0 0 19022 12 0 0 25 0 1 0 491353053 9744384 1938 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2379 1938 603 41 0 2338 0
vsize: 9516
[startup+200.369 s]
Raw data (loadavg): 1.19 0.99 0.91 2/54 15340
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2029 0 0 0 20022 12 0 0 25 0 1 0 491353053 10010624 2007 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2007 603 41 0 2403 0
vsize: 9776
[startup+210.369 s]
Raw data (loadavg): 1.16 0.99 0.91 2/54 15340
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2144 0 0 0 21022 12 0 0 25 0 1 0 491353053 10534912 2122 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2572 2122 603 41 0 2531 0
vsize: 10288
[startup+220.391 s]
Raw data (loadavg): 1.14 0.99 0.91 2/54 15340
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 22024 12 0 0 25 0 1 0 491353053 10665984 2154 4294967295 134512640 134672761 3221224528 3221223728 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2604 2154 603 41 0 2563 0
vsize: 10416
[startup+230.39 s]
Raw data (loadavg): 1.11 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 23024 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223712 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+240.391 s]
Raw data (loadavg): 1.10 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 24025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+250.391 s]
Raw data (loadavg): 1.08 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 25025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+260.392 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 26025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+270.391 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 27025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+280.397 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 28026 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+290.402 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 29026 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+300.401 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 30027 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+310.402 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 31027 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2154 603 41 0 2561 0
vsize: 10408
[startup+320.402 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2186 0 0 0 32027 12 0 0 25 0 1 0 491353053 10657792 2164 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2164 603 41 0 2561 0
vsize: 10408
[startup+330.402 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 33026 12 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223712 134559304 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+340.402 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 34026 12 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+350.402 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 35026 12 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+360.402 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 36027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+370.402 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 37027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223632 134560267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+380.402 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 38027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+390.402 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 39027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+400.402 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 40027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+410.405 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 41028 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2168 603 41 0 2561 0
vsize: 10408
[startup+420.405 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2200 0 0 0 42028 13 0 0 25 0 1 0 491353053 10657792 2178 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2178 603 41 0 2561 0
vsize: 10408
[startup+430.405 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2213 0 0 0 43028 13 0 0 25 0 1 0 491353053 10805248 2191 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2638 2191 603 41 0 2597 0
vsize: 10552
[startup+440.406 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2305 0 0 0 44028 13 0 0 25 0 1 0 491353053 11075584 2283 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2704 2283 603 41 0 2663 0
vsize: 10816
[startup+450.405 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2320 0 0 0 45027 13 0 0 25 0 1 0 491353053 11218944 2298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2739 2298 603 41 0 2698 0
vsize: 10956
[startup+460.406 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2320 0 0 0 46028 13 0 0 25 0 1 0 491353053 11218944 2298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2739 2298 603 41 0 2698 0
vsize: 10956
[startup+470.406 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15342
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2323 0 0 0 47028 13 0 0 25 0 1 0 491353053 11218944 2301 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2739 2301 603 41 0 2698 0
vsize: 10956
[startup+480.405 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2414 0 0 0 48028 14 0 0 25 0 1 0 491353053 11616256 2392 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2392 603 41 0 2795 0
vsize: 11344
[startup+490.406 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2511 0 0 0 49028 14 0 0 25 0 1 0 491353053 12017664 2489 4294967295 134512640 134672761 3221224528 3221223712 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2934 2489 603 41 0 2893 0
vsize: 11736
[startup+500.406 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2518 0 0 0 50028 14 0 0 25 0 1 0 491353053 12017664 2496 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2934 2496 603 41 0 2893 0
vsize: 11736
[startup+510.407 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2588 0 0 0 51028 14 0 0 25 0 1 0 491353053 12279808 2566 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2998 2566 603 41 0 2957 0
vsize: 11992
[startup+520.407 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2600 0 0 0 52028 14 0 0 25 0 1 0 491353053 12414976 2578 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3031 2578 603 41 0 2990 0
vsize: 12124
[startup+530.407 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2608 0 0 0 53028 14 0 0 25 0 1 0 491353053 12414976 2586 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3031 2586 603 41 0 2990 0
vsize: 12124
[startup+540.407 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2614 0 0 0 54028 14 0 0 25 0 1 0 491353053 12414976 2592 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3031 2592 603 41 0 2990 0
vsize: 12124
[startup+550.408 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2634 0 0 0 55028 14 0 0 25 0 1 0 491353053 12546048 2612 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2612 603 41 0 3022 0
vsize: 12252
[startup+560.408 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2638 0 0 0 56029 14 0 0 25 0 1 0 491353053 12546048 2616 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2616 603 41 0 3022 0
vsize: 12252
[startup+570.409 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2645 0 0 0 57029 14 0 0 25 0 1 0 491353053 12546048 2623 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2623 603 41 0 3022 0
vsize: 12252
[startup+580.409 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2663 0 0 0 58029 14 0 0 25 0 1 0 491353053 12693504 2641 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3099 2641 603 41 0 3058 0
vsize: 12396
[startup+590.409 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2667 0 0 0 59029 14 0 0 25 0 1 0 491353053 12693504 2645 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3099 2645 603 41 0 3058 0
vsize: 12396
[startup+600.41 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2667 0 0 0 60029 14 0 0 25 0 1 0 491353053 12693504 2645 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3099 2645 603 41 0 3058 0
vsize: 12396
[startup+610.411 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2695 0 0 0 61030 14 0 0 25 0 1 0 491353053 12828672 2673 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3132 2673 603 41 0 3091 0
vsize: 12528
[startup+620.412 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2724 0 0 0 62030 15 0 0 25 0 1 0 491353053 12959744 2702 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3164 2702 603 41 0 3123 0
vsize: 12656
[startup+630.411 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2759 0 0 0 63030 15 0 0 25 0 1 0 491353053 13094912 2737 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3197 2737 603 41 0 3156 0
vsize: 12788
[startup+640.412 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2767 0 0 0 64030 15 0 0 25 0 1 0 491353053 13094912 2745 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3197 2745 603 41 0 3156 0
vsize: 12788
[startup+650.412 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2768 0 0 0 65030 15 0 0 25 0 1 0 491353053 13094912 2746 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3197 2746 603 41 0 3156 0
vsize: 12788
[startup+660.413 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2791 0 0 0 66030 15 0 0 25 0 1 0 491353053 13234176 2769 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2769 603 41 0 3190 0
vsize: 12924
[startup+670.414 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2796 0 0 0 67030 15 0 0 25 0 1 0 491353053 13234176 2774 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2774 603 41 0 3190 0
vsize: 12924
[startup+680.413 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2797 0 0 0 68030 15 0 0 25 0 1 0 491353053 13234176 2775 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2775 603 41 0 3190 0
vsize: 12924
[startup+690.414 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2803 0 0 0 69031 15 0 0 25 0 1 0 491353053 13234176 2781 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2781 603 41 0 3190 0
vsize: 12924
[startup+700.414 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2804 0 0 0 70031 15 0 0 25 0 1 0 491353053 13234176 2782 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3231 2782 603 41 0 3190 0
vsize: 12924
[startup+710.416 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2806 0 0 0 71031 15 0 0 25 0 1 0 491353053 13234176 2784 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2784 603 41 0 3190 0
vsize: 12924
[startup+720.415 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2806 0 0 0 72031 15 0 0 25 0 1 0 491353053 13234176 2784 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2784 603 41 0 3190 0
vsize: 12924
[startup+730.416 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2806 0 0 0 73031 15 0 0 25 0 1 0 491353053 13234176 2784 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2784 603 41 0 3190 0
vsize: 12924
[startup+740.416 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2811 0 0 0 74031 15 0 0 25 0 1 0 491353053 13398016 2789 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3271 2789 603 41 0 3230 0
vsize: 13084
[startup+750.416 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2812 0 0 0 75031 15 0 0 25 0 1 0 491353053 13398016 2790 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3271 2790 603 41 0 3230 0
vsize: 13084
[startup+760.417 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2907 0 0 0 76031 15 0 0 25 0 1 0 491353053 13668352 2885 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3337 2885 603 41 0 3296 0
vsize: 13348
[startup+770.417 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2907 0 0 0 77032 15 0 0 25 0 1 0 491353053 13668352 2885 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3337 2885 603 41 0 3296 0
vsize: 13348
[startup+780.416 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2929 0 0 0 78032 15 0 0 25 0 1 0 491353053 13807616 2907 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3371 2907 603 41 0 3330 0
vsize: 13484
[startup+790.417 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2933 0 0 0 79032 15 0 0 25 0 1 0 491353053 13807616 2911 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3371 2911 603 41 0 3330 0
vsize: 13484
[startup+800.417 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2943 0 0 0 80032 15 0 0 25 0 1 0 491353053 13963264 2921 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3409 2921 603 41 0 3368 0
vsize: 13636
[startup+810.417 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 81032 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+820.418 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 82032 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+830.417 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 83033 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+840.418 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 84033 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3409 2926 603 41 0 3368 0
vsize: 13636
[startup+850.418 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3004 0 0 0 85033 15 0 0 25 0 1 0 491353053 14094336 2982 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3441 2982 603 41 0 3400 0
vsize: 13764
[startup+860.419 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3018 0 0 0 86033 16 0 0 25 0 1 0 491353053 14229504 2996 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3474 2996 603 41 0 3433 0
vsize: 13896
[startup+870.418 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3034 0 0 0 87033 16 0 0 25 0 1 0 491353053 14372864 3012 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3509 3012 603 41 0 3468 0
vsize: 14036
[startup+880.418 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3035 0 0 0 88033 16 0 0 25 0 1 0 491353053 14372864 3013 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3509 3013 603 41 0 3468 0
vsize: 14036
[startup+890.419 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3041 0 0 0 89033 16 0 0 25 0 1 0 491353053 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3509 3019 603 41 0 3468 0
vsize: 14036
[startup+900.419 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3041 0 0 0 90034 16 0 0 25 0 1 0 491353053 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3509 3019 603 41 0 3468 0
vsize: 14036
[startup+910.42 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3041 0 0 0 91033 16 0 0 25 0 1 0 491353053 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560942 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.422 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3043 0 0 0 92032 16 0 0 25 0 1 0 491353053 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3021 603 41 0 3468 0
vsize: 14036
[startup+930.421 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3043 0 0 0 93031 17 0 0 25 0 1 0 491353053 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+940.421 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3043 0 0 0 94031 17 0 0 25 0 1 0 491353053 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134561205 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.422 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3046 0 0 0 95030 17 0 0 25 0 1 0 491353053 14372864 3024 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3024 603 41 0 3468 0
vsize: 14036
[startup+960.422 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3059 0 0 0 96030 18 0 0 25 0 1 0 491353053 14372864 3037 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3037 603 41 0 3468 0
vsize: 14036
[startup+970.423 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3063 0 0 0 97030 18 0 0 25 0 1 0 491353053 14372864 3041 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3041 603 41 0 3468 0
vsize: 14036
[startup+980.423 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3067 0 0 0 98030 18 0 0 25 0 1 0 491353053 14372864 3045 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 3045 603 41 0 3468 0
vsize: 14036
[startup+990.424 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3078 0 0 0 99030 18 0 0 25 0 1 0 491353053 14520320 3056 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3056 603 41 0 3504 0
vsize: 14180
[startup+1000.42 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3085 0 0 0 100030 18 0 0 25 0 1 0 491353053 14520320 3063 4294967295 134512640 134672761 3221224528 3221223696 134560785 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.42 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3093 0 0 0 101030 18 0 0 25 0 1 0 491353053 14520320 3071 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3071 603 41 0 3504 0
vsize: 14180
[startup+1020.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3094 0 0 0 102030 19 0 0 25 0 1 0 491353053 14520320 3072 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3072 603 41 0 3504 0
vsize: 14180
[startup+1030.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3106 0 0 0 103030 19 0 0 25 0 1 0 491353053 14663680 3084 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 3084 603 41 0 3539 0
vsize: 14320
[startup+1040.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 104029 20 0 0 25 0 1 0 491353053 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.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 105029 20 0 0 25 0 1 0 491353053 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134561011 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.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 106029 20 0 0 25 0 1 0 491353053 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134561151 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.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 107029 20 0 0 25 0 1 0 491353053 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+1080.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3118 0 0 0 108029 20 0 0 25 0 1 0 491353053 14663680 3096 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3580 3096 603 41 0 3539 0
vsize: 14320
[startup+1090.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3156 0 0 0 109029 20 0 0 25 0 1 0 491353053 14794752 3134 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3612 3134 603 41 0 3571 0
vsize: 14448
[startup+1100.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3172 0 0 0 110029 20 0 0 25 0 1 0 491353053 14942208 3150 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3648 3150 603 41 0 3607 0
vsize: 14592
[startup+1110.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3186 0 0 0 111029 21 0 0 25 0 1 0 491353053 14942208 3164 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3648 3164 603 41 0 3607 0
vsize: 14592
[startup+1120.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3193 0 0 0 112029 21 0 0 25 0 1 0 491353053 15089664 3171 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3684 3171 603 41 0 3643 0
vsize: 14736
[startup+1130.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3203 0 0 0 113029 21 0 0 25 0 1 0 491353053 15089664 3181 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3684 3181 603 41 0 3643 0
vsize: 14736
[startup+1140.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3210 0 0 0 114029 21 0 0 25 0 1 0 491353053 15089664 3188 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3684 3188 603 41 0 3643 0
vsize: 14736
[startup+1150.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3215 0 0 0 115030 21 0 0 25 0 1 0 491353053 15089664 3193 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3684 3193 603 41 0 3643 0
vsize: 14736
[startup+1160.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3216 0 0 0 116030 21 0 0 25 0 1 0 491353053 15089664 3194 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3684 3194 603 41 0 3643 0
vsize: 14736
[startup+1170.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3226 0 0 0 117030 21 0 0 25 0 1 0 491353053 15253504 3204 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3724 3204 603 41 0 3683 0
vsize: 14896
[startup+1180.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3227 0 0 0 118030 21 0 0 25 0 1 0 491353053 15253504 3205 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3724 3205 603 41 0 3683 0
vsize: 14896
[startup+1190.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3236 0 0 0 119030 21 0 0 25 0 1 0 491353053 15253504 3214 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3724 3214 603 41 0 3683 0
vsize: 14896
[startup+1200.43 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15344
Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3237 0 0 0 120030 21 0 0 25 0 1 0 491353053 15253504 3215 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3724 3215 603 41 0 3683 0
vsize: 14896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.44 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 15344
Raw data (stat): 15287 (minisat+) Z 15286 32461 32460 0 -1 12 3240 0 0 0 120030 22 0 0 25 0 1 0 491353053 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.44
CPU time (s): 1200.53
CPU user time (s): 1200.31
CPU system time (s): 0.221966
CPU usage (%): 100.008
Max. virtual memory (Kb): 14896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####