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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-lseu.opb
MD5SUM	99657262afbbfce7034a3ec6b29d9b3b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1120
Optimality of the best value was proved	NO
Number of terms in the objective function	85
Biggest coefficient in the objective function	517
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	15494
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1656
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	15494
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02884
Number of variables	89
Total number of constraints	117
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	104
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	47
Trace number 15135

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        828024 kB
Buffers:         22560 kB
Cached:         162628 kB
SwapCached:        316 kB
Active:          27472 kB
Inactive:       160016 kB
HighTotal:      131008 kB
HighFree:        38444 kB
LowTotal:       903652 kB
LowFree:        789580 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13496 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:20:29 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 18496 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ...s..
c ---[  28]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  26]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[  21]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  19]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  17]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  12]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   9]---> Adder-cost: 276   maxlim: 540   bits: 11/10
c ---[   8]---> Adder-cost: 44   maxlim: 125   bits: 8/7
c ---[   7]---> Adder-cost: 122   maxlim: 179   bits: 9/8
c ---[   6]---> Adder-cost: 177   maxlim: 331   bits: 10/9
c ---[   4]---> Adder-cost: 182   maxlim: 205   bits: 9/8
c ---[   2]---> Adder-cost: 37   maxlim: 99   bits: 8/7
c ---[   0]---> Adder-cost: 79   maxlim: 66   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6073    21615 |    2024       0        0     nan |  0.000 % |
c |       100 |    6042    21516 |    2226      97      696     7.2 |  7.123 % |
c |       250 |    6012    21412 |    2449     237     1761     7.4 |  7.401 % |
c ==============================================================================
c [1mFound solution: 3744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 596   maxlim: 11750   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       326 |   10077    35877 |    3359     313     2716     8.7 |  7.401 % |
c |       427 |   10077    35877 |    3694     414     5022    12.1 |  5.388 % |
c |       578 |   10068    35848 |    4064     564     7554    13.4 |  5.506 % |
c ==============================================================================
c [1mFound solution: 2742[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12752   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       670 |   10068    35818 |    3356     656     9564    14.6 |  5.506 % |
c |       770 |   10068    35818 |    3691     756    10783    14.3 |  5.893 % |
c |       920 |   10068    35818 |    4060     906    14323    15.8 |  5.893 % |
c ==============================================================================
c [1mFound solution: 2123[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13371   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       993 |   10075    35865 |    3358     979    16062    16.4 |  5.893 % |
c |      1094 |   10075    35865 |    3693    1080    17993    16.7 |  6.169 % |
c |      1244 |   10075    35865 |    4063    1230    20024    16.3 |  6.169 % |
c |      1469 |   10039    35737 |    4469    1448    21972    15.2 |  6.287 % |
c |      1808 |   10039    35737 |    4916    1787    40323    22.6 |  6.287 % |
c |      2314 |    9981    35547 |    5408    2286    51063    22.3 |  6.758 % |
c |      3073 |    9981    35547 |    5948    3045    72515    23.8 |  6.757 % |
c ==============================================================================
c [1mFound solution: 2063[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13431   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3941 |    9986    35583 |    3328    3913   113826    29.1 |  6.757 % |
c |      4041 |    9956    35484 |    3660    2049    56022    27.3 |  7.147 % |
c |      4193 |    9956    35484 |    4026    2201    62222    28.3 |  7.147 % |
c |      4418 |    9956    35484 |    4429    2426    69505    28.7 |  7.147 % |
c |      4757 |    9956    35484 |    4872    2765    81253    29.4 |  7.147 % |
c |      5264 |    9956    35484 |    5359    3272    97024    29.7 |  7.147 % |
c |      6023 |    9956    35484 |    5895    4031   125996    31.3 |  7.147 % |
c |      7163 |    9956    35484 |    6485    5171   186389    36.0 |  7.147 % |
c ==============================================================================
c [1mFound solution: 2056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13438   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8826 |    9961    35524 |    3320    6834   293189    42.9 |  7.147 % |
c |      8926 |    9961    35524 |    3652    3517   150842    42.9 |  7.301 % |
c |      9077 |    9946    35471 |    4017    3664   153692    41.9 |  7.360 % |
c |      9303 |    9946    35471 |    4418    3890   165590    42.6 |  7.360 % |
c |      9640 |    9946    35471 |    4860    4227   177037    41.9 |  7.360 % |
c |     10146 |    9922    35389 |    5346    4729   194617    41.2 |  7.477 % |
c |     10907 |    9922    35389 |    5881    5490   229481    41.8 |  7.477 % |
c |     12049 |    9913    35358 |    6469    3600   114427    31.8 |  7.535 % |
c |     13758 |    9913    35358 |    7116    5309   203119    38.3 |  7.535 % |
c |     16320 |    9886    35269 |    7828    4187   129662    31.0 |  7.769 % |
c |     20167 |    9886    35269 |    8611    8034   338658    42.2 |  7.769 % |
c ==============================================================================
c [1mFound solution: 1595[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13899   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20212 |    9893    35309 |    3297    8079   341094    42.2 |  7.769 % |
c |     20312 |    9893    35309 |    3626    2120    65162    30.7 |  7.979 % |
c |     20462 |    9893    35309 |    3989    2270    72349    31.9 |  7.979 % |
c |     20687 |    9893    35309 |    4388    2495    81525    32.7 |  7.979 % |
c |     21024 |    9893    35309 |    4827    2832    99154    35.0 |  7.979 % |
c |     21534 |    9893    35309 |    5309    3342   120991    36.2 |  7.979 % |
c ==============================================================================
c [1mFound solution: 1411[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14083   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22133 |    9896    35327 |    3298    3941   151145    38.4 |  7.979 % |
c |     22235 |    9896    35327 |    3627    2073    53987    26.0 |  8.081 % |
c |     22385 |    9896    35327 |    3990    2223    60560    27.2 |  8.082 % |
c |     22610 |    9896    35327 |    4389    2448    68321    27.9 |  8.081 % |
c |     22954 |    9896    35327 |    4828    2792    83698    30.0 |  8.081 % |
c |     23461 |    9870    35237 |    5311    3286   101785    31.0 |  8.314 % |
c |     24220 |    9870    35237 |    5842    4045   142097    35.1 |  8.314 % |
c |     25359 |    9870    35237 |    6426    5184   196191    37.8 |  8.314 % |
c |     27067 |    9870    35237 |    7069    3503   112162    32.0 |  8.314 % |
c ==============================================================================
c [1mFound solution: 1409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14085   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29382 |    9872    35251 |    3290    5818   242642    41.7 |  8.314 % |
c |     29483 |    9872    35251 |    3619    3010   104451    34.7 |  8.362 % |
c |     29633 |    9857    35200 |    3980    3154   108200    34.3 |  8.479 % |
c |     29858 |    9857    35200 |    4378    3379   119910    35.5 |  8.479 % |
c |     30196 |    9857    35200 |    4816    3717   131296    35.3 |  8.479 % |
c |     30702 |    9857    35200 |    5298    4223   152616    36.1 |  8.479 % |
c |     31464 |    9857    35200 |    5828    4985   186177    37.3 |  8.479 % |
c |     32603 |    9857    35200 |    6411    6124   251862    41.1 |  8.479 % |
c |     34311 |    9857    35200 |    7052    4258   130688    30.7 |  8.479 % |
c |     36874 |    9830    35107 |    7757    6815   223583    32.8 |  8.595 % |
c |     40718 |    9830    35107 |    8533    6466   267915    41.4 |  8.595 % |
c ==============================================================================
c [1mFound solution: 1355[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14139   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41279 |    9838    35150 |    3279    7027   296604    42.2 |  8.595 % |
c |     41381 |    9838    35150 |    3606    1859    47805    25.7 |  8.786 % |
c |     41532 |    9838    35150 |    3967    2010    54805    27.3 |  8.786 % |
c |     41757 |    9838    35150 |    4364    2235    63140    28.3 |  8.786 % |
c |     42095 |    9838    35150 |    4800    2573    75549    29.4 |  8.786 % |
c |     42604 |    9838    35150 |    5280    3082    97659    31.7 |  8.786 % |
c |     43365 |    9838    35150 |    5808    3843   126545    32.9 |  8.786 % |
c |     44504 |    9838    35150 |    6389    4982   188574    37.9 |  8.786 % |
c |     46213 |    9838    35150 |    7028    6691   262858    39.3 |  8.786 % |
c |     48778 |    9838    35150 |    7731    5487   199986    36.4 |  8.786 % |
c |     52622 |    9838    35150 |    8504    5191   194613    37.5 |  8.786 % |
c ==============================================================================
c [1mFound solution: 1354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14140   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55808 |    9839    35163 |    3279    8377   369220    44.1 |  8.786 % |
c |     55908 |    9839    35163 |    3606    2195    63417    28.9 |  8.839 % |
c |     56059 |    9839    35163 |    3967    2346    70072    29.9 |  8.839 % |
c |     56284 |    9839    35163 |    4364    2571    78194    30.4 |  8.839 % |
c |     56624 |    9839    35163 |    4800    2911    92105    31.6 |  8.839 % |
c |     57130 |    9839    35163 |    5280    3417   115959    33.9 |  8.839 % |
c |     57890 |    9839    35163 |    5808    4177   151534    36.3 |  8.839 % |
c |     59029 |    9839    35163 |    6389    5316   196591    37.0 |  8.839 % |
c ==============================================================================
c [1mFound solution: 1341[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14153   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60642 |    9843    35194 |    3281    3484   112905    32.4 |  8.839 % |
c |     60742 |    9843    35194 |    3609    1842    44074    23.9 |  8.991 % |
c |     60892 |    9843    35194 |    3970    1992    51390    25.8 |  8.991 % |
c |     61117 |    9843    35194 |    4367    2217    58712    26.5 |  8.991 % |
c |     61454 |    9843    35194 |    4803    2554    73564    28.8 |  8.991 % |
c |     61960 |    9843    35194 |    5284    3060    96285    31.5 |  8.991 % |
c |     62721 |    9843    35194 |    5812    3821   133487    34.9 |  8.991 % |
c ==============================================================================
c [1mFound solution: 1244[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14250   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63503 |    9849    35245 |    3283    4603   175620    38.2 |  8.991 % |
c |     63608 |    9849    35245 |    3611    2407    77173    32.1 |  9.248 % |
c |     63760 |    9849    35245 |    3972    2559    82963    32.4 |  9.248 % |
c |     63986 |    9849    35245 |    4369    2785    90166    32.4 |  9.248 % |
c |     64326 |    9849    35245 |    4806    3125   102835    32.9 |  9.248 % |
c |     64833 |    9849    35245 |    5287    3632   122546    33.7 |  9.248 % |
c |     65594 |    9849    35245 |    5816    4393   155468    35.4 |  9.248 % |
c |     66735 |    9849    35245 |    6397    5534   210113    38.0 |  9.248 % |
c |     68443 |    9849    35245 |    7037    3775   121107    32.1 |  9.248 % |
c ==============================================================================
c [1mFound solution: 1225[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14269   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69543 |    9857    35292 |    3285    4875   178413    36.6 |  9.248 % |
c |     69643 |    9857    35292 |    3613    2538    80051    31.5 |  9.434 % |
c |     69793 |    9857    35292 |    3974    2688    86260    32.1 |  9.434 % |
c |     70019 |    9857    35292 |    4372    2914    95776    32.9 |  9.434 % |
c |     70358 |    9857    35292 |    4809    3253   109307    33.6 |  9.434 % |
c |     70865 |    9857    35292 |    5290    3760   131825    35.1 |  9.434 % |
c |     71625 |    9857    35292 |    5819    4520   165459    36.6 |  9.434 % |
c |     72764 |    9857    35292 |    6401    5659   218043    38.5 |  9.434 % |
c |     74473 |    9857    35292 |    7041    3973   127402    32.1 |  9.434 % |
c |     77036 |    9857    35292 |    7745    6536   234123    35.8 |  9.434 % |
c |     80880 |    9857    35292 |    8520    6264   215952    34.5 |  9.434 % |
c |     86646 |    9857    35292 |    9372    7573   269385    35.6 |  9.434 % |
c |     95295 |    9857    35292 |   10309    6357   219836    34.6 |  9.434 % |
c |    108269 |    9857    35292 |   11340    8599   339048    39.4 |  9.434 % |
c ==============================================================================
c [1mFound solution: 1176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14318   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    116581 |    9869    35364 |    3289   11045   498401    45.1 |  9.434 % |
c |    116682 |    9869    35364 |    3617    2863    82915    29.0 |  9.710 % |
c |    116832 |    9869    35364 |    3979    3013    88735    29.5 |  9.710 % |
c |    117058 |    9869    35364 |    4377    3239    96618    29.8 |  9.710 % |
c |    117396 |    9869    35364 |    4815    3577   109222    30.5 |  9.710 % |
c |    117902 |    9869    35364 |    5296    4083   127446    31.2 |  9.710 % |
c |    118661 |    9869    35364 |    5826    4842   156380    32.3 |  9.710 % |
c |    119803 |    9869    35364 |    6409    5984   205650    34.4 |  9.710 % |
c |    121515 |    9869    35364 |    7050    3987   139653    35.0 |  9.711 % |
c |    124077 |    9855    35318 |    7755    6545   242235    37.0 |  9.824 % |
c |    127921 |    9855    35318 |    8530    6309   257348    40.8 |  9.824 % |
c |    133690 |    9855    35318 |    9383    7620   328945    43.2 |  9.824 % |
c |    142340 |    9855    35318 |   10322    6445   223000    34.6 |  9.824 % |
c |    155316 |    9855    35318 |   11354    8686   297676    34.3 |  9.824 % |
c ==============================================================================
c [1mFound solution: 1148[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14346   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    161045 |    9801    34907 |    3267    7834   268043    34.2 |  9.824 % |
c |    161145 |    9801    34907 |    3593    2059    40534    19.7 | 10.238 % |
c |    161295 |    9801    34907 |    3953    2209    45299    20.5 | 10.238 % |
c |    161520 |    9801    34907 |    4348    2434    54304    22.3 | 10.238 % |
c |    161860 |    9801    34907 |    4783    2774    67924    24.5 | 10.238 % |
c |    162366 |    9801    34907 |    5261    3280    91085    27.8 | 10.238 % |
c |    163126 |    9801    34907 |    5787    4040   123661    30.6 | 10.238 % |
c |    164265 |    9801    34907 |    6366    5179   171504    33.1 | 10.238 % |
c |    165974 |    9801    34907 |    7003    3516   108593    30.9 | 10.238 % |
c |    168536 |    9801    34907 |    7703    6078   217407    35.8 | 10.238 % |
c |    172382 |    9801    34907 |    8473    5878   205802    35.0 | 10.238 % |
c |    178149 |    9801    34907 |    9321    7166   286124    39.9 | 10.238 % |
c |    186799 |    9801    34907 |   10253    6069   210970    34.8 | 10.238 % |
c |    199778 |    9801    34907 |   11278    8312   303623    36.5 | 10.238 % |
c |    219240 |    9801    34907 |   12406   10355   356774    34.5 | 10.238 % |
c |    248434 |    9801    34907 |   13647    7537   258472    34.3 | 10.238 % |
c |    292223 |    9801    34907 |   15011    9057   327651    36.2 | 10.238 % |
c |    357909 |    9801    34907 |   16512   13193   545895    41.4 | 10.238 % |
c |    456437 |    9801    34907 |   18164   10196   324063    31.8 | 10.238 % |
c |    604226 |    9801    34907 |   19980    9536   331668    34.8 | 10.238 % |
c |    825910 |    9801    34907 |   21978   17142   712255    41.6 | 10.238 % |
c ==============================================================================
c [1mFound solution: 1143[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 14351   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    954270 |    9802    34915 |    3267   11239   445236    39.6 | 10.238 % |
c |    954370 |    9802    34915 |    3593    2910    75141    25.8 | 10.288 % |
c |    954520 |    9802    34915 |    3953    3060    80689    26.4 | 10.288 % |
c |    954745 |    9802    34915 |    4348    3285    89747    27.3 | 10.288 % |
c |    955083 |    9802    34915 |    4783    3623   100874    27.8 | 10.288 % |
c |    955589 |    9802    34915 |    5261    4129   125730    30.5 | 10.288 % |
c |    956349 |    9802    34915 |    5787    4889   161348    33.0 | 10.288 % |
c |    957488 |    9802    34915 |    6366    6028   210446    34.9 | 10.288 % |
c |    959196 |    9802    34915 |    7003    4347   129377    29.8 | 10.288 % |
c |    961758 |    9802    34915 |    7703    6909   225823    32.7 | 10.288 % |
c |    965602 |    9802    34915 |    8473    6707   209886    31.3 | 10.288 % |
c |    971370 |    9802    34915 |    9321    7948   255665    32.2 | 10.288 % |
c |    980020 |    9802    34915 |   10253    6694   250490    37.4 | 10.288 % |
c |    992995 |    9802    34915 |   11278    8952   354605    39.6 | 10.288 % |
c |   1012456 |    9802    34915 |   12406   10773   449362    41.7 | 10.288 % |
c |   1041651 |    9802    34915 |   13647    7911   288333    36.4 | 10.288 % |
c |   1085443 |    9802    34915 |   15011    9601   290659    30.3 | 10.288 % |
c |   1151127 |    9802    34915 |   16512   13438   545719    40.6 | 10.288 % |
#### 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.97 0.97 0.91 2/54 19040
Raw data (stat): 19040 (runsolver) D 19039 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483447736 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19040
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 882 0 0 0 996 2 0 0 25 0 1 0 483447736 5156864 860 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1259 860 603 41 0 1218 0
vsize: 5036
[startup+20.0014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 19040
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 943 0 0 0 1995 3 0 0 25 0 1 0 483447736 5419008 921 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1323 921 603 41 0 1282 0
vsize: 5292
[startup+30.0011 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 19040
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1016 0 0 0 2994 4 0 0 25 0 1 0 483447736 5836800 994 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 994 603 41 0 1384 0
vsize: 5700
[startup+40.0024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19040
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1064 0 0 0 3993 4 0 0 25 0 1 0 483447736 5967872 1042 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1457 1042 603 41 0 1416 0
vsize: 5828
[startup+50.0029 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19040
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1068 0 0 0 4993 5 0 0 25 0 1 0 483447736 5967872 1046 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1457 1046 603 41 0 1416 0
vsize: 5828
[startup+60.0045 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1137 0 0 0 5993 5 0 0 25 0 1 0 483447736 6238208 1115 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1523 1115 603 41 0 1482 0
vsize: 6092
[startup+70.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1217 0 0 0 6992 6 0 0 25 0 1 0 483447736 6639616 1195 4294967295 134512640 134672761 3221224544 3221223760 134557680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1621 1195 603 41 0 1580 0
vsize: 6484
[startup+80.0064 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1326 0 0 0 7992 6 0 0 25 0 1 0 483447736 7041024 1304 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1719 1304 603 41 0 1678 0
vsize: 6876
[startup+90.0077 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1326 0 0 0 8992 6 0 0 25 0 1 0 483447736 7041024 1304 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1719 1304 603 41 0 1678 0
vsize: 6876
[startup+100.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1326 0 0 0 9991 7 0 0 25 0 1 0 483447736 7041024 1304 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1719 1304 603 41 0 1678 0
vsize: 6876
[startup+110.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1341 0 0 0 10991 7 0 0 25 0 1 0 483447736 7176192 1319 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1752 1319 603 41 0 1711 0
vsize: 7008
[startup+120.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1352 0 0 0 11991 8 0 0 25 0 1 0 483447736 7176192 1330 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1752 1330 603 41 0 1711 0
vsize: 7008
[startup+130.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1353 0 0 0 12991 8 0 0 25 0 1 0 483447736 7176192 1331 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1752 1331 603 41 0 1711 0
vsize: 7008
[startup+140.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1396 0 0 0 13991 8 0 0 25 0 1 0 483447736 7311360 1374 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1785 1374 603 41 0 1744 0
vsize: 7140
[startup+150.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1422 0 0 0 14991 8 0 0 25 0 1 0 483447736 7458816 1400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1821 1400 603 41 0 1780 0
vsize: 7284
[startup+160.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1432 0 0 0 15990 9 0 0 25 0 1 0 483447736 7458816 1410 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1821 1410 603 41 0 1780 0
vsize: 7284
[startup+170.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1496 0 0 0 16990 9 0 0 25 0 1 0 483447736 7729152 1474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1474 603 41 0 1846 0
vsize: 7548
[startup+180.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1516 0 0 0 17990 10 0 0 25 0 1 0 483447736 7864320 1494 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1920 1494 603 41 0 1879 0
vsize: 7680
[startup+190.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1563 0 0 0 18990 10 0 0 25 0 1 0 483447736 7995392 1541 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1952 1541 603 41 0 1911 0
vsize: 7808
[startup+200.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1604 0 0 0 19989 11 0 0 25 0 1 0 483447736 8290304 1582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2024 1582 603 41 0 1983 0
vsize: 8096
[startup+210.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1624 0 0 0 20989 11 0 0 25 0 1 0 483447736 8290304 1602 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2024 1602 603 41 0 1983 0
vsize: 8096
[startup+220.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1645 0 0 0 21989 11 0 0 25 0 1 0 483447736 8421376 1623 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2056 1623 603 41 0 2015 0
vsize: 8224
[startup+230.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1686 0 0 0 22989 12 0 0 25 0 1 0 483447736 8552448 1664 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2088 1664 603 41 0 2047 0
vsize: 8352
[startup+240.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1695 0 0 0 23989 12 0 0 25 0 1 0 483447736 8708096 1673 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2126 1673 603 41 0 2085 0
vsize: 8504
[startup+250.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1714 0 0 0 24989 12 0 0 25 0 1 0 483447736 8708096 1692 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2126 1692 603 41 0 2085 0
vsize: 8504
[startup+260.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1720 0 0 0 25989 12 0 0 25 0 1 0 483447736 8708096 1698 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2126 1698 603 41 0 2085 0
vsize: 8504
[startup+270.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1729 0 0 0 26989 12 0 0 25 0 1 0 483447736 8867840 1707 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2165 1707 603 41 0 2124 0
vsize: 8660
[startup+280.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1735 0 0 0 27989 12 0 0 25 0 1 0 483447736 8867840 1713 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2165 1713 603 41 0 2124 0
vsize: 8660
[startup+290.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1740 0 0 0 28990 12 0 0 25 0 1 0 483447736 8867840 1718 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2165 1718 603 41 0 2124 0
vsize: 8660
[startup+300.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1802 0 0 0 29990 12 0 0 25 0 1 0 483447736 9175040 1780 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1780 603 41 0 2199 0
vsize: 8960
[startup+310.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19042
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1807 0 0 0 30990 12 0 0 25 0 1 0 483447736 9175040 1785 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1785 603 41 0 2199 0
vsize: 8960
[startup+320.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1825 0 0 0 31990 12 0 0 25 0 1 0 483447736 9322496 1803 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2276 1803 603 41 0 2235 0
vsize: 9104
[startup+330.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1833 0 0 0 32990 12 0 0 25 0 1 0 483447736 9322496 1811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2276 1811 603 41 0 2235 0
vsize: 9104
[startup+340.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1847 0 0 0 33990 12 0 0 25 0 1 0 483447736 9486336 1825 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2316 1825 603 41 0 2275 0
vsize: 9264
[startup+350.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1854 0 0 0 34990 12 0 0 25 0 1 0 483447736 9486336 1832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2316 1832 603 41 0 2275 0
vsize: 9264
[startup+360.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1855 0 0 0 35991 12 0 0 25 0 1 0 483447736 9486336 1833 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2316 1833 603 41 0 2275 0
vsize: 9264
[startup+370.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1861 0 0 0 36991 12 0 0 25 0 1 0 483447736 9486336 1839 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2316 1839 603 41 0 2275 0
vsize: 9264
[startup+380.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1861 0 0 0 37991 12 0 0 25 0 1 0 483447736 9486336 1839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2316 1839 603 41 0 2275 0
vsize: 9264
[startup+390.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1863 0 0 0 38991 12 0 0 25 0 1 0 483447736 9486336 1841 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2316 1841 603 41 0 2275 0
vsize: 9264
[startup+400.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1936 0 0 0 39991 12 0 0 25 0 1 0 483447736 9752576 1914 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1914 603 41 0 2340 0
vsize: 9524
[startup+410.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1955 0 0 0 40991 12 0 0 25 0 1 0 483447736 9887744 1933 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1933 603 41 0 2373 0
vsize: 9656
[startup+420.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1956 0 0 0 41991 12 0 0 25 0 1 0 483447736 9887744 1934 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1934 603 41 0 2373 0
vsize: 9656
[startup+430.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1963 0 0 0 42992 12 0 0 25 0 1 0 483447736 9887744 1941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1941 603 41 0 2373 0
vsize: 9656
[startup+440.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1964 0 0 0 43992 12 0 0 25 0 1 0 483447736 9887744 1942 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1942 603 41 0 2373 0
vsize: 9656
[startup+450.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1967 0 0 0 44992 12 0 0 25 0 1 0 483447736 9887744 1945 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1945 603 41 0 2373 0
vsize: 9656
[startup+460.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1974 0 0 0 45992 12 0 0 25 0 1 0 483447736 9887744 1952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1952 603 41 0 2373 0
vsize: 9656
[startup+470.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1974 0 0 0 46992 12 0 0 25 0 1 0 483447736 9887744 1952 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1952 603 41 0 2373 0
vsize: 9656
[startup+480.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1982 0 0 0 47993 12 0 0 25 0 1 0 483447736 10047488 1960 4294967295 134512640 134672761 3221224544 3221223632 134555602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1960 603 41 0 2412 0
vsize: 9812
[startup+490.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1983 0 0 0 48993 12 0 0 25 0 1 0 483447736 10047488 1961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1961 603 41 0 2412 0
vsize: 9812
[startup+500.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1985 0 0 0 49993 12 0 0 25 0 1 0 483447736 10047488 1963 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1963 603 41 0 2412 0
vsize: 9812
[startup+510.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1993 0 0 0 50993 12 0 0 25 0 1 0 483447736 10047488 1971 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1971 603 41 0 2412 0
vsize: 9812
[startup+520.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1994 0 0 0 51993 12 0 0 25 0 1 0 483447736 10047488 1972 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1972 603 41 0 2412 0
vsize: 9812
[startup+530.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1994 0 0 0 52994 12 0 0 25 0 1 0 483447736 10047488 1972 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1972 603 41 0 2412 0
vsize: 9812
[startup+540.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 1995 0 0 0 53994 13 0 0 25 0 1 0 483447736 10047488 1973 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1973 603 41 0 2412 0
vsize: 9812
[startup+550.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2131 0 0 0 54993 13 0 0 25 0 1 0 483447736 10575872 2109 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2109 603 41 0 2541 0
vsize: 10328
[startup+560.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2140 0 0 0 55992 13 0 0 25 0 1 0 483447736 10575872 2118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2118 603 41 0 2541 0
vsize: 10328
[startup+570.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2179 0 0 0 56992 14 0 0 25 0 1 0 483447736 10711040 2157 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2615 2157 603 41 0 2574 0
vsize: 10460
[startup+580.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2184 0 0 0 57992 14 0 0 25 0 1 0 483447736 10711040 2162 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2615 2162 603 41 0 2574 0
vsize: 10460
[startup+590.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2197 0 0 0 58992 14 0 0 25 0 1 0 483447736 10891264 2175 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2175 603 41 0 2618 0
vsize: 10636
[startup+600.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2203 0 0 0 59991 15 0 0 25 0 1 0 483447736 10891264 2181 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2181 603 41 0 2618 0
vsize: 10636
[startup+610.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2204 0 0 0 60991 15 0 0 25 0 1 0 483447736 10891264 2182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2182 603 41 0 2618 0
vsize: 10636
[startup+620.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2210 0 0 0 61991 15 0 0 25 0 1 0 483447736 10891264 2188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2188 603 41 0 2618 0
vsize: 10636
[startup+630.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2211 0 0 0 62991 16 0 0 25 0 1 0 483447736 10891264 2189 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2189 603 41 0 2618 0
vsize: 10636
[startup+640.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2221 0 0 0 63990 16 0 0 25 0 1 0 483447736 10891264 2199 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2199 603 41 0 2618 0
vsize: 10636
[startup+650.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2237 0 0 0 64990 16 0 0 25 0 1 0 483447736 11022336 2215 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2215 603 41 0 2650 0
vsize: 10764
[startup+660.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2241 0 0 0 65990 17 0 0 25 0 1 0 483447736 11022336 2219 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2219 603 41 0 2650 0
vsize: 10764
[startup+670.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2241 0 0 0 66990 17 0 0 25 0 1 0 483447736 11022336 2219 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2219 603 41 0 2650 0
vsize: 10764
[startup+680.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2243 0 0 0 67990 17 0 0 25 0 1 0 483447736 11022336 2221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2221 603 41 0 2650 0
vsize: 10764
[startup+690.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2244 0 0 0 68990 17 0 0 25 0 1 0 483447736 11022336 2222 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2222 603 41 0 2650 0
vsize: 10764
[startup+700.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2244 0 0 0 69989 18 0 0 25 0 1 0 483447736 11022336 2222 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2222 603 41 0 2650 0
vsize: 10764
[startup+710.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2254 0 0 0 70989 18 0 0 25 0 1 0 483447736 11169792 2232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2232 603 41 0 2686 0
vsize: 10908
[startup+720.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2254 0 0 0 71989 18 0 0 25 0 1 0 483447736 11169792 2232 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2232 603 41 0 2686 0
vsize: 10908
[startup+730.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2266 0 0 0 72989 19 0 0 25 0 1 0 483447736 11169792 2244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2244 603 41 0 2686 0
vsize: 10908
[startup+740.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2266 0 0 0 73989 19 0 0 25 0 1 0 483447736 11169792 2244 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2244 603 41 0 2686 0
vsize: 10908
[startup+750.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2266 0 0 0 74989 19 0 0 25 0 1 0 483447736 11169792 2244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2244 603 41 0 2686 0
vsize: 10908
[startup+760.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2276 0 0 0 75989 19 0 0 25 0 1 0 483447736 11169792 2254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2254 603 41 0 2686 0
vsize: 10908
[startup+770.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2276 0 0 0 76988 20 0 0 25 0 1 0 483447736 11169792 2254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2254 603 41 0 2686 0
vsize: 10908
[startup+780.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2277 0 0 0 77989 20 0 0 25 0 1 0 483447736 11169792 2255 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2255 603 41 0 2686 0
vsize: 10908
[startup+790.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2277 0 0 0 78988 20 0 0 25 0 1 0 483447736 11169792 2255 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2255 603 41 0 2686 0
vsize: 10908
[startup+800.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2295 0 0 0 79988 20 0 0 25 0 1 0 483447736 11304960 2273 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2760 2273 603 41 0 2719 0
vsize: 11040
[startup+810.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2372 0 0 0 80988 21 0 0 25 0 1 0 483447736 11571200 2350 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2350 603 41 0 2784 0
vsize: 11300
[startup+820.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2379 0 0 0 81988 21 0 0 25 0 1 0 483447736 11571200 2357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2357 603 41 0 2784 0
vsize: 11300
[startup+830.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2379 0 0 0 82987 21 0 0 25 0 1 0 483447736 11571200 2357 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2357 603 41 0 2784 0
vsize: 11300
[startup+840.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2383 0 0 0 83988 22 0 0 25 0 1 0 483447736 11710464 2361 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2361 603 41 0 2818 0
vsize: 11436
[startup+850.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2387 0 0 0 84987 22 0 0 25 0 1 0 483447736 11710464 2365 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2365 603 41 0 2818 0
vsize: 11436
[startup+860.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2397 0 0 0 85987 22 0 0 25 0 1 0 483447736 11710464 2375 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2375 603 41 0 2818 0
vsize: 11436
[startup+870.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2397 0 0 0 86988 22 0 0 25 0 1 0 483447736 11710464 2375 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2375 603 41 0 2818 0
vsize: 11436
[startup+880.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2399 0 0 0 87988 23 0 0 25 0 1 0 483447736 11710464 2377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2377 603 41 0 2818 0
vsize: 11436
[startup+890.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2409 0 0 0 88988 23 0 0 25 0 1 0 483447736 11857920 2387 4294967295 134512640 134672761 3221224544 3221223800 134562593 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2387 603 41 0 2854 0
vsize: 11580
[startup+900.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2409 0 0 0 89988 23 0 0 25 0 1 0 483447736 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2387 603 41 0 2854 0
vsize: 11580
[startup+910.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2409 0 0 0 90987 23 0 0 25 0 1 0 483447736 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2387 603 41 0 2854 0
vsize: 11580
[startup+920.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2409 0 0 0 91987 24 0 0 25 0 1 0 483447736 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2387 603 41 0 2854 0
vsize: 11580
[startup+930.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2427 0 0 0 92986 24 0 0 25 0 1 0 483447736 11857920 2405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2405 603 41 0 2854 0
vsize: 11580
[startup+940.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2467 0 0 0 93986 24 0 0 25 0 1 0 483447736 12029952 2445 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2445 603 41 0 2896 0
vsize: 11748
[startup+950.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 94986 25 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+960.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 95986 25 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+970.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 96985 26 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+980.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 97985 26 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+990.068 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 98985 26 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 99985 26 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 100985 26 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 101985 26 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 102984 27 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 103984 27 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 104983 28 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 105983 28 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 106983 29 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 107983 29 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 108983 29 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 109982 30 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 110982 30 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 111982 30 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 112984 31 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 113983 31 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 114983 31 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 115983 32 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 116983 32 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 117982 32 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 118982 33 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223280 134565752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19044
Raw data (stat): 19040 (minisat+) R 19039 25285 25284 0 -1 0 2474 0 0 0 119983 33 0 0 25 0 1 0 483447736 12029952 2452 4294967295 134512640 134672761 3221224544 3221223544 1075350251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 19044
Raw data (stat): 19040 (minisat+) Z 19039 25285 25284 0 -1 12 2478 0 0 0 119983 33 0 0 24 0 1 0 483447736 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.13
CPU time (s): 1200.17
CPU user time (s): 1199.83
CPU system time (s): 0.337948
CPU usage (%): 100.004
Max. virtual memory (Kb): 11748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####