PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen2.opb
MD5SUM	30256c883dd8af773c334a2b26410bd9
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	9400
Biggest coefficient in the objective function	2494038016
Number of bits for the biggest coefficient in the objective function	32
Sum of the numbers in the objective function	391862963250
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	2494038016
Number of bits of the biggest number in a constraint	32
Biggest sum of numbers in a constraint	391862963250
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.092985
Number of variables	10680
Total number of constraints	444
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	40
Maximum length of a constraint	1700
Trace number 16221

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 06:31:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15691 boxname=wulflinc13 idbench=1207 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  30256c883dd8af773c334a2b26410bd9  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb
IDLAUNCH: 15691
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        756808 kB
Buffers:         33736 kB
Cached:         221360 kB
SwapCached:        176 kB
Active:          66224 kB
Inactive:       191624 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        756556 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            14352 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:51:38 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 15691 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 665 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[ 667]---> Adder-cost: 1514   maxlim: 182446   bits: 18/18
c ---[ 666]---> Adder-cost: 1514   maxlim: 103596   bits: 17/17
c ---[ 665]---> Adder-cost: 1168   maxlim: 90177   bits: 17/17
c ---[ 663]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 659]---> Adder-cost: 256   maxlim: 2167   bits: 13/12
c ---[ 657]---> Adder-cost: 256   maxlim: 2295   bits: 13/12
c ---[ 655]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 647]---> Adder-cost: 496   maxlim: 4335   bits: 13/13
c ---[ 645]---> Adder-cost: 528   maxlim: 4335   bits: 14/13
c ---[ 643]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 639]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 637]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 635]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 631]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 629]---> Adder-cost: 336   maxlim: 2805   bits: 13/12
c ---[ 627]---> BDD-cost:   22
c ---[ 625]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 623]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 621]---> Adder-cost: 632   maxlim: 5228   bits: 14/13
c ---[ 619]---> Adder-cost: 600   maxlim: 4845   bits: 14/13
c ---[ 617]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 832   maxlim: 6375   bits: 14/13
c ---[ 607]---> Adder-cost: 848   maxlim: 6758   bits: 14/13
c ---[ 605]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 585]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[ 583]---> Adder-cost: 224   maxlim: 2040   bits: 12/11
c ---[ 581]---> Adder-cost: 464   maxlim: 3825   bits: 13/12
c ---[ 579]---> Adder-cost: 480   maxlim: 4080   bits: 13/12
c ---[ 577]---> BDD-cost:   64
c ---[ 576]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[ 571]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 570]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 568]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> BDD-cost:   67
c ---[ 564]---> BDD-cost:   67
c ---[ 563]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 7
c ---[ 561]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 1654     Base: 2 2 2 2 2 2 2 7
c ---[ 559]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 7
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   67
c ---[ 556]---> BDD-cost:   67
c ---[ 555]---> BDD-cost:   68
c ---[ 554]---> BDD-cost:   67
c ---[ 553]---> BDD-cost:   67
c ---[ 552]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost:  854     Base: 2 2 2 2 2 2 2 7
c ---[ 546]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 544]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 543]---> Adder-cost: 167   maxlim: 1529   bits: 12/11
c ---[ 542]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 7
c ---[ 541]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 7
c ---[ 540]---> Adder-cost: 217   maxlim: 2039   bits: 12/11
c ---[ 539]---> Adder-cost: 230   maxlim: 1911   bits: 12/11
c ---[ 538]---> Adder-cost: 230   maxlim: 2039   bits: 12/11
c ---[ 537]---> Adder-cost: 217   maxlim: 2294   bits: 13/12
c ---[ 536]---> Adder-cost: 224   maxlim: 2166   bits: 13/12
c ---[ 535]---> Adder-cost: 240   maxlim: 2294   bits: 13/12
c ---[ 534]---> Adder-cost: 262   maxlim: 3059   bits: 13/12
c ---[ 533]---> Adder-cost: 295   maxlim: 2931   bits: 13/12
c ---[ 532]---> Adder-cost: 311   maxlim: 3059   bits: 13/12
c ---[ 531]---> Adder-cost: 346   maxlim: 3314   bits: 13/12
c ---[ 530]---> Adder-cost: 361   maxlim: 3186   bits: 13/12
c ---[ 529]---> Adder-cost: 361   maxlim: 3314   bits: 13/12
c ---[ 528]---> Adder-cost: 346   maxlim: 3569   bits: 13/12
c ---[ 527]---> Adder-cost: 377   maxlim: 3441   bits: 13/12
c ---[ 526]---> Adder-cost: 393   maxlim: 3569   bits: 13/12
c ---[ 525]---> Adder-cost: 304   maxlim: 3824   bits: 13/12
c ---[ 524]---> Adder-cost: 323   maxlim: 3696   bits: 13/12
c ---[ 523]---> Adder-cost: 405   maxlim: 3824   bits: 13/12
c ---[ 522]---> BDD-cost:   68
c ---[ 521]---> BDD-cost:   67
c ---[ 520]---> BDD-cost:   67
c ---[ 519]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 513]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 511]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 7
c ---[ 509]---> BDD-cost:   67
c ---[ 508]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 167   maxlim: 1784   bits: 12/11
c ---[ 506]---> Sorter-cost: 1753     Base: 2 2 2 2 2 2 2 7
c ---[ 505]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 504]---> Adder-cost: 199   maxlim: 2294   bits: 13/12
c ---[ 503]---> Adder-cost: 214   maxlim: 2294   bits: 13/12
c ---[ 502]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 7
c ---[ 501]---> Adder-cost: 225   maxlim: 2549   bits: 13/12
c ---[ 500]---> Adder-cost: 240   maxlim: 2549   bits: 13/12
c ---[ 499]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> BDD-cost:   68
c ---[ 496]---> BDD-cost:   67
c ---[ 495]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1359     Base: 2 2 2 2 2 2 2 7
c ---[ 493]---> Adder-cost: 185   maxlim: 1274   bits: 12/11
c ---[ 492]---> Adder-cost: 196   maxlim: 1274   bits: 12/11
c ---[ 491]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> BDD-cost:   68
c ---[ 489]---> BDD-cost:   67
c ---[ 488]---> BDD-cost:   67
c ---[ 487]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  456     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 481]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 479]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 478]---> Adder-cost: 135   maxlim: 1274   bits: 12/11
c ---[ 477]---> Sorter-cost: 1722     Base: 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1721     Base: 2 2 2 2 2 2 2 7
c ---[ 475]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 7
c ---[ 471]---> Adder-cost: 149   maxlim: 764   bits: 11/10
c ---[ 470]---> BDD-cost:   67
c ---[ 469]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Adder-cost: 249   maxlim: 1784   bits: 12/11
c ---[ 467]---> Adder-cost: 230   maxlim: 1657   bits: 12/11
c ---[ 466]---> Adder-cost: 210   maxlim: 2039   bits: 12/11
c ---[ 465]---> Adder-cost: 206   maxlim: 1912   bits: 12/11
c ---[ 464]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 463]---> Adder-cost: 297   maxlim: 2167   bits: 13/12
c ---[ 462]---> Adder-cost: 294   maxlim: 2422   bits: 13/12
c ---[ 461]---> Adder-cost: 286   maxlim: 2677   bits: 13/12
c ---[ 460]---> Adder-cost: 269   maxlim: 2422   bits: 13/12
c ---[ 459]---> Sorter-cost: 1587     Base: 2 2 2 2 2 2 2 7
c ---[ 458]---> Adder-cost: 426   maxlim: 2804   bits: 13/12
c ---[ 457]---> Adder-cost: 456   maxlim: 3186   bits: 13/12
c ---[ 456]---> Adder-cost: 439   maxlim: 3059   bits: 13/12
c ---[ 455]---> BDD-cost:   66
c ---[ 454]---> BDD-cost:   65
c ---[ 453]---> BDD-cost:   67
c ---[ 452]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> BDD-cost:   68
c ---[ 446]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 442]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:  475     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 438]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 7
c ---[ 437]---> Adder-cost: 185   maxlim: 1912   bits: 12/11
c ---[ 436]---> Adder-cost: 200   maxlim: 2167   bits: 13/12
c ---[ 435]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 434]---> Adder-cost: 266   maxlim: 2677   bits: 13/12
c ---[ 433]---> Adder-cost: 279   maxlim: 2932   bits: 13/12
c ---[ 432]---> Adder-cost: 256   maxlim: 2677   bits: 13/12
c ---[ 431]---> Adder-cost: 314   maxlim: 2932   bits: 13/12
c ---[ 430]---> Adder-cost: 309   maxlim: 3187   bits: 13/12
c ---[ 429]---> Adder-cost: 222   maxlim: 3187   bits: 13/12
c ---[ 428]---> Adder-cost: 296   maxlim: 3569   bits: 13/12
c ---[ 427]---> Adder-cost: 339   maxlim: 3952   bits: 13/12
c ---[ 426]---> Adder-cost: 287   maxlim: 3442   bits: 13/12
c ---[ 425]---> Adder-cost: 258   maxlim: 3442   bits: 13/12
c ---[ 424]---> Adder-cost: 422   maxlim: 4079   bits: 13/12
c ---[ 423]---> Adder-cost: 442   maxlim: 4462   bits: 14/13
c ---[ 422]---> Adder-cost: 391   maxlim: 3952   bits: 13/12
c ---[ 421]---> Adder-cost: 421   maxlim: 4844   bits: 14/13
c ---[ 420]---> Adder-cost: 420   maxlim: 5227   bits: 14/13
c ---[ 419]---> Adder-cost: 490   maxlim: 4462   bits: 14/13
c ---[ 418]---> Adder-cost: 493   maxlim: 5609   bits: 14/13
c ---[ 417]---> Adder-cost: 470   maxlim: 5992   bits: 14/13
c ---[ 416]---> Adder-cost: 496   maxlim: 5227   bits: 14/13
c ---[ 415]---> Adder-cost: 553   maxlim: 5864   bits: 14/13
c ---[ 414]---> Adder-cost: 562   maxlim: 6247   bits: 14/13
c ---[ 413]---> Adder-cost: 610   maxlim: 5482   bits: 14/13
c ---[ 412]---> Adder-cost: 597   maxlim: 6119   bits: 14/13
c ---[ 411]---> Adder-cost: 598   maxlim: 6502   bits: 14/13
c ---[ 410]---> Adder-cost: 564   maxlim: 5737   bits: 14/13
c ---[ 409]---> BDD-cost:   27
c ---[ 408]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> BDD-cost:   67
c ---[ 406]---> BDD-cost:   67
c ---[ 405]---> BDD-cost:   68
c ---[ 404]---> BDD-cost:   67
c ---[ 403]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 7
c ---[ 399]---> BDD-cost:   68
c ---[ 398]---> BDD-cost:   67
c ---[ 397]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> BDD-cost:   67
c ---[ 394]---> BDD-cost:   66
c ---[ 393]---> BDD-cost:   65
c ---[ 392]---> BDD-cost:   67
c ---[ 391]---> BDD-cost:   66
c ---[ 390]---> BDD-cost:   65
c ---[ 389]---> BDD-cost:   67
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> BDD-cost:   68
c ---[ 383]---> BDD-cost:   67
c ---[ 382]---> BDD-cost:   67
c ---[ 381]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 7
c ---[ 377]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 7
c ---[ 376]---> BDD-cost:   67
c ---[ 374]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Adder-cost: 167   maxlim: 1275   bits: 12/11
c ---[ 370]---> Adder-cost: 184   maxlim: 1274   bits: 12/11
c ---[ 369]---> Adder-cost: 185   maxlim: 1785   bits: 12/11
c ---[ 368]---> Adder-cost: 182   maxlim: 1784   bits: 12/11
c ---[ 367]---> Adder-cost: 233   maxlim: 2040   bits: 12/11
c ---[ 366]---> Adder-cost: 240   maxlim: 2039   bits: 12/11
c ---[ 365]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 7
c ---[ 364]---> Adder-cost: 228   maxlim: 2295   bits: 13/12
c ---[ 363]---> Adder-cost: 245   maxlim: 2294   bits: 13/12
c ---[ 362]---> Adder-cost: 410   maxlim: 2294   bits: 13/12
c ---[ 361]---> Adder-cost: 409   maxlim: 2549   bits: 13/12
c ---[ 360]---> Adder-cost: 304   maxlim: 2549   bits: 13/12
c ---[ 359]---> Adder-cost: 335   maxlim: 2804   bits: 13/12
c ---[ 358]---> BDD-cost:   65
c ---[ 357]---> BDD-cost:   67
c ---[ 355]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   35
c ---[ 351]---> BDD-cost:   35
c ---[ 349]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   35
c ---[ 343]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   35
c ---[ 333]---> BDD-cost:   35
c ---[ 331]---> BDD-cost:   35
c ---[ 329]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 323]---> BDD-cost:   35
c ---[ 321]---> BDD-cost:   35
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   35
c ---[ 313]---> BDD-cost:   35
c ---[ 311]---> BDD-cost:   35
c ---[ 309]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   35
c ---[ 305]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   35
c ---[ 295]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   35
c ---[ 287]---> BDD-cost:   35
c ---[ 285]---> BDD-cost:   35
c ---[ 283]---> BDD-cost:   35
c ---[ 281]---> BDD-cost:   35
c ---[ 279]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   35
c ---[ 275]---> BDD-cost:   35
c ---[ 273]---> BDD-cost:   35
c ---[ 271]---> BDD-cost:   35
c ---[ 269]---> BDD-cost:   35
c ---[ 267]---> BDD-cost:   35
c ---[ 265]---> BDD-cost:   35
c ---[ 263]---> BDD-cost:   35
c ---[ 261]---> BDD-cost:   35
c ---[ 259]---> BDD-cost:   35
c ---[ 257]---> BDD-cost:   35
c ---[ 255]---> BDD-cost:   35
c ---[ 253]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   35
c ---[ 243]---> BDD-cost:   35
c ---[ 241]---> BDD-cost:   35
c ---[ 239]---> BDD-cost:   35
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   35
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 143]---> BDD-cost:   76
c ---[ 141]---> BDD-cost:   76
c ---[ 139]---> BDD-cost:   76
c ---[ 137]---> BDD-cost:   76
c ---[ 135]---> BDD-cost:   76
c ---[ 133]---> BDD-cost:   76
c ---[ 131]---> BDD-cost:   76
c ---[ 129]---> BDD-cost:   76
c ---[ 127]---> BDD-cost:   76
c ---[ 125]---> BDD-cost:   76
c ---[ 123]---> BDD-cost:   76
c ---[ 121]---> BDD-cost:   76
c ---[ 119]---> BDD-cost:   76
c ---[ 117]---> BDD-cost:   76
c ---[ 115]---> BDD-cost:   76
c ---[ 113]---> BDD-cost:   76
c ---[ 111]---> BDD-cost:   35
c ---[ 109]---> BDD-cost:   76
c ---[ 107]---> BDD-cost:   76
c ---[ 105]---> BDD-cost:   76
c ---[ 103]---> BDD-cost:   76
c ---[ 101]---> BDD-cost:   76
c ---[  99]---> BDD-cost:   76
c ---[  97]---> BDD-cost:   76
c ---[  95]---> BDD-cost:   76
c ---[  93]---> BDD-cost:   76
c ---[  91]---> BDD-cost:   76
c ---[  89]---> BDD-cost:   76
c ---[  87]---> BDD-cost:   76
c ---[  85]---> BDD-cost:   76
c ---[  83]---> BDD-cost:   76
c ---[  81]---> BDD-cost:   76
c ---[  79]---> BDD-cost:   76
c ---[  77]---> BDD-cost:   76
c ---[  75]---> BDD-cost:   76
c ---[  73]---> BDD-cost:   76
c ---[  71]---> BDD-cost:   76
c ---[  69]---> BDD-cost:   76
c ---[  67]---> BDD-cost:   76
c ---[  65]---> BDD-cost:   76
c ---[  63]---> BDD-cost:   76
c ---[  61]---> BDD-cost:   76
c ---[  59]---> BDD-cost:   76
c ---[  57]---> BDD-cost:   76
c ---[  55]---> BDD-cost:   76
c ---[  53]---> BDD-cost:   76
c ---[  51]---> BDD-cost:   76
c ---[  49]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  41]---> BDD-cost:   76
c ---[  39]---> BDD-cost:   76
c ---[  37]---> BDD-cost:   76
c ---[  35]---> BDD-cost:   76
c ---[  33]---> BDD-cost:   76
c ---[  31]---> BDD-cost:   35
c ---[  29]---> BDD-cost:   35
c ---[  27]---> BDD-cost:   76
c ---[  25]---> BDD-cost:   76
c ---[  23]---> BDD-cost:   76
c ---[  21]---> BDD-cost:   76
c ---[  19]---> BDD-cost:   76
c ---[  17]---> BDD-cost:   76
c ---[  15]---> BDD-cost:   76
c ---[  13]---> BDD-cost:   76
c ---[  11]---> BDD-cost:   76
c ---[   9]---> BDD-cost:   76
c ---[   7]---> BDD-cost:   76
c ---[   5]---> BDD-cost:   76
c ---[   3]---> BDD-cost:   76
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  557400  1648122 |  185800       0        0     nan |  0.000 % |
c |       100 |  557400  1648122 |  204380     100     5349    53.5 |  5.868 % |
c |       250 |  557400  1648122 |  224818     250     6371    25.5 |  5.868 % |
c |       475 |  557321  1647947 |  247299     465     7853    16.9 |  5.885 % |
c |       812 |  557321  1647947 |  272029     802    11473    14.3 |  5.885 % |
c |      1318 |  557311  1647925 |  299232    1307    14714    11.3 |  5.887 % |
c |      2077 |  557301  1647903 |  329156    2065    41423    20.1 |  5.889 % |
c |      3216 |  557272  1647839 |  362071    3201    49122    15.3 |  5.895 % |
c |      4924 |  557123  1647507 |  398278    4897    58965    12.0 |  5.922 % |
c |      7487 |  557007  1647248 |  438106    7444    74649    10.0 |  5.945 % |
c |     11331 |  556704  1646565 |  481917   11252    97369     8.7 |  6.003 % |
c |     17097 |  556231  1645505 |  530109   16964   132171     7.8 |  6.093 % |
c |     25746 |  555971  1644923 |  583119   25570   433199    16.9 |  6.143 % |
c |     38721 |  555692  1644294 |  641431   38505  1241617    32.2 |  6.197 % |
c |     58182 |  555166  1643070 |  705575   57896  1419384    24.5 |  6.294 % |
c |     87374 |  555018  1642669 |  776132   87065  2051191    23.6 |  6.318 % |
c |    131163 |  554745  1641944 |  853745  130804  3633991    27.8 |  6.365 % |
c |    196848 |  554471  1641221 |  939120  196455  6565380    33.4 |  6.409 % |
c |    295376 |  554366  1640944 | 1033032  294966 10986563    37.2 |  6.425 % |
c |    443165 |  554179  1640444 | 1136335  442709 17277743    39.0 |  6.456 % |
#### 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.76 0.90 0.89 1/54 32631
Raw data (stat): 32631 (runsolver) D 32630 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 484722501 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.79 0.90 0.89 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13150 0 0 0 960 32 0 0 25 0 1 0 484722501 65044480 12775 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15880 12775 603 41 0 15839 0
vsize: 63520
[startup+20.0007 s]
Raw data (loadavg): 0.82 0.90 0.89 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13227 0 0 0 1960 33 0 0 25 0 1 0 484722501 65314816 12852 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15946 12852 603 41 0 15905 0
vsize: 63784
[startup+30.0008 s]
Raw data (loadavg): 0.85 0.91 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13289 0 0 0 2959 33 0 0 25 0 1 0 484722501 65622016 12914 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16021 12914 603 41 0 15980 0
vsize: 64084
[startup+40.0084 s]
Raw data (loadavg): 0.87 0.91 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13354 0 0 0 3960 33 0 0 25 0 1 0 484722501 65892352 12979 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16087 12979 603 41 0 16046 0
vsize: 64348
[startup+50.0156 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13392 0 0 0 4961 33 0 0 25 0 1 0 484722501 66027520 13017 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16120 13017 603 41 0 16079 0
vsize: 64480
[startup+60.0156 s]
Raw data (loadavg): 0.91 0.91 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13431 0 0 0 5960 33 0 0 25 0 1 0 484722501 66203648 13056 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16163 13056 603 41 0 16122 0
vsize: 64652
[startup+70.0166 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13745 0 0 0 6959 34 0 0 25 0 1 0 484722501 67407872 13370 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16457 13371 603 41 0 16416 0
vsize: 65828
[startup+80.0166 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13828 0 0 0 7959 34 0 0 25 0 1 0 484722501 67813376 13453 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16556 13453 603 41 0 16515 0
vsize: 66224
[startup+90.0165 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14204 0 0 0 8958 36 0 0 25 0 1 0 484722501 69410816 13829 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16946 13829 603 41 0 16905 0
vsize: 67784
[startup+100.016 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14739 0 0 0 9954 38 0 0 25 0 1 0 484722501 71561216 14364 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17471 14364 603 41 0 17430 0
vsize: 69884
[startup+110.032 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14778 0 0 0 10956 38 0 0 25 0 1 0 484722501 71696384 14403 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 14403 603 41 0 17463 0
vsize: 70016
[startup+120.033 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14829 0 0 0 11956 38 0 0 25 0 1 0 484722501 71966720 14454 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17570 14454 603 41 0 17529 0
vsize: 70280
[startup+130.04 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14877 0 0 0 12957 38 0 0 25 0 1 0 484722501 72101888 14502 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17603 14502 603 41 0 17562 0
vsize: 70412
[startup+140.041 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14949 0 0 0 13957 38 0 0 25 0 1 0 484722501 72368128 14574 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17668 14574 603 41 0 17627 0
vsize: 70672
[startup+150.042 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15006 0 0 0 14957 39 0 0 25 0 1 0 484722501 72638464 14631 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17734 14631 603 41 0 17693 0
vsize: 70936
[startup+160.041 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15084 0 0 0 15957 39 0 0 25 0 1 0 484722501 72908800 14709 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17800 14709 603 41 0 17759 0
vsize: 71200
[startup+170.041 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15242 0 0 0 16956 39 0 0 25 0 1 0 484722501 73584640 14867 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17965 14867 603 41 0 17924 0
vsize: 71860
[startup+180.041 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15397 0 0 0 17956 40 0 0 25 0 1 0 484722501 74387456 15022 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18161 15022 603 41 0 18120 0
vsize: 72644
[startup+190.041 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15441 0 0 0 18956 40 0 0 25 0 1 0 484722501 74522624 15066 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18194 15066 603 41 0 18153 0
vsize: 72776
[startup+200.041 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15587 0 0 0 19956 40 0 0 25 0 1 0 484722501 75194368 15212 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18358 15212 603 41 0 18317 0
vsize: 73432
[startup+210.04 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15676 0 0 0 20956 41 0 0 25 0 1 0 484722501 75460608 15301 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18423 15301 603 41 0 18382 0
vsize: 73692
[startup+220.041 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15932 0 0 0 21955 42 0 0 25 0 1 0 484722501 76541952 15557 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18687 15557 603 41 0 18646 0
vsize: 74748
[startup+230.041 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16046 0 0 0 22955 42 0 0 25 0 1 0 484722501 76947456 15671 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18786 15671 603 41 0 18745 0
vsize: 75144
[startup+240.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16132 0 0 0 23954 43 0 0 25 0 1 0 484722501 77352960 15757 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18885 15757 603 41 0 18844 0
vsize: 75540
[startup+250.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16536 0 0 0 24953 44 0 0 25 0 1 0 484722501 78958592 16161 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19277 16161 603 41 0 19236 0
vsize: 77108
[startup+260.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16695 0 0 0 25953 45 0 0 25 0 1 0 484722501 79495168 16320 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19408 16320 603 41 0 19367 0
vsize: 77632
[startup+270.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16778 0 0 0 26952 45 0 0 25 0 1 0 484722501 79896576 16403 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19506 16403 603 41 0 19465 0
vsize: 78024
[startup+280.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16906 0 0 0 27952 46 0 0 25 0 1 0 484722501 80433152 16531 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19637 16531 603 41 0 19596 0
vsize: 78548
[startup+290.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16968 0 0 0 28952 46 0 0 25 0 1 0 484722501 80568320 16593 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19670 16593 603 41 0 19629 0
vsize: 78680
[startup+300.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 17215 0 0 0 29952 47 0 0 25 0 1 0 484722501 81633280 16840 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19930 16840 603 41 0 19889 0
vsize: 79720
[startup+310.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 17701 0 0 0 30950 48 0 0 25 0 1 0 484722501 83668992 17326 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20427 17326 603 41 0 20386 0
vsize: 81708
[startup+320.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 17942 0 0 0 31950 49 0 0 25 0 1 0 484722501 84615168 17567 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20658 17567 603 41 0 20617 0
vsize: 82632
[startup+330.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18112 0 0 0 32949 50 0 0 25 0 1 0 484722501 85282816 17737 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20821 17737 603 41 0 20780 0
vsize: 83284
[startup+340.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18183 0 0 0 33948 50 0 0 25 0 1 0 484722501 86077440 17808 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21015 17808 603 41 0 20974 0
vsize: 84060
[startup+350.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18512 0 0 0 34947 51 0 0 25 0 1 0 484722501 87420928 18137 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21343 18137 603 41 0 21302 0
vsize: 85372
[startup+360.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18627 0 0 0 35947 51 0 0 25 0 1 0 484722501 87826432 18252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21442 18252 603 41 0 21401 0
vsize: 85768
[startup+370.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18877 0 0 0 36946 52 0 0 25 0 1 0 484722501 88772608 18502 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21673 18502 603 41 0 21632 0
vsize: 86692
[startup+380.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18939 0 0 0 37946 52 0 0 25 0 1 0 484722501 89042944 18564 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21739 18564 603 41 0 21698 0
vsize: 86956
[startup+390.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19041 0 0 0 38946 53 0 0 25 0 1 0 484722501 89448448 18666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21838 18666 603 41 0 21797 0
vsize: 87352
[startup+400.046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19197 0 0 0 39946 53 0 0 25 0 1 0 484722501 90124288 18822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22003 18822 603 41 0 21962 0
vsize: 88012
[startup+410.046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19430 0 0 0 40946 54 0 0 25 0 1 0 484722501 91070464 19055 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22234 19055 603 41 0 22193 0
vsize: 88936
[startup+420.046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19908 0 0 0 41945 55 0 0 25 0 1 0 484722501 92954624 19533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22694 19533 603 41 0 22653 0
vsize: 90776
[startup+430.047 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 20250 0 0 0 42944 56 0 0 25 0 1 0 484722501 94294016 19875 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23021 19875 603 41 0 22980 0
vsize: 92084
[startup+440.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 20515 0 0 0 43943 57 0 0 25 0 1 0 484722501 95367168 20140 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23283 20140 603 41 0 23242 0
vsize: 93132
[startup+450.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 21108 0 0 0 44941 60 0 0 25 0 1 0 484722501 97792000 20733 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23875 20733 603 41 0 23834 0
vsize: 95500
[startup+460.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 21623 0 0 0 45939 61 0 0 25 0 1 0 484722501 99942400 21248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24400 21248 603 41 0 24359 0
vsize: 97600
[startup+470.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 21930 0 0 0 46938 62 0 0 25 0 1 0 484722501 101150720 21555 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24695 21555 603 41 0 24654 0
vsize: 98780
[startup+480.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22064 0 0 0 47937 63 0 0 25 0 1 0 484722501 101687296 21689 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24826 21689 603 41 0 24785 0
vsize: 99304
[startup+490.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22203 0 0 0 48936 64 0 0 25 0 1 0 484722501 102227968 21828 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24958 21828 603 41 0 24917 0
vsize: 99832
[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22387 0 0 0 49936 64 0 0 25 0 1 0 484722501 102903808 22012 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25123 22012 603 41 0 25082 0
vsize: 100492
[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22447 0 0 0 50936 64 0 0 25 0 1 0 484722501 103174144 22072 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25189 22072 603 41 0 25148 0
vsize: 100756
[startup+520.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22974 0 0 0 51935 65 0 0 25 0 1 0 484722501 105324544 22599 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25714 22599 603 41 0 25673 0
vsize: 102856
[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 23503 0 0 0 52934 67 0 0 25 0 1 0 484722501 107479040 23128 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26240 23128 603 41 0 26199 0
vsize: 104960
[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 23873 0 0 0 53933 68 0 0 25 0 1 0 484722501 108957696 23498 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26601 23498 603 41 0 26560 0
vsize: 106404
[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24021 0 0 0 54933 69 0 0 25 0 1 0 484722501 109494272 23646 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26732 23646 603 41 0 26691 0
vsize: 106928
[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24409 0 0 0 55932 70 0 0 25 0 1 0 484722501 111108096 24034 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27126 24034 603 41 0 27085 0
vsize: 108504
[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24708 0 0 0 56932 70 0 0 25 0 1 0 484722501 112320512 24333 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27422 24333 603 41 0 27381 0
vsize: 109688
[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24876 0 0 0 57931 71 0 0 25 0 1 0 484722501 112996352 24501 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27587 24501 603 41 0 27546 0
vsize: 110348
[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25044 0 0 0 58930 72 0 0 25 0 1 0 484722501 113672192 24669 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27752 24669 603 41 0 27711 0
vsize: 111008
[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25464 0 0 0 59929 73 0 0 25 0 1 0 484722501 115429376 25089 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28181 25089 603 41 0 28140 0
vsize: 112724
[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25678 0 0 0 60928 74 0 0 25 0 1 0 484722501 117280768 25303 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28633 25303 603 41 0 28592 0
vsize: 114532
[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25763 0 0 0 61928 75 0 0 25 0 1 0 484722501 117551104 25388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 25388 603 41 0 28658 0
vsize: 114796
[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 26206 0 0 0 62927 76 0 0 25 0 1 0 484722501 119439360 25831 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29160 25831 603 41 0 29119 0
vsize: 116640
[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 26516 0 0 0 63926 78 0 0 25 0 1 0 484722501 120639488 26141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29453 26141 603 41 0 29412 0
vsize: 117812
[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 26854 0 0 0 64925 79 0 0 25 0 1 0 484722501 121974784 26479 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29779 26479 603 41 0 29738 0
vsize: 119116
[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27080 0 0 0 65924 80 0 0 25 0 1 0 484722501 122920960 26705 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30010 26705 603 41 0 29969 0
vsize: 120040
[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27255 0 0 0 66923 80 0 0 25 0 1 0 484722501 123584512 26880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30172 26880 603 41 0 30131 0
vsize: 120688
[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27492 0 0 0 67922 82 0 0 25 0 1 0 484722501 124530688 27117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30403 27117 603 41 0 30362 0
vsize: 121612
[startup+690.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27703 0 0 0 68921 82 0 0 25 0 1 0 484722501 125333504 27328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30599 27328 603 41 0 30558 0
vsize: 122396
[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27924 0 0 0 69921 83 0 0 25 0 1 0 484722501 126259200 27549 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30825 27549 603 41 0 30784 0
vsize: 123300
[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 28033 0 0 0 70921 83 0 0 25 0 1 0 484722501 126664704 27658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30924 27659 603 41 0 30883 0
vsize: 123696
[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 28292 0 0 0 71920 84 0 0 25 0 1 0 484722501 127737856 27917 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31186 27917 603 41 0 31145 0
vsize: 124744
[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 28709 0 0 0 72919 85 0 0 25 0 1 0 484722501 129359872 28334 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31582 28334 603 41 0 31541 0
vsize: 126328
[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29055 0 0 0 73919 86 0 0 25 0 1 0 484722501 130830336 28680 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31941 28680 603 41 0 31900 0
vsize: 127764
[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29400 0 0 0 74918 87 0 0 25 0 1 0 484722501 132169728 29025 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32268 29025 603 41 0 32227 0
vsize: 129072
[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29519 0 0 0 75918 87 0 0 25 0 1 0 484722501 132702208 29144 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32398 29144 603 41 0 32357 0
vsize: 129592
[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29780 0 0 0 76917 88 0 0 25 0 1 0 484722501 133771264 29405 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32659 29405 603 41 0 32618 0
vsize: 130636
[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30001 0 0 0 77917 88 0 0 25 0 1 0 484722501 134578176 29626 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32856 29626 603 41 0 32815 0
vsize: 131424
[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30185 0 0 0 78917 89 0 0 25 0 1 0 484722501 135385088 29810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33053 29810 603 41 0 33012 0
vsize: 132212
[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30396 0 0 0 79916 89 0 0 25 0 1 0 484722501 136196096 30021 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33251 30021 603 41 0 33210 0
vsize: 133004
[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30713 0 0 0 80916 90 0 0 25 0 1 0 484722501 137539584 30338 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33579 30338 603 41 0 33538 0
vsize: 134316
[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30972 0 0 0 81916 91 0 0 25 0 1 0 484722501 138481664 30597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33809 30597 603 41 0 33768 0
vsize: 135236
[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31123 0 0 0 82915 91 0 0 25 0 1 0 484722501 139157504 30748 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33974 30748 603 41 0 33933 0
vsize: 135896
[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31250 0 0 0 83915 92 0 0 25 0 1 0 484722501 139698176 30875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34106 30875 603 41 0 34065 0
vsize: 136424
[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31499 0 0 0 84915 92 0 0 25 0 1 0 484722501 140640256 31124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34336 31124 603 41 0 34295 0
vsize: 137344
[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31778 0 0 0 85914 93 0 0 25 0 1 0 484722501 141848576 31403 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34631 31403 603 41 0 34590 0
vsize: 138524
[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31889 0 0 0 86914 93 0 0 25 0 1 0 484722501 142254080 31514 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34730 31514 603 41 0 34689 0
vsize: 138920
[startup+880.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 32196 0 0 0 87913 94 0 0 25 0 1 0 484722501 143458304 31821 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35024 31821 603 41 0 34983 0
vsize: 140096
[startup+890.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 32610 0 0 0 88912 95 0 0 25 0 1 0 484722501 145076224 32235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35419 32235 603 41 0 35378 0
vsize: 141676
[startup+900.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 32916 0 0 0 89912 96 0 0 25 0 1 0 484722501 146419712 32541 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35747 32541 603 41 0 35706 0
vsize: 142988
[startup+910.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33164 0 0 0 90911 97 0 0 25 0 1 0 484722501 147361792 32789 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35977 32789 603 41 0 35936 0
vsize: 143908
[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33331 0 0 0 91911 97 0 0 25 0 1 0 484722501 148033536 32956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36141 32956 603 41 0 36100 0
vsize: 144564
[startup+930.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33544 0 0 0 92911 98 0 0 25 0 1 0 484722501 148844544 33169 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36339 33169 603 41 0 36298 0
vsize: 145356
[startup+940.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33658 0 0 0 93911 98 0 0 25 0 1 0 484722501 149385216 33283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36471 33283 603 41 0 36430 0
vsize: 145884
[startup+950.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33779 0 0 0 94911 98 0 0 25 0 1 0 484722501 149786624 33404 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36569 33404 603 41 0 36528 0
vsize: 146276
[startup+960.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33900 0 0 0 95911 98 0 0 25 0 1 0 484722501 150323200 33525 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36700 33525 603 41 0 36659 0
vsize: 146800
[startup+970.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34007 0 0 0 96911 98 0 0 25 0 1 0 484722501 150728704 33632 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36799 33632 603 41 0 36758 0
vsize: 147196
[startup+980.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34349 0 0 0 97910 100 0 0 25 0 1 0 484722501 152072192 33974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37127 33974 603 41 0 37086 0
vsize: 148508
[startup+990.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34601 0 0 0 98910 100 0 0 25 0 1 0 484722501 153145344 34226 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37389 34226 603 41 0 37348 0
vsize: 149556
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34719 0 0 0 99910 100 0 0 25 0 1 0 484722501 153550848 34344 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37488 34344 603 41 0 37447 0
vsize: 149952
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34990 0 0 0 100909 101 0 0 25 0 1 0 484722501 154619904 34615 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37749 34615 603 41 0 37708 0
vsize: 150996
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 35237 0 0 0 101908 102 0 0 25 0 1 0 484722501 155688960 34862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38010 34862 603 41 0 37969 0
vsize: 152040
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 35595 0 0 0 102907 103 0 0 25 0 1 0 484722501 157175808 35220 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38373 35220 603 41 0 38332 0
vsize: 153492
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 35899 0 0 0 103907 103 0 0 25 0 1 0 484722501 158392320 35524 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38670 35524 603 41 0 38629 0
vsize: 154680
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 36263 0 0 0 104907 104 0 0 25 0 1 0 484722501 159875072 35888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39032 35888 603 41 0 38991 0
vsize: 156128
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 36515 0 0 0 105906 105 0 0 25 0 1 0 484722501 160821248 36140 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39263 36140 603 41 0 39222 0
vsize: 157052
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 36836 0 0 0 106906 105 0 0 25 0 1 0 484722501 162164736 36461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39591 36461 603 41 0 39550 0
vsize: 158364
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 37114 0 0 0 107905 106 0 0 25 0 1 0 484722501 163241984 36739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39854 36739 603 41 0 39813 0
vsize: 159416
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 37425 0 0 0 108904 107 0 0 25 0 1 0 484722501 164614144 37050 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40189 37050 603 41 0 40148 0
vsize: 160756
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 37706 0 0 0 109903 108 0 0 25 0 1 0 484722501 165687296 37331 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40451 37331 603 41 0 40410 0
vsize: 161804
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 38452 0 0 0 110902 110 0 0 25 0 1 0 484722501 168779776 38077 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41206 38077 603 41 0 41165 0
vsize: 164824
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 39168 0 0 0 111900 112 0 0 25 0 1 0 484722501 171593728 38793 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41893 38793 603 41 0 41852 0
vsize: 167572
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 39778 0 0 0 112898 113 0 0 25 0 1 0 484722501 174137344 39403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42514 39403 603 41 0 42473 0
vsize: 170056
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40344 0 0 0 113897 115 0 0 25 0 1 0 484722501 176418816 39969 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43071 39969 603 41 0 43030 0
vsize: 172284
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40699 0 0 0 114895 117 0 0 25 0 1 0 484722501 177893376 40324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43431 40324 603 41 0 43390 0
vsize: 173724
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40750 0 0 0 115896 117 0 0 25 0 1 0 484722501 178163712 40375 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43497 40375 603 41 0 43456 0
vsize: 173988
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40899 0 0 0 116895 117 0 0 25 0 1 0 484722501 178700288 40524 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43628 40524 603 41 0 43587 0
vsize: 174512
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 41394 0 0 0 117894 119 0 0 25 0 1 0 484722501 180715520 41019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44120 41019 603 41 0 44079 0
vsize: 176480
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 41947 0 0 0 118893 120 0 0 25 0 1 0 484722501 182980608 41572 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44673 41572 603 41 0 44632 0
vsize: 178692
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32631
Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 42377 0 0 0 119892 122 0 0 25 0 1 0 484722501 184754176 42002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45106 42002 603 41 0 45065 0
vsize: 180424
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32631
Raw data (stat): 32631 (minisat+) Z 32630 30701 30700 0 -1 12 42379 0 0 0 119892 129 0 0 25 0 1 0 484722501 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.22
CPU user time (s): 1198.92
CPU system time (s): 1.2998
CPU usage (%): 100.006
Max. virtual memory (Kb): 180424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####