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-markshare2.opb
MD5SUM	111dddb6adf389a5275ab413feff6076
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.36
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 21302

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        224656 kB
Buffers:         33520 kB
Cached:         755044 kB
SwapCached:        508 kB
Active:         157588 kB
Inactive:       633108 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        224404 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13744 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:40:03 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 13533 7 1200.21 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.84 0.94 0.91 2/54 7995
Raw data (stat): 7995 (runsolver) R 7994 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490765985 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 1311 0 0 0 995 4 0 0 25 0 1 0 490765985 6991872 1289 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1707 1289 603 41 0 1666 0
vsize: 6828
[startup+20.0019 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 1731 0 0 0 1993 5 0 0 25 0 1 0 490765985 8716288 1709 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2128 1709 603 41 0 2087 0
vsize: 8512
[startup+30.0028 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2122 0 0 0 2992 7 0 0 25 0 1 0 490765985 10317824 2100 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2519 2100 603 41 0 2478 0
vsize: 10076
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2472 0 0 0 3990 9 0 0 25 0 1 0 490765985 11644928 2450 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2843 2450 603 41 0 2802 0
vsize: 11372
[startup+50.0034 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 4990 9 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223712 134559161 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.0043 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 5990 9 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561394 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.0047 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 6989 10 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561164 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.0063 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 7989 10 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+90.0068 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 8989 10 0 0 25 0 1 0 490765985 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+100.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 9989 11 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2665 603 41 0 3048 0
vsize: 12356
[startup+110.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 10989 11 0 0 25 0 1 0 490765985 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+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2688 0 0 0 11988 12 0 0 25 0 1 0 490765985 12652544 2666 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2666 603 41 0 3048 0
vsize: 12356
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2688 0 0 0 12988 12 0 0 25 0 1 0 490765985 12652544 2666 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2666 603 41 0 3048 0
vsize: 12356
[startup+140.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2690 0 0 0 13988 12 0 0 25 0 1 0 490765985 12652544 2668 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2668 603 41 0 3048 0
vsize: 12356
[startup+150.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2690 0 0 0 14987 13 0 0 25 0 1 0 490765985 12652544 2668 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2668 603 41 0 3048 0
vsize: 12356
[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2691 0 0 0 15987 13 0 0 25 0 1 0 490765985 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2669 603 41 0 3048 0
vsize: 12356
[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2691 0 0 0 16987 13 0 0 25 0 1 0 490765985 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2669 603 41 0 3048 0
vsize: 12356
[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2691 0 0 0 17987 14 0 0 25 0 1 0 490765985 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2669 603 41 0 3048 0
vsize: 12356
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2843 0 0 0 18986 15 0 0 25 0 1 0 490765985 13324288 2821 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3253 2821 603 41 0 3212 0
vsize: 13012
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2911 0 0 0 19986 15 0 0 25 0 1 0 490765985 13594624 2889 4294967295 134512640 134672761 3221224528 3221223664 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3319 2889 603 41 0 3278 0
vsize: 13276
[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2913 0 0 0 20986 15 0 0 25 0 1 0 490765985 13594624 2891 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3319 2891 603 41 0 3278 0
vsize: 13276
[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3096 0 0 0 21986 16 0 0 25 0 1 0 490765985 14266368 3074 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3483 3074 603 41 0 3442 0
vsize: 13932
[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3365 0 0 0 22984 18 0 0 25 0 1 0 490765985 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3743 3343 603 41 0 3702 0
vsize: 14972
[startup+240.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3365 0 0 0 23983 18 0 0 25 0 1 0 490765985 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3743 3343 603 41 0 3702 0
vsize: 14972
[startup+250.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3365 0 0 0 24983 19 0 0 25 0 1 0 490765985 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3743 3343 603 41 0 3702 0
vsize: 14972
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3372 0 0 0 25983 19 0 0 25 0 1 0 490765985 15474688 3350 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3778 3350 603 41 0 3737 0
vsize: 15112
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3380 0 0 0 26983 19 0 0 25 0 1 0 490765985 15474688 3358 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3778 3358 603 41 0 3737 0
vsize: 15112
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 27982 19 0 0 25 0 1 0 490765985 15609856 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3811 3379 603 41 0 3770 0
vsize: 15244
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 28982 20 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 29982 20 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 30982 20 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 31982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3810 3379 603 41 0 3769 0
vsize: 15240
[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 32982 21 0 0 25 0 1 0 490765985 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 33982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223712 134558662 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 34982 21 0 0 25 0 1 0 490765985 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+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 35982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561201 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 36982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561011 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 37982 21 0 0 25 0 1 0 490765985 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 38983 21 0 0 25 0 1 0 490765985 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+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 39983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560806 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 40983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223728 134557822 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 41983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223484 1075349891 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 42983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561215 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3494 0 0 0 43983 21 0 0 25 0 1 0 490765985 15867904 3472 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3472 603 41 0 3833 0
vsize: 15496
[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3789 0 0 0 44983 22 0 0 25 0 1 0 490765985 17199104 3767 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4199 3767 603 41 0 4158 0
vsize: 16796
[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4066 0 0 0 45983 22 0 0 25 0 1 0 490765985 18264064 4044 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4459 4044 603 41 0 4418 0
vsize: 17836
[startup+470.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4128 0 0 0 46982 23 0 0 25 0 1 0 490765985 18530304 4106 4294967295 134512640 134672761 3221224528 3221223664 134565098 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4128 0 0 0 47982 23 0 0 25 0 1 0 490765985 18530304 4106 4294967295 134512640 134672761 3221224528 3221223696 134560892 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4130 0 0 0 48982 23 0 0 25 0 1 0 490765985 18530304 4108 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4524 4108 603 41 0 4483 0
vsize: 18096
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4142 0 0 0 49983 23 0 0 25 0 1 0 490765985 18669568 4120 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4558 4120 603 41 0 4517 0
vsize: 18232
[startup+510.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4244 0 0 0 50983 23 0 0 25 0 1 0 490765985 19066880 4222 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4655 4222 603 41 0 4614 0
vsize: 18620
[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 51983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223632 134560410 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 52983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134561382 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 53983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 54983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223600 134565153 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 55983 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560956 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 56984 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560869 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 57985 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561385 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 58985 23 0 0 25 0 1 0 490765985 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+600.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 59986 23 0 0 25 0 1 0 490765985 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+610.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 60986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560917 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 61986 23 0 0 25 0 1 0 490765985 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+630.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 62986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560920 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 63986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561027 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 64987 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560895 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 65985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4687 4282 603 41 0 4646 0
vsize: 18748
[startup+670.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 66985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223712 134559405 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 67985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223712 134559538 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 68985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561151 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 69985 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223828 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4456 603 41 0 4841 0
vsize: 19528
[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 70986 24 0 0 25 0 1 0 490765985 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+720.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 71986 24 0 0 25 0 1 0 490765985 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+730.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 72986 24 0 0 25 0 1 0 490765985 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.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 73986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560979 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.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 74986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561154 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.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 75986 24 0 0 25 0 1 0 490765985 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+770.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 76986 24 0 0 25 0 1 0 490765985 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+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 77987 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561385 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.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 78987 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561207 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.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 79987 24 0 0 25 0 1 0 490765985 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+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 80987 24 0 0 25 0 1 0 490765985 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 81988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223712 134559405 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 82988 24 0 0 25 0 1 0 490765985 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+840.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 83988 24 0 0 25 0 1 0 490765985 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 84988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560852 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 85988 24 0 0 25 0 1 0 490765985 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 86988 24 0 0 25 0 1 0 490765985 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 87989 24 0 0 25 0 1 0 490765985 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 88989 24 0 0 25 0 1 0 490765985 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+900.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 89989 24 0 0 25 0 1 0 490765985 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 90990 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561154 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 91990 24 0 0 25 0 1 0 490765985 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+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 92990 24 0 0 25 0 1 0 490765985 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+940.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 93990 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561400 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 94991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560940 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 95991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561385 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 96991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560917 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 97991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561018 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 98991 24 0 0 25 0 1 0 490765985 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+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 99992 24 0 0 25 0 1 0 490765985 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+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 100992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561005 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 101992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560852 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 102992 24 0 0 25 0 1 0 490765985 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+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 103992 24 0 0 25 0 1 0 490765985 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+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 104993 24 0 0 25 0 1 0 490765985 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 105993 24 0 0 25 0 1 0 490765985 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+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 106993 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4946 4491 603 41 0 4905 0
vsize: 19784
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 107993 24 0 0 25 0 1 0 490765985 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+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 108993 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560929 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 109993 24 0 0 25 0 1 0 490765985 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+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 110994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223632 134560218 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 111994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223712 134559161 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 112994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560912 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 113994 24 0 0 25 0 1 0 490765985 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+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 114994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223632 134560196 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 115995 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223664 134560598 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 116995 24 0 0 25 0 1 0 490765985 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+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 117994 24 0 0 25 0 1 0 490765985 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+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4687 0 0 0 118994 25 0 0 25 0 1 0 490765985 20926464 4665 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5109 4665 603 41 0 5068 0
vsize: 20436
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7995
Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4687 0 0 0 119994 25 0 0 25 0 1 0 490765985 20926464 4665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5109 4665 603 41 0 5068 0
vsize: 20436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7995
Raw data (stat): 7995 (minisat+) Z 7994 25285 25284 0 -1 12 4690 0 0 0 119994 26 0 0 25 0 1 0 490765985 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.09
CPU time (s): 1200.21
CPU user time (s): 1199.94
CPU system time (s): 0.264959
CPU usage (%): 100.01
Max. virtual memory (Kb): 20436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####