PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	c00b2eef1eabd5880b83093b756a5dd4
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	429056
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.34
Number of variables	270
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	90
Trace number 21784

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-22 00:57:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12662 boxname=wulflinc27 idbench=974 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c00b2eef1eabd5880b83093b756a5dd4  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-markshare2.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 12662
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
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:        561096 kB
Buffers:         18996 kB
Cached:         431932 kB
SwapCached:        524 kB
Active:          80508 kB
Inactive:       372348 kB
HighTotal:      131008 kB
HighFree:         4564 kB
LowTotal:       903652 kB
LowFree:        556532 kB
SwapTotal:     2097892 kB
SwapFree:      2096452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5088 kB
Slab:            14928 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:17:28 (client local time) WITH STATUS 10 IN 1200.58 SECONDS
stats: 12662 7 1200.58 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 3452927   bits: 23/22
c ---[  10]---> Adder-cost: 380   maxlim: 3689471   bits: 23/22
c ---[   8]---> Adder-cost: 350   maxlim: 3561471   bits: 23/22
c ---[   6]---> Adder-cost: 340   maxlim: 3823615   bits: 23/22
c ---[   4]---> Adder-cost: 390   maxlim: 3614719   bits: 23/22
c ---[   2]---> Adder-cost: 358   maxlim: 3749887   bits: 23/22
c ---[   0]---> Adder-cost: 374   maxlim: 3556351   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17222    61228 |    6314     100      354     3.5 | 12.727 % |
c |       250 |   17214    61202 |    6945     249     1122     4.5 | 12.761 % |
c ==============================================================================
c [1mFound solution: 7023616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       344 |   20137    68094 |    6712     343     1819     5.3 | 12.761 % |
c |       444 |   20137    68094 |    7383     443    12460    28.1 |  9.716 % |
c |       594 |   20129    68068 |    8121     592    32128    54.3 |  9.742 % |
c ==============================================================================
c [1mFound solution: 6494208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       701 |   20179    68196 |    6726     698    39584    56.7 |  9.742 % |
c ==============================================================================
c [1mFound solution: 6488064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       765 |   20197    68242 |    6732     762    49821    65.4 |  9.742 % |
c ==============================================================================
c [1mFound solution: 6160384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       788 |   20216    68289 |    6738     785    50389    64.2 |  9.742 % |
c ==============================================================================
c [1mFound solution: 5926912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       855 |   20240    68347 |    6746     852    61121    71.7 |  9.742 % |
c |       957 |   20240    68347 |    7420     954    74178    77.8 |  9.794 % |
c |      1108 |   20232    68321 |    8162    1104    93548    84.7 |  9.820 % |
c |      1333 |   20232    68321 |    8978    1329   120525    90.7 |  9.820 % |
c |      1672 |   20232    68321 |    9876    1668   139880    83.9 |  9.820 % |
c ==============================================================================
c [1mFound solution: 5922816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1696 |   20253    68372 |    6751    1692   142492    84.2 |  9.820 % |
c ==============================================================================
c [1mFound solution: 5918720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1764 |   20277    68430 |    6759    1760   150818    85.7 |  9.820 % |
c |      1865 |   20277    68430 |    7434    1861   160047    86.0 |  9.833 % |
c |      2015 |   20277    68430 |    8178    2011   171202    85.1 |  9.833 % |
c |      2240 |   20277    68430 |    8996    2236   190935    85.4 |  9.833 % |
c ==============================================================================
c [1mFound solution: 5232640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2385 |   20301    68492 |    6767    2381   203817    85.6 |  9.833 % |
c |      2485 |   20301    68492 |    7443    2481   212464    85.6 |  9.841 % |
c |      2636 |   20301    68492 |    8188    2632   227536    86.4 |  9.841 % |
c ==============================================================================
c [1mFound solution: 4543488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2817 |   20332    68567 |    6777    2813   235715    83.8 |  9.841 % |
c ==============================================================================
c [1mFound solution: 4190208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2907 |   20341    68592 |    6780    2903   239840    82.6 |  9.841 % |
c |      3008 |   20341    68592 |    7458    3004   253054    84.2 |  9.862 % |
c |      3160 |   20341    68592 |    8203    3156   264777    83.9 |  9.862 % |
c |      3386 |   20333    68566 |    9024    3381   282561    83.6 |  9.887 % |
c |      3724 |   20333    68566 |    9926    3719   308609    83.0 |  9.887 % |
c |      4230 |   20325    68540 |   10919    4224   359168    85.0 |  9.912 % |
c |      4991 |   20317    68514 |   12011    4984   448360    90.0 |  9.937 % |
c |      6131 |   20309    68488 |   13212    6123   544455    88.9 |  9.962 % |
c |      7840 |   20301    68462 |   14533    7831   756142    96.6 |  9.987 % |
c |     10402 |   20269    68358 |   15986   10389  1034854    99.6 | 10.088 % |
c |     14246 |   20253    68306 |   17585   14231  1313201    92.3 | 10.138 % |
c ==============================================================================
c [1mFound solution: 3871744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17662 |   20280    68371 |    6760   17647  1712464    97.0 | 10.138 % |
c |     17762 |   20280    68371 |    7436    4512   392059    86.9 | 10.141 % |
c |     17913 |   20280    68371 |    8179    4663   405086    86.9 | 10.141 % |
c |     18139 |   20280    68371 |    8997    4889   423670    86.7 | 10.141 % |
c |     18477 |   20280    68371 |    9897    5227   454333    86.9 | 10.141 % |
c |     18984 |   20280    68371 |   10887    5734   495202    86.4 | 10.141 % |
c |     19744 |   20280    68371 |   11975    6494   570493    87.8 | 10.141 % |
c |     20884 |   20280    68371 |   13173    7634   623596    81.7 | 10.141 % |
c |     22592 |   20266    68327 |   14490    9340   765876    82.0 | 10.191 % |
c ==============================================================================
c [1mFound solution: 3836928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24403 |   20295    68396 |    6765   11151   886232    79.5 | 10.191 % |
c |     24503 |   20295    68396 |    7441    5676   320244    56.4 | 10.190 % |
c |     24654 |   20295    68396 |    8185    5827   331873    57.0 | 10.190 % |
c |     24879 |   20295    68396 |    9004    6052   354549    58.6 | 10.190 % |
c |     25218 |   20295    68396 |    9904    6391   379680    59.4 | 10.190 % |
c |     25724 |   20295    68396 |   10895    6897   398476    57.8 | 10.190 % |
c |     26483 |   20295    68396 |   11984    7656   486672    63.6 | 10.190 % |
c |     27624 |   20295    68396 |   13183    8797   548152    62.3 | 10.190 % |
c |     29333 |   20288    68380 |   14501   10505   700085    66.6 | 10.215 % |
c ==============================================================================
c [1mFound solution: 3792896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30965 |   20302    68414 |    6767   12137   892437    73.5 | 10.215 % |
c |     31066 |   20302    68414 |    7443    6170   432933    70.2 | 10.228 % |
c |     31218 |   20302    68414 |    8188    6322   437963    69.3 | 10.228 % |
c |     31444 |   20302    68414 |    9006    6548   459010    70.1 | 10.228 % |
c |     31781 |   20302    68414 |    9907    6885   474941    69.0 | 10.228 % |
c |     32287 |   20302    68414 |   10898    7391   516443    69.9 | 10.228 % |
c |     33046 |   20302    68414 |   11988    8150   564384    69.2 | 10.228 % |
c |     34185 |   20302    68414 |   13186    9289   661071    71.2 | 10.228 % |
c ==============================================================================
c [1mFound solution: 3509248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35428 |   20307    68419 |    6769   10531   710963    67.5 | 10.228 % |
c |     35530 |   20307    68419 |    7445    5368   259347    48.3 | 10.265 % |
c |     35682 |   20307    68419 |    8190    5520   269127    48.8 | 10.265 % |
c |     35907 |   20307    68419 |    9009    5745   281440    49.0 | 10.265 % |
c |     36245 |   20307    68419 |    9910    6083   308126    50.7 | 10.265 % |
c |     36751 |   20307    68419 |   10901    6589   333711    50.6 | 10.265 % |
c |     37510 |   20307    68419 |   11991    7348   385155    52.4 | 10.265 % |
c |     38649 |   20307    68419 |   13190    8487   441397    52.0 | 10.265 % |
c |     40359 |   20307    68419 |   14509   10197   558964    54.8 | 10.265 % |
c |     42921 |   20307    68419 |   15960   12759   841784    66.0 | 10.265 % |
c |     46767 |   20307    68419 |   17557   16605  1186457    71.5 | 10.265 % |
c |     52533 |   20307    68419 |   19312   12796   894451    69.9 | 10.265 % |
c |     61182 |   20307    68419 |   21244   11191   693224    61.9 | 10.265 % |
c |     74157 |   20307    68419 |   23368   13001   715476    55.0 | 10.265 % |
c |     93619 |   20307    68419 |   25705   20163  1499595    74.4 | 10.265 % |
c ==============================================================================
c [1mFound solution: 3228672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119436 |   20314    68426 |    6771   18890  1282179    67.9 | 10.265 % |
c |    119537 |   20314    68426 |    7448    4824   243711    50.5 | 10.322 % |
c |    119688 |   20314    68426 |    8192    4975   248947    50.0 | 10.322 % |
c |    119914 |   20314    68426 |    9012    5201   262506    50.5 | 10.322 % |
c |    120252 |   20314    68426 |    9913    5539   286002    51.6 | 10.322 % |
c |    120760 |   20314    68426 |   10904    6047   307590    50.9 | 10.322 % |
c |    121521 |   20314    68426 |   11995    6808   353352    51.9 | 10.322 % |
c |    122662 |   20314    68426 |   13194    7949   493941    62.1 | 10.322 % |
c |    124371 |   20314    68426 |   14514    9658   639691    66.2 | 10.322 % |
c |    126933 |   20314    68426 |   15965   12220   865667    70.8 | 10.322 % |
c |    130778 |   20314    68426 |   17562   16065  1113387    69.3 | 10.322 % |
c |    136544 |   20307    68411 |   19318   12438   673798    54.2 | 10.371 % |
c |    145194 |   20307    68411 |   21250   10739  1086432   101.2 | 10.371 % |
c |    158171 |   20299    68389 |   23375   12512   692110    55.3 | 10.421 % |
c |    177632 |   20286    68361 |   25712   19588  1743706    89.0 | 10.521 % |
c |    206825 |   20286    68361 |   28284   21608  1986898    92.0 | 10.521 % |
c |    250615 |   20259    68296 |   31112   17604  1442774    82.0 | 10.671 % |
c ==============================================================================
c [1mFound solution: 3090432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    265322 |   20259    68302 |    6753   14118  1121736    79.5 | 10.671 % |
c |    265422 |   20259    68302 |    7428    7159   474900    66.3 | 10.804 % |
c |    265573 |   20259    68302 |    8171    7310   479753    65.6 | 10.804 % |
c |    265801 |   20259    68302 |    8988    7538   483583    64.2 | 10.804 % |
c |    266138 |   20259    68302 |    9887    7875   491646    62.4 | 10.804 % |
c ==============================================================================
c [1mFound solution: 3012608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    266412 |   20277    68348 |    6759    8149   497096    61.0 | 10.804 % |
c |    266512 |   20277    68348 |    7434    4175   128007    30.7 | 10.816 % |
c |    266663 |   20277    68348 |    8178    4326   131572    30.4 | 10.816 % |
c |    266888 |   20277    68348 |    8996    4551   138163    30.4 | 10.816 % |
c |    267229 |   20277    68348 |    9895    4892   143487    29.3 | 10.816 % |
c ==============================================================================
c [1mFound solution: 2960384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    267434 |   20291    68382 |    6763    5097   153533    30.1 | 10.816 % |
c |    267536 |   20291    68382 |    7439    5199   161846    31.1 | 10.827 % |
c |    267686 |   20291    68382 |    8183    5349   170477    31.9 | 10.827 % |
c |    267911 |   20282    68355 |    9001    5573   185872    33.4 | 10.877 % |
c |    268248 |   20282    68355 |    9901    5910   206816    35.0 | 10.877 % |
c |    268757 |   20282    68355 |   10891    6419   230843    36.0 | 10.877 % |
c |    269516 |   20282    68355 |   11981    7178   288249    40.2 | 10.877 % |
c |    270655 |   20282    68355 |   13179    8317   367200    44.2 | 10.877 % |
c ==============================================================================
c [1mFound solution: 2712576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    272032 |   20294    68379 |    6764    9693   444611    45.9 | 10.877 % |
c |    272132 |   20294    68379 |    7440    4947   203000    41.0 | 10.932 % |
c |    272282 |   20294    68379 |    8184    5097   209884    41.2 | 10.932 % |
c |    272509 |   20294    68379 |    9002    5324   216068    40.6 | 10.932 % |
c |    272848 |   20294    68379 |    9903    5663   252577    44.6 | 10.932 % |
c |    273355 |   20294    68379 |   10893    6170   273314    44.3 | 10.932 % |
c |    274115 |   20294    68379 |   11982    6930   354800    51.2 | 10.932 % |
c |    275254 |   20294    68379 |   13181    8069   427580    53.0 | 10.932 % |
c ==============================================================================
c [1mFound solution: 2147328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    275572 |   20305    68408 |    6768    8387   431860    51.5 | 10.932 % |
c |    275672 |   20305    68408 |    7444    4294   182758    42.6 | 10.949 % |
c |    275823 |   20305    68408 |    8189    4445   202925    45.7 | 10.949 % |
c |    276049 |   20305    68408 |    9008    4671   216826    46.4 | 10.949 % |
c |    276388 |   20305    68408 |    9909    5010   225188    44.9 | 10.949 % |
c |    276894 |   20305    68408 |   10899    5516   247985    45.0 | 10.949 % |
c |    277655 |   20305    68408 |   11989    6277   305413    48.7 | 10.949 % |
c |    278794 |   20305    68408 |   13188    7416   357800    48.2 | 10.949 % |
c |    280502 |   20305    68408 |   14507    9124   461871    50.6 | 10.949 % |
c |    283065 |   20305    68408 |   15958   11687   710315    60.8 | 10.949 % |
c |    286909 |   20305    68408 |   17554   15531   911059    58.7 | 10.949 % |
c |    292676 |   20292    68378 |   19309   11981   580839    48.5 | 11.048 % |
c |    301325 |   20292    68378 |   21240   10402   676281    65.0 | 11.048 % |
c |    314300 |   20292    68378 |   23364   12071   790578    65.5 | 11.048 % |
c |    333763 |   20273    68335 |   25701   19251  1138815    59.2 | 11.196 % |
c |    362955 |   20259    68295 |   28271   20901   970705    46.4 | 11.271 % |
c |    406746 |   20259    68295 |   31098   19932   977282    49.0 | 11.271 % |
c |    472430 |   20230    68231 |   34208   29183  1453573    49.8 | 11.469 % |
#### 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.65 0.85 0.89 2/54 31687
Raw data (stat): 31687 (runsolver) R 31686 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549572684 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0143 s]
Raw data (loadavg): 0.79 0.87 0.89 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 1319 0 0 0 996 3 0 0 25 0 1 0 549572684 6991872 1297 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1707 1297 603 41 0 1666 0
vsize: 6828
[startup+20.1547 s]
Raw data (loadavg): 0.82 0.88 0.89 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 1744 0 0 0 2008 5 0 0 25 0 1 0 549572684 8716288 1722 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1722 603 41 0 2087 0
vsize: 8512
[startup+30.1547 s]
Raw data (loadavg): 0.85 0.88 0.89 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2135 0 0 0 3004 7 0 0 25 0 1 0 549572684 10317824 2113 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2519 2113 603 41 0 2478 0
vsize: 10076
[startup+40.1611 s]
Raw data (loadavg): 0.87 0.88 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2488 0 0 0 4002 8 0 0 25 0 1 0 549572684 11780096 2466 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2876 2466 603 41 0 2835 0
vsize: 11504
[startup+50.1733 s]
Raw data (loadavg): 0.89 0.89 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 5003 9 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+60.1742 s]
Raw data (loadavg): 0.91 0.89 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 6002 9 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+70.1754 s]
Raw data (loadavg): 0.92 0.89 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 7001 10 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+80.1756 s]
Raw data (loadavg): 0.93 0.90 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 8001 10 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+90.1806 s]
Raw data (loadavg): 0.94 0.90 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 9001 10 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+100.181 s]
Raw data (loadavg): 0.95 0.90 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 10001 10 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223712 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+110.18 s]
Raw data (loadavg): 0.96 0.90 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2687 0 0 0 11001 11 0 0 25 0 1 0 549572684 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+120.181 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2688 0 0 0 12002 11 0 0 25 0 1 0 549572684 12652544 2666 4294967295 134512640 134672761 3221224528 3221223664 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2666 603 41 0 3048 0
vsize: 12356
[startup+130.181 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2688 0 0 0 13002 11 0 0 25 0 1 0 549572684 12652544 2666 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2666 603 41 0 3048 0
vsize: 12356
[startup+140.181 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2690 0 0 0 14002 11 0 0 25 0 1 0 549572684 12652544 2668 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2668 603 41 0 3048 0
vsize: 12356
[startup+150.288 s]
Raw data (loadavg): 0.98 0.91 0.91 2/54 31687
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2690 0 0 0 15013 11 0 0 25 0 1 0 549572684 12652544 2668 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2668 603 41 0 3048 0
vsize: 12356
[startup+160.288 s]
Raw data (loadavg): 0.98 0.92 0.91 2/55 31688
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2691 0 0 0 16013 11 0 0 25 0 1 0 549572684 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2669 603 41 0 3048 0
vsize: 12356
[startup+170.3 s]
Raw data (loadavg): 1.06 0.94 0.91 2/56 31723
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2691 0 0 0 17013 11 0 0 25 0 1 0 549572684 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2669 603 41 0 3048 0
vsize: 12356
[startup+180.313 s]
Raw data (loadavg): 1.13 0.95 0.92 2/54 31740
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2691 0 0 0 18015 11 0 0 25 0 1 0 549572684 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2669 603 41 0 3048 0
vsize: 12356
[startup+190.313 s]
Raw data (loadavg): 1.11 0.95 0.92 2/54 31740
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2862 0 0 0 19014 12 0 0 25 0 1 0 549572684 13324288 2840 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3253 2840 603 41 0 3212 0
vsize: 13012
[startup+200.313 s]
Raw data (loadavg): 1.09 0.96 0.92 2/54 31740
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2911 0 0 0 20014 12 0 0 25 0 1 0 549572684 13594624 2889 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3319 2889 603 41 0 3278 0
vsize: 13276
[startup+210.312 s]
Raw data (loadavg): 1.08 0.96 0.92 2/54 31740
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 2913 0 0 0 21014 12 0 0 25 0 1 0 549572684 13594624 2891 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3319 2891 603 41 0 3278 0
vsize: 13276
[startup+220.32 s]
Raw data (loadavg): 1.06 0.96 0.92 2/54 31740
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3110 0 0 0 22014 13 0 0 25 0 1 0 549572684 14401536 3088 4294967295 134512640 134672761 3221224528 3221223696 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3088 603 41 0 3475 0
vsize: 14064
[startup+230.325 s]
Raw data (loadavg): 1.05 0.96 0.92 2/54 31740
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3365 0 0 0 23013 14 0 0 25 0 1 0 549572684 15331328 3343 4294967295 134512640 134672761 3221224528 3221223712 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3743 3343 603 41 0 3702 0
vsize: 14972
[startup+240.324 s]
Raw data (loadavg): 1.04 0.96 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3365 0 0 0 24013 14 0 0 25 0 1 0 549572684 15331328 3343 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3743 3343 603 41 0 3702 0
vsize: 14972
[startup+250.325 s]
Raw data (loadavg): 1.04 0.96 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3365 0 0 0 25014 14 0 0 25 0 1 0 549572684 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3743 3343 603 41 0 3702 0
vsize: 14972
[startup+260.325 s]
Raw data (loadavg): 1.03 0.96 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3372 0 0 0 26014 15 0 0 25 0 1 0 549572684 15474688 3350 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3778 3350 603 41 0 3737 0
vsize: 15112
[startup+270.325 s]
Raw data (loadavg): 1.03 0.96 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3380 0 0 0 27014 15 0 0 25 0 1 0 549572684 15474688 3358 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3778 3358 603 41 0 3737 0
vsize: 15112
[startup+280.325 s]
Raw data (loadavg): 1.02 0.96 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 28014 15 0 0 25 0 1 0 549572684 15609856 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3379 603 41 0 3770 0
vsize: 15244
[startup+290.329 s]
Raw data (loadavg): 1.02 0.96 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 29014 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223664 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+300.329 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 30015 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223664 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+310.329 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 31015 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+320.33 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 32015 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+330.329 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 33015 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+340.329 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 34015 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223728 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+350.33 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 35015 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223712 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+360.33 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 36016 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+370.33 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 37016 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+380.334 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 38016 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+390.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 39026 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+400.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 40027 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+410.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 41026 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+420.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 42027 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223664 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+430.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3401 0 0 0 43027 15 0 0 25 0 1 0 549572684 15605760 3379 4294967295 134512640 134672761 3221224528 3221223680 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+440.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3434 0 0 0 44027 16 0 0 25 0 1 0 549572684 15736832 3412 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3842 3412 603 41 0 3801 0
vsize: 15368
[startup+450.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 3734 0 0 0 45026 17 0 0 25 0 1 0 549572684 16932864 3712 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4134 3712 603 41 0 4093 0
vsize: 16536
[startup+460.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4006 0 0 0 46025 18 0 0 25 0 1 0 549572684 17997824 3984 4294967295 134512640 134672761 3221224528 3221223448 1075351202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4394 3984 603 41 0 4353 0
vsize: 17576
[startup+470.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4128 0 0 0 47025 18 0 0 25 0 1 0 549572684 18530304 4106 4294967295 134512640 134672761 3221224528 3221223712 134558553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4524 4106 603 41 0 4483 0
vsize: 18096
[startup+480.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4128 0 0 0 48025 18 0 0 25 0 1 0 549572684 18530304 4106 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4524 4106 603 41 0 4483 0
vsize: 18096
[startup+490.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31742
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4128 0 0 0 49025 18 0 0 25 0 1 0 549572684 18530304 4106 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4524 4106 603 41 0 4483 0
vsize: 18096
[startup+500.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4137 0 0 0 50025 18 0 0 25 0 1 0 549572684 18530304 4115 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4524 4115 603 41 0 4483 0
vsize: 18096
[startup+510.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4162 0 0 0 51025 18 0 0 25 0 1 0 549572684 18669568 4140 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4558 4140 603 41 0 4517 0
vsize: 18232
[startup+520.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4301 0 0 0 52025 19 0 0 25 0 1 0 549572684 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4279 603 41 0 4646 0
vsize: 18748
[startup+530.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4301 0 0 0 53025 19 0 0 25 0 1 0 549572684 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4279 603 41 0 4646 0
vsize: 18748
[startup+540.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4301 0 0 0 54025 19 0 0 25 0 1 0 549572684 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4279 603 41 0 4646 0
vsize: 18748
[startup+550.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4301 0 0 0 55025 19 0 0 25 0 1 0 549572684 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4279 603 41 0 4646 0
vsize: 18748
[startup+560.436 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 56025 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+570.437 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 57025 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223728 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+580.437 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 58026 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+590.437 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 59026 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+600.438 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 60026 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+610.437 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 61026 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+620.438 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 62026 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+630.439 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 63027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+640.439 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 64027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+650.439 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 65027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+660.439 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 66027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+670.439 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 67027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+680.439 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 68027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+690.439 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4304 0 0 0 69027 19 0 0 25 0 1 0 549572684 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+700.44 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4359 0 0 0 70028 19 0 0 25 0 1 0 549572684 19464192 4337 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4752 4337 603 41 0 4711 0
vsize: 19008
[startup+710.44 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 71027 20 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+720.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 72027 20 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+730.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 73027 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+740.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 74027 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+750.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 75027 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223664 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+760.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 76028 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+770.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 77028 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+780.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 78028 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+790.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 79028 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+800.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 80028 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+810.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 81028 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+820.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 82029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+830.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 83029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+840.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 84029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+850.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 85029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+860.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 86029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+870.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 87029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+880.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 88029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+890.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 89029 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+900.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 90030 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+910.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 91030 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+920.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 92030 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+930.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 93030 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+940.441 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 94030 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+950.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 95030 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+960.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 96031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+970.443 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 97031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+980.443 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 98031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+990.442 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 99031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1000.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 100031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1010.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 101031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1020.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 102031 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1030.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 103032 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223664 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1040.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 104032 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1050.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 105032 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1060.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 106032 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1070.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4478 0 0 0 107032 21 0 0 25 0 1 0 549572684 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+1080.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 108032 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1090.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 109032 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1100.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 110032 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1110.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 111032 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1120.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 112033 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1130.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 113033 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1140.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 114033 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1150.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 115033 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1160.44 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 116033 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1170.45 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 117034 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1180.45 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 118034 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1190.45 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4513 0 0 0 119034 22 0 0 25 0 1 0 549572684 20258816 4491 4294967295 134512640 134672761 3221224528 3221223712 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1200.45 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31744
Raw data (stat): 31687 (minisat+) R 31686 18865 18864 0 -1 0 4664 0 0 0 120034 22 0 0 25 0 1 0 549572684 20791296 4642 4294967295 134512640 134672761 3221224528 3221223680 134560074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5076 4642 603 41 0 5035 0
vsize: 20304
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.46 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 31744
Raw data (stat): 31687 (minisat+) Z 31686 18865 18864 0 -1 12 4667 0 0 0 120034 23 0 0 25 0 1 0 549572684 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.46
CPU time (s): 1200.58
CPU user time (s): 1200.34
CPU system time (s): 0.237963
CPU usage (%): 100.01
Max. virtual memory (Kb): 20304
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####