PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.02984
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 16420

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 07:10:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13504 boxname=wulflinc30 idbench=1039 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  99657262afbbfce7034a3ec6b29d9b3b  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-lseu.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-lseu.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-lseu.opb
IDLAUNCH: 13504
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        652896 kB
Buffers:         25680 kB
Cached:         324656 kB
SwapCached:          0 kB
Active:         162756 kB
Inactive:       190324 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        652644 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23056 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:30:24 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 13504 7 1200.32 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.93 0.98 0.92 2/54 14617
Raw data (stat): 14617 (runsolver) R 14616 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543169451 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.0013 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 890 0 0 0 996 2 0 0 25 0 1 0 543169451 5287936 868 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1291 868 603 41 0 1250 0
vsize: 5164
[startup+20.0021 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 943 0 0 0 1996 3 0 0 25 0 1 0 543169451 5419008 921 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.0023 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1018 0 0 0 2995 4 0 0 25 0 1 0 543169451 5836800 996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 996 603 41 0 1384 0
vsize: 5700
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1064 0 0 0 3995 4 0 0 25 0 1 0 543169451 5967872 1042 4294967295 134512640 134672761 3221224544 3221223716 134559060 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.0022 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1068 0 0 0 4996 4 0 0 25 0 1 0 543169451 5967872 1046 4294967295 134512640 134672761 3221224544 3221223712 134561382 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.0018 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1137 0 0 0 5995 4 0 0 25 0 1 0 543169451 6238208 1115 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.0019 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1265 0 0 0 6995 4 0 0 25 0 1 0 543169451 6770688 1243 4294967295 134512640 134672761 3221224544 3221223500 1075350256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1653 1243 603 41 0 1612 0
vsize: 6612
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1326 0 0 0 7995 4 0 0 25 0 1 0 543169451 7041024 1304 4294967295 134512640 134672761 3221224544 3221223712 134560858 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.0022 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1326 0 0 0 8995 4 0 0 25 0 1 0 543169451 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.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1326 0 0 0 9995 4 0 0 25 0 1 0 543169451 7041024 1304 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1352 0 0 0 10995 5 0 0 25 0 1 0 543169451 7176192 1330 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1353 0 0 0 11996 5 0 0 25 0 1 0 543169451 7176192 1331 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1353 0 0 0 12996 5 0 0 25 0 1 0 543169451 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1409 0 0 0 13995 5 0 0 25 0 1 0 543169451 7458816 1387 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1821 1387 603 41 0 1780 0
vsize: 7284
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1425 0 0 0 14996 5 0 0 25 0 1 0 543169451 7458816 1403 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1458 0 0 0 15995 5 0 0 25 0 1 0 543169451 7593984 1436 4294967295 134512640 134672761 3221224544 3221223648 134560264 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1508 0 0 0 16995 6 0 0 25 0 1 0 543169451 7864320 1486 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1920 1486 603 41 0 1879 0
vsize: 7680
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1519 0 0 0 17996 6 0 0 25 0 1 0 543169451 7864320 1497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1920 1497 603 41 0 1879 0
vsize: 7680
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1599 0 0 0 18996 6 0 0 25 0 1 0 543169451 8130560 1577 4294967295 134512640 134672761 3221224544 3221223648 134560418 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1610 0 0 0 19996 6 0 0 25 0 1 0 543169451 8290304 1588 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2024 1588 603 41 0 1983 0
vsize: 8096
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1624 0 0 0 20996 6 0 0 25 0 1 0 543169451 8290304 1602 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1681 0 0 0 21996 6 0 0 25 0 1 0 543169451 8552448 1659 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1687 0 0 0 22996 6 0 0 25 0 1 0 543169451 8552448 1665 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1695 0 0 0 23996 6 0 0 25 0 1 0 543169451 8708096 1673 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1714 0 0 0 24996 6 0 0 25 0 1 0 543169451 8708096 1692 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1723 0 0 0 25997 6 0 0 25 0 1 0 543169451 8708096 1701 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1729 0 0 0 26997 6 0 0 25 0 1 0 543169451 8867840 1707 4294967295 134512640 134672761 3221224544 3221223712 134561161 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1740 0 0 0 27997 6 0 0 25 0 1 0 543169451 8867840 1718 4294967295 134512640 134672761 3221224544 3221223712 134560956 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1793 0 0 0 28997 6 0 0 25 0 1 0 543169451 9175040 1771 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1771 603 41 0 2199 0
vsize: 8960
[startup+300.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1802 0 0 0 29997 6 0 0 25 0 1 0 543169451 9175040 1780 4294967295 134512640 134672761 3221224544 3221223648 134560054 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1824 0 0 0 30997 6 0 0 25 0 1 0 543169451 9322496 1802 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2276 1802 603 41 0 2235 0
vsize: 9104
[startup+320.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1828 0 0 0 31997 6 0 0 25 0 1 0 543169451 9322496 1806 4294967295 134512640 134672761 3221224544 3221223440 134565745 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1839 0 0 0 32998 6 0 0 25 0 1 0 543169451 9322496 1817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2276 1817 603 41 0 2235 0
vsize: 9104
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1847 0 0 0 33998 6 0 0 25 0 1 0 543169451 9486336 1825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1825 603 41 0 2275 0
vsize: 9264
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1854 0 0 0 34998 6 0 0 25 0 1 0 543169451 9486336 1832 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1861 0 0 0 35998 6 0 0 25 0 1 0 543169451 9486336 1839 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.005 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1861 0 0 0 36998 6 0 0 25 0 1 0 543169451 9486336 1839 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.006 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1861 0 0 0 37998 6 0 0 25 0 1 0 543169451 9486336 1839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1839 603 41 0 2275 0
vsize: 9264
[startup+390.005 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1869 0 0 0 38998 6 0 0 25 0 1 0 543169451 9486336 1847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2316 1847 603 41 0 2275 0
vsize: 9264
[startup+400.006 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1936 0 0 0 39998 7 0 0 25 0 1 0 543169451 9752576 1914 4294967295 134512640 134672761 3221224544 3221223648 134559862 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.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1955 0 0 0 40998 7 0 0 25 0 1 0 543169451 9887744 1933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1933 603 41 0 2373 0
vsize: 9656
[startup+420.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1963 0 0 0 41999 7 0 0 25 0 1 0 543169451 9887744 1941 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1963 0 0 0 42999 7 0 0 25 0 1 0 543169451 9887744 1941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 1941 603 41 0 2373 0
vsize: 9656
[startup+440.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1964 0 0 0 43999 7 0 0 25 0 1 0 543169451 9887744 1942 4294967295 134512640 134672761 3221224544 3221223648 134560224 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.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1974 0 0 0 44999 7 0 0 25 0 1 0 543169451 9887744 1952 4294967295 134512640 134672761 3221224544 3221223712 134561190 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.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1974 0 0 0 45999 7 0 0 25 0 1 0 543169451 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.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1982 0 0 0 46999 7 0 0 25 0 1 0 543169451 10047488 1960 4294967295 134512640 134672761 3221224544 3221223712 134561060 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.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1982 0 0 0 48000 7 0 0 25 0 1 0 543169451 10047488 1960 4294967295 134512640 134672761 3221224544 3221223648 134560501 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.008 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1985 0 0 0 49000 7 0 0 25 0 1 0 543169451 10047488 1963 4294967295 134512640 134672761 3221224544 3221223712 134560948 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.007 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1993 0 0 0 50000 7 0 0 25 0 1 0 543169451 10047488 1971 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.008 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1993 0 0 0 51000 7 0 0 25 0 1 0 543169451 10047488 1971 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1971 603 41 0 2412 0
vsize: 9812
[startup+520.008 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1994 0 0 0 52000 7 0 0 25 0 1 0 543169451 10047488 1972 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.009 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1995 0 0 0 53001 7 0 0 25 0 1 0 543169451 10047488 1973 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 1973 603 41 0 2412 0
vsize: 9812
[startup+540.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 1995 0 0 0 54000 7 0 0 25 0 1 0 543169451 10047488 1973 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2453 1973 603 41 0 2412 0
vsize: 9812
[startup+550.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2140 0 0 0 55000 8 0 0 25 0 1 0 543169451 10575872 2118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2582 2118 603 41 0 2541 0
vsize: 10328
[startup+560.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2179 0 0 0 55999 8 0 0 25 0 1 0 543169451 10711040 2157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2615 2157 603 41 0 2574 0
vsize: 10460
[startup+570.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2184 0 0 0 56999 9 0 0 25 0 1 0 543169451 10711040 2162 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2615 2162 603 41 0 2574 0
vsize: 10460
[startup+580.011 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2187 0 0 0 57999 9 0 0 25 0 1 0 543169451 10711040 2165 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2615 2165 603 41 0 2574 0
vsize: 10460
[startup+590.012 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2197 0 0 0 58999 9 0 0 25 0 1 0 543169451 10891264 2175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2175 603 41 0 2618 0
vsize: 10636
[startup+600.011 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2203 0 0 0 59999 9 0 0 25 0 1 0 543169451 10891264 2181 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2181 603 41 0 2618 0
vsize: 10636
[startup+610.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2204 0 0 0 60999 9 0 0 25 0 1 0 543169451 10891264 2182 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2182 603 41 0 2618 0
vsize: 10636
[startup+620.012 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2210 0 0 0 61998 10 0 0 25 0 1 0 543169451 10891264 2188 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2188 603 41 0 2618 0
vsize: 10636
[startup+630.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2221 0 0 0 62998 10 0 0 25 0 1 0 543169451 10891264 2199 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2199 603 41 0 2618 0
vsize: 10636
[startup+640.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2221 0 0 0 63998 10 0 0 25 0 1 0 543169451 10891264 2199 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2199 603 41 0 2618 0
vsize: 10636
[startup+650.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2241 0 0 0 64998 11 0 0 25 0 1 0 543169451 11022336 2219 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2691 2219 603 41 0 2650 0
vsize: 10764
[startup+660.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2241 0 0 0 65997 11 0 0 25 0 1 0 543169451 11022336 2219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2691 2219 603 41 0 2650 0
vsize: 10764
[startup+670.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2241 0 0 0 66997 12 0 0 25 0 1 0 543169451 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+680.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2244 0 0 0 67997 12 0 0 25 0 1 0 543169451 11022336 2222 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2244 0 0 0 68998 12 0 0 25 0 1 0 543169451 11022336 2222 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2254 0 0 0 69998 12 0 0 25 0 1 0 543169451 11169792 2232 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2254 0 0 0 70998 12 0 0 25 0 1 0 543169451 11169792 2232 4294967295 134512640 134672761 3221224544 3221223648 134554636 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2264 0 0 0 71998 12 0 0 25 0 1 0 543169451 11169792 2242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2727 2242 603 41 0 2686 0
vsize: 10908
[startup+730.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2266 0 0 0 72998 12 0 0 25 0 1 0 543169451 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2266 0 0 0 73998 12 0 0 25 0 1 0 543169451 11169792 2244 4294967295 134512640 134672761 3221224544 3221223648 134560215 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2276 0 0 0 74999 12 0 0 25 0 1 0 543169451 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+760.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2276 0 0 0 75999 12 0 0 25 0 1 0 543169451 11169792 2254 4294967295 134512640 134672761 3221224544 3221223712 134560996 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2276 0 0 0 76999 12 0 0 25 0 1 0 543169451 11169792 2254 4294967295 134512640 134672761 3221224544 3221223712 134560942 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2277 0 0 0 77999 12 0 0 25 0 1 0 543169451 11169792 2255 4294967295 134512640 134672761 3221224544 3221223712 134561215 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2278 0 0 0 78999 12 0 0 25 0 1 0 543169451 11169792 2256 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2727 2256 603 41 0 2686 0
vsize: 10908
[startup+800.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2372 0 0 0 79998 12 0 0 25 0 1 0 543169451 11571200 2350 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2350 603 41 0 2784 0
vsize: 11300
[startup+810.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2379 0 0 0 80998 12 0 0 25 0 1 0 543169451 11571200 2357 4294967295 134512640 134672761 3221224544 3221223712 134560988 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2379 0 0 0 81998 12 0 0 25 0 1 0 543169451 11571200 2357 4294967295 134512640 134672761 3221224544 3221223712 134560912 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2383 0 0 0 82998 12 0 0 25 0 1 0 543169451 11710464 2361 4294967295 134512640 134672761 3221224544 3221223712 134561218 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2383 0 0 0 83999 12 0 0 25 0 1 0 543169451 11710464 2361 4294967295 134512640 134672761 3221224544 3221223648 134560250 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2397 0 0 0 85000 12 0 0 25 0 1 0 543169451 11710464 2375 4294967295 134512640 134672761 3221224544 3221223712 134560864 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2397 0 0 0 86000 12 0 0 25 0 1 0 543169451 11710464 2375 4294967295 134512640 134672761 3221224544 3221223728 134559161 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2399 0 0 0 87001 12 0 0 25 0 1 0 543169451 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+880.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2409 0 0 0 88001 12 0 0 25 0 1 0 543169451 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+890.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2409 0 0 0 89001 12 0 0 25 0 1 0 543169451 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560888 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2409 0 0 0 90001 12 0 0 25 0 1 0 543169451 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2409 0 0 0 91001 12 0 0 25 0 1 0 543169451 11857920 2387 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2433 0 0 0 92001 12 0 0 25 0 1 0 543169451 11857920 2411 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2411 603 41 0 2854 0
vsize: 11580
[startup+930.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2469 0 0 0 93001 13 0 0 25 0 1 0 543169451 12029952 2447 4294967295 134512640 134672761 3221224544 3221223712 134560895 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 94001 13 0 0 25 0 1 0 543169451 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+950.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 95001 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134559787 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 96001 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 97001 13 0 0 25 0 1 0 543169451 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+980.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 98001 13 0 0 25 0 1 0 543169451 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+990.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 99001 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223648 134560212 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 100001 13 0 0 25 0 1 0 543169451 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 101002 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223668 134566068 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 102002 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560909 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 103002 13 0 0 25 0 1 0 543169451 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 104002 13 0 0 25 0 1 0 543169451 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+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 105002 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223744 134557852 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 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 106003 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560926 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 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 107004 13 0 0 25 0 1 0 543169451 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+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 108004 13 0 0 25 0 1 0 543169451 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 109015 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560926 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 110016 13 0 0 25 0 1 0 543169451 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 111016 13 0 0 25 0 1 0 543169451 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 112016 13 0 0 25 0 1 0 543169451 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+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 113016 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561021 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 114016 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561212 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 115017 13 0 0 25 0 1 0 543169451 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 116017 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 117017 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560909 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2474 0 0 0 118017 13 0 0 25 0 1 0 543169451 12029952 2452 4294967295 134512640 134672761 3221224544 3221223712 134560882 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.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2475 0 0 0 119017 13 0 0 25 0 1 0 543169451 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
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 14617
Raw data (stat): 14617 (minisat+) R 14616 11931 11930 0 -1 0 2475 0 0 0 120018 13 0 0 25 0 1 0 543169451 12029952 2453 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.17 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 14617
Raw data (stat): 14617 (minisat+) Z 14616 11931 11930 0 -1 12 2478 0 0 0 120018 14 0 0 25 0 1 0 543169451 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.17
CPU time (s): 1200.32
CPU user time (s): 1200.18
CPU system time (s): 0.141978
CPU usage (%): 100.013
Max. virtual memory (Kb): 11748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####