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/miplib/normalized-mps-v2-13-7-lseu.opb
MD5SUM	5fcfa2f72175b9723ffb2781fb76fcdc
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.02584
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 15659

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        745528 kB
Buffers:         28256 kB
Cached:         238372 kB
SwapCached:          0 kB
Active:          40256 kB
Inactive:       229112 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        745276 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14152 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:46:28 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 16923 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 % |
c |   1249653 |    9793    34884 |   18164   10568   364724    34.5 | 10.345 % |
#### 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.73 0.90 0.89 2/54 783
Raw data (stat): 783 (runsolver) R 782 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484322852 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.77 0.90 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 904 0 0 0 996 2 0 0 25 0 1 0 484322852 5287936 882 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1291 882 603 41 0 1250 0
vsize: 5164
[startup+20.0016 s]
Raw data (loadavg): 0.81 0.90 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 943 0 0 0 1995 3 0 0 25 0 1 0 484322852 5419008 921 4294967295 134512640 134672761 3221224544 3221223728 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1323 921 603 41 0 1282 0
vsize: 5292
[startup+30.0028 s]
Raw data (loadavg): 0.84 0.91 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1022 0 0 0 2994 3 0 0 25 0 1 0 484322852 5836800 1000 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1000 603 41 0 1384 0
vsize: 5700
[startup+40.0026 s]
Raw data (loadavg): 0.86 0.91 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1064 0 0 0 3994 4 0 0 25 0 1 0 484322852 5967872 1042 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0032 s]
Raw data (loadavg): 0.88 0.91 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1068 0 0 0 4994 4 0 0 25 0 1 0 484322852 5967872 1046 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0037 s]
Raw data (loadavg): 0.90 0.91 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1138 0 0 0 5994 4 0 0 25 0 1 0 484322852 6238208 1116 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1523 1116 603 41 0 1482 0
vsize: 6092
[startup+70.0042 s]
Raw data (loadavg): 0.92 0.92 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1290 0 0 0 6992 5 0 0 25 0 1 0 484322852 6905856 1268 4294967295 134512640 134672761 3221224544 3221223744 134557857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1686 1268 603 41 0 1645 0
vsize: 6744
[startup+80.0048 s]
Raw data (loadavg): 0.93 0.92 0.89 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1326 0 0 0 7992 5 0 0 25 0 1 0 484322852 7041024 1304 4294967295 134512640 134672761 3221224544 3221223712 134560855 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.0053 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1326 0 0 0 8992 5 0 0 25 0 1 0 484322852 7041024 1304 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.006 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1326 0 0 0 9993 5 0 0 25 0 1 0 484322852 7041024 1304 4294967295 134512640 134672761 3221224544 3221223712 134560895 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.006 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1352 0 0 0 10993 5 0 0 25 0 1 0 484322852 7176192 1330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1752 1330 603 41 0 1711 0
vsize: 7008
[startup+120.007 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1353 0 0 0 11993 5 0 0 25 0 1 0 484322852 7176192 1331 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1752 1331 603 41 0 1711 0
vsize: 7008
[startup+130.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1353 0 0 0 12993 5 0 0 25 0 1 0 484322852 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.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1417 0 0 0 13993 5 0 0 25 0 1 0 484322852 7458816 1395 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1821 1395 603 41 0 1780 0
vsize: 7284
[startup+150.008 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1425 0 0 0 14993 5 0 0 25 0 1 0 484322852 7458816 1403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1821 1403 603 41 0 1780 0
vsize: 7284
[startup+160.009 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1458 0 0 0 15993 5 0 0 25 0 1 0 484322852 7593984 1436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1854 1436 603 41 0 1813 0
vsize: 7416
[startup+170.008 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1512 0 0 0 16993 6 0 0 25 0 1 0 484322852 7864320 1490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1920 1490 603 41 0 1879 0
vsize: 7680
[startup+180.009 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1520 0 0 0 17993 6 0 0 25 0 1 0 484322852 7864320 1498 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1920 1498 603 41 0 1879 0
vsize: 7680
[startup+190.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1599 0 0 0 18993 6 0 0 25 0 1 0 484322852 8130560 1577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1985 1577 603 41 0 1944 0
vsize: 7940
[startup+200.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1614 0 0 0 19993 6 0 0 25 0 1 0 484322852 8290304 1592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2024 1592 603 41 0 1983 0
vsize: 8096
[startup+210.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1624 0 0 0 20994 6 0 0 25 0 1 0 484322852 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.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1681 0 0 0 21994 6 0 0 25 0 1 0 484322852 8552448 1659 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1659 603 41 0 2047 0
vsize: 8352
[startup+230.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1687 0 0 0 22994 6 0 0 25 0 1 0 484322852 8552448 1665 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1665 603 41 0 2047 0
vsize: 8352
[startup+240.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1695 0 0 0 23994 6 0 0 25 0 1 0 484322852 8708096 1673 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1673 603 41 0 2085 0
vsize: 8504
[startup+250.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1714 0 0 0 24994 6 0 0 25 0 1 0 484322852 8708096 1692 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1692 603 41 0 2085 0
vsize: 8504
[startup+260.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1723 0 0 0 25994 6 0 0 25 0 1 0 484322852 8708096 1701 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1701 603 41 0 2085 0
vsize: 8504
[startup+270.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1729 0 0 0 26995 6 0 0 25 0 1 0 484322852 8867840 1707 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1707 603 41 0 2124 0
vsize: 8660
[startup+280.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1740 0 0 0 27995 6 0 0 25 0 1 0 484322852 8867840 1718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1718 603 41 0 2124 0
vsize: 8660
[startup+290.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1796 0 0 0 28995 6 0 0 25 0 1 0 484322852 9175040 1774 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1774 603 41 0 2199 0
vsize: 8960
[startup+300.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1802 0 0 0 29995 6 0 0 25 0 1 0 484322852 9175040 1780 4294967295 134512640 134672761 3221224544 3221223648 134560070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1780 603 41 0 2199 0
vsize: 8960
[startup+310.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1825 0 0 0 30995 6 0 0 25 0 1 0 484322852 9322496 1803 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2276 1803 603 41 0 2235 0
vsize: 9104
[startup+320.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1828 0 0 0 31996 6 0 0 25 0 1 0 484322852 9322496 1806 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2276 1806 603 41 0 2235 0
vsize: 9104
[startup+330.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1840 0 0 0 32996 6 0 0 25 0 1 0 484322852 9322496 1818 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2276 1818 603 41 0 2235 0
vsize: 9104
[startup+340.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1854 0 0 0 33996 6 0 0 25 0 1 0 484322852 9486336 1832 4294967295 134512640 134672761 3221224544 3221223712 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1832 603 41 0 2275 0
vsize: 9264
[startup+350.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1854 0 0 0 34996 6 0 0 25 0 1 0 484322852 9486336 1832 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1832 603 41 0 2275 0
vsize: 9264
[startup+360.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1861 0 0 0 35996 6 0 0 25 0 1 0 484322852 9486336 1839 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1839 603 41 0 2275 0
vsize: 9264
[startup+370.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1861 0 0 0 36996 6 0 0 25 0 1 0 484322852 9486336 1839 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1839 603 41 0 2275 0
vsize: 9264
[startup+380.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1862 0 0 0 37997 6 0 0 25 0 1 0 484322852 9486336 1840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1840 603 41 0 2275 0
vsize: 9264
[startup+390.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1881 0 0 0 38997 6 0 0 25 0 1 0 484322852 9617408 1859 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2348 1859 603 41 0 2307 0
vsize: 9392
[startup+400.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1936 0 0 0 39997 6 0 0 25 0 1 0 484322852 9752576 1914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1914 603 41 0 2340 0
vsize: 9524
[startup+410.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1956 0 0 0 40997 7 0 0 25 0 1 0 484322852 9887744 1934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1934 603 41 0 2373 0
vsize: 9656
[startup+420.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1963 0 0 0 41997 7 0 0 25 0 1 0 484322852 9887744 1941 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1941 603 41 0 2373 0
vsize: 9656
[startup+430.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1964 0 0 0 42997 7 0 0 25 0 1 0 484322852 9887744 1942 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1942 603 41 0 2373 0
vsize: 9656
[startup+440.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1964 0 0 0 43998 7 0 0 25 0 1 0 484322852 9887744 1942 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1942 603 41 0 2373 0
vsize: 9656
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1974 0 0 0 44998 7 0 0 25 0 1 0 484322852 9887744 1952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1952 603 41 0 2373 0
vsize: 9656
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1974 0 0 0 45998 7 0 0 25 0 1 0 484322852 9887744 1952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1952 603 41 0 2373 0
vsize: 9656
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1982 0 0 0 46998 7 0 0 25 0 1 0 484322852 10047488 1960 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1960 603 41 0 2412 0
vsize: 9812
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1982 0 0 0 47998 7 0 0 25 0 1 0 484322852 10047488 1960 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1960 603 41 0 2412 0
vsize: 9812
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1985 0 0 0 48999 7 0 0 25 0 1 0 484322852 10047488 1963 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1963 603 41 0 2412 0
vsize: 9812
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1993 0 0 0 49999 7 0 0 25 0 1 0 484322852 10047488 1971 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1971 603 41 0 2412 0
vsize: 9812
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1994 0 0 0 50999 7 0 0 25 0 1 0 484322852 10047488 1972 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1972 603 41 0 2412 0
vsize: 9812
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1994 0 0 0 51999 7 0 0 25 0 1 0 484322852 10047488 1972 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1972 603 41 0 2412 0
vsize: 9812
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 1995 0 0 0 52999 7 0 0 25 0 1 0 484322852 10047488 1973 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1973 603 41 0 2412 0
vsize: 9812
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2048 0 0 0 53998 7 0 0 25 0 1 0 484322852 10178560 2026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2485 2026 603 41 0 2444 0
vsize: 9940
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2140 0 0 0 54998 8 0 0 25 0 1 0 484322852 10575872 2118 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2118 603 41 0 2541 0
vsize: 10328
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2179 0 0 0 55998 8 0 0 25 0 1 0 484322852 10711040 2157 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2615 2157 603 41 0 2574 0
vsize: 10460
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2184 0 0 0 56998 8 0 0 25 0 1 0 484322852 10711040 2162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2615 2162 603 41 0 2574 0
vsize: 10460
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2197 0 0 0 57998 8 0 0 25 0 1 0 484322852 10891264 2175 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2175 603 41 0 2618 0
vsize: 10636
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2197 0 0 0 58999 8 0 0 25 0 1 0 484322852 10891264 2175 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2204 0 0 0 59999 8 0 0 25 0 1 0 484322852 10891264 2182 4294967295 134512640 134672761 3221224544 3221222752 134565813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2182 603 41 0 2618 0
vsize: 10636
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2210 0 0 0 60999 8 0 0 25 0 1 0 484322852 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+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2211 0 0 0 61999 8 0 0 25 0 1 0 484322852 10891264 2189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2189 603 41 0 2618 0
vsize: 10636
[startup+630.027 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2221 0 0 0 62999 8 0 0 25 0 1 0 484322852 10891264 2199 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2199 603 41 0 2618 0
vsize: 10636
[startup+640.027 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2237 0 0 0 63999 8 0 0 25 0 1 0 484322852 11022336 2215 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2215 603 41 0 2650 0
vsize: 10764
[startup+650.027 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2241 0 0 0 65000 8 0 0 25 0 1 0 484322852 11022336 2219 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2219 603 41 0 2650 0
vsize: 10764
[startup+660.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2241 0 0 0 66000 8 0 0 25 0 1 0 484322852 11022336 2219 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2243 0 0 0 67000 8 0 0 25 0 1 0 484322852 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+680.029 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2244 0 0 0 68000 8 0 0 25 0 1 0 484322852 11022336 2222 4294967295 134512640 134672761 3221224544 3221223712 134561081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2691 2222 603 41 0 2650 0
vsize: 10764
[startup+690.029 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2253 0 0 0 69000 8 0 0 25 0 1 0 484322852 11169792 2231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2231 603 41 0 2686 0
vsize: 10908
[startup+700.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2254 0 0 0 70001 8 0 0 25 0 1 0 484322852 11169792 2232 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2232 603 41 0 2686 0
vsize: 10908
[startup+710.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2254 0 0 0 71001 8 0 0 25 0 1 0 484322852 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.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2266 0 0 0 72001 8 0 0 25 0 1 0 484322852 11169792 2244 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2244 603 41 0 2686 0
vsize: 10908
[startup+730.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2266 0 0 0 73001 8 0 0 25 0 1 0 484322852 11169792 2244 4294967295 134512640 134672761 3221224544 3221223712 134561005 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.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2276 0 0 0 74001 8 0 0 25 0 1 0 484322852 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+750.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2276 0 0 0 75001 8 0 0 25 0 1 0 484322852 11169792 2254 4294967295 134512640 134672761 3221224544 3221223728 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2254 603 41 0 2686 0
vsize: 10908
[startup+760.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2276 0 0 0 76002 8 0 0 25 0 1 0 484322852 11169792 2254 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2277 0 0 0 77002 8 0 0 25 0 1 0 484322852 11169792 2255 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2255 603 41 0 2686 0
vsize: 10908
[startup+780.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2277 0 0 0 78002 8 0 0 25 0 1 0 484322852 11169792 2255 4294967295 134512640 134672761 3221224544 3221223712 134561016 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.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2372 0 0 0 79001 9 0 0 25 0 1 0 484322852 11571200 2350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2825 2350 603 41 0 2784 0
vsize: 11300
[startup+800.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2374 0 0 0 80000 9 0 0 25 0 1 0 484322852 11571200 2352 4294967295 134512640 134672761 3221224544 3221223604 1075346562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2352 603 41 0 2784 0
vsize: 11300
[startup+810.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2379 0 0 0 81000 9 0 0 25 0 1 0 484322852 11571200 2357 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2357 603 41 0 2784 0
vsize: 11300
[startup+820.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2379 0 0 0 82001 9 0 0 25 0 1 0 484322852 11571200 2357 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2383 0 0 0 83001 9 0 0 25 0 1 0 484322852 11710464 2361 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2361 603 41 0 2818 0
vsize: 11436
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2388 0 0 0 84001 9 0 0 25 0 1 0 484322852 11710464 2366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2366 603 41 0 2818 0
vsize: 11436
[startup+850.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2397 0 0 0 85001 9 0 0 25 0 1 0 484322852 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+860.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2397 0 0 0 86001 9 0 0 25 0 1 0 484322852 11710464 2375 4294967295 134512640 134672761 3221224544 3221223648 134559862 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.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2409 0 0 0 87001 9 0 0 25 0 1 0 484322852 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2387 603 41 0 2854 0
vsize: 11580
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2409 0 0 0 88002 9 0 0 25 0 1 0 484322852 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2387 603 41 0 2854 0
vsize: 11580
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2409 0 0 0 89002 9 0 0 25 0 1 0 484322852 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2409 0 0 0 90002 9 0 0 25 0 1 0 484322852 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2427 0 0 0 91002 9 0 0 25 0 1 0 484322852 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+920.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2444 0 0 0 92002 9 0 0 25 0 1 0 484322852 12029952 2422 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2422 603 41 0 2896 0
vsize: 11748
[startup+930.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2469 0 0 0 93002 9 0 0 25 0 1 0 484322852 12029952 2447 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2447 603 41 0 2896 0
vsize: 11748
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 94002 9 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2937 2452 603 41 0 2896 0
vsize: 11748
[startup+950.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 95002 9 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560942 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.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 96002 9 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223728 134558648 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.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 97002 9 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 98002 9 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223680 134560647 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 99002 10 0 0 25 0 1 0 484322852 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+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 100002 10 0 0 25 0 1 0 484322852 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+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 101003 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 102003 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 103003 10 0 0 25 0 1 0 484322852 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+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 104003 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560917 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 105003 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134560237 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 106004 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 107004 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223728 134559383 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 108004 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134560057 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 109004 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134554662 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 110004 10 0 0 25 0 1 0 484322852 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+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 111004 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 112005 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560920 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 113005 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 114005 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560892 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 115005 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 116005 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134554636 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 117006 10 0 0 25 0 1 0 484322852 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2474 0 0 0 118006 10 0 0 25 0 1 0 484322852 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2475 0 0 0 119006 10 0 0 25 0 1 0 484322852 12029952 2453 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2453 603 41 0 2896 0
vsize: 11748
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 783
Raw data (stat): 783 (minisat+) R 782 5897 5896 0 -1 0 2475 0 0 0 120006 10 0 0 25 0 1 0 484322852 12029952 2453 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2453 603 41 0 2896 0
vsize: 11748
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 783
Raw data (stat): 783 (minisat+) Z 782 5897 5896 0 -1 12 2478 0 0 0 120006 10 0 0 25 0 1 0 484322852 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.17
CPU user time (s): 1200.07
CPU system time (s): 0.106983
CPU usage (%): 100.01
Max. virtual memory (Kb): 11748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####