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/submitted/een/normalized-p2756.opb
MD5SUM	f3d955cf36894e7107b7f25ccaa97360
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	7463
Optimality of the best value was proved	NO
Number of terms in the objective function	2166
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	321831
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	321831
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04884
Number of variables	2734
Total number of constraints	738
Number of constraints which are clauses	132
Number of constraints which are cardinality constraints (but not clauses)	220
Number of constraints which are nor clauses,nor cardinality constraints	386
Minimum length of a constraint	2
Maximum length of a constraint	535
Trace number 7074

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        816352 kB
Buffers:         34996 kB
Cached:         139648 kB
SwapCached:        524 kB
Active:          57668 kB
Inactive:       120392 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        816072 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            34572 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:30:54 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 5106 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 738 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ....................................................................................................................................s..ssssssssss.s.sssssssssss
c ---[ 627]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 626]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 625]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 624]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 623]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 622]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 621]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 620]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 619]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 618]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 617]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 616]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 615]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 614]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 613]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 612]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 611]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 609]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 607]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 606]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 605]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 604]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 603]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 602]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 600]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 598]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 595]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 594]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 591]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 589]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 588]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 587]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 586]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 585]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 584]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 583]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 582]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 581]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 580]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 579]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 578]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 577]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 576]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 575]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 574]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 573]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 572]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 571]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 570]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 569]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 568]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 567]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 566]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 565]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 564]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 563]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 562]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 561]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 560]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 559]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 558]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 557]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 556]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 555]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 554]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 553]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 552]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 551]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 550]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 549]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 548]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 547]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 546]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 545]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 544]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 543]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 542]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 541]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 540]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 539]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 538]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 537]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 536]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 535]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 534]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 533]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 532]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 531]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 530]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 529]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 528]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 527]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 526]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 525]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 524]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 523]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 522]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 521]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 520]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 519]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 518]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 517]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 516]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 515]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 514]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 513]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 512]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 511]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 510]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 509]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 508]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 507]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 506]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 505]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 504]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 503]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 502]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 501]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 500]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 499]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 498]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 497]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 496]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 495]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 494]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 493]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 492]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 491]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 490]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 489]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 488]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 487]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 486]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 485]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 484]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 483]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 482]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 481]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 480]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 479]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 478]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 477]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 476]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 475]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 474]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 473]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 472]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 471]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 470]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 469]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 468]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 467]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 466]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 465]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 464]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 463]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 462]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 461]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 460]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 459]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 458]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 457]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 456]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 455]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 454]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 453]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 452]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 451]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 450]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 449]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 448]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 447]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 446]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 445]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 444]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 443]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 442]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 441]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 440]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 439]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 438]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 437]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 436]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 435]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 434]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 433]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 432]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 431]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 430]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 429]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 428]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 427]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 426]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 425]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 424]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 423]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 422]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 421]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 420]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 419]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 418]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 417]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 416]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 415]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 414]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 413]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 412]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 411]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 410]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 409]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 408]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 405]---> Adder-cost: 40   maxlim: 491   bits: 10/9
c ---[ 404]---> Adder-cost: 28   maxlim: 165   bits: 9/8
c ---[ 403]---> Adder-cost: 43   maxlim: 156   bits: 9/8
c ---[ 401]---> Adder-cost: 24   maxlim: 450   bits: 10/9
c ---[ 400]---> Adder-cost: 58   maxlim: 526   bits: 11/10
c ---[ 399]---> Adder-cost: 15   maxlim: 7   bits: 4/3
c ---[ 398]---> Adder-cost: 56   maxlim: 529   bits: 11/10
c ---[ 397]---> Adder-cost: 46   maxlim: 364   bits: 10/9
c ---[ 396]---> Adder-cost: 61   maxlim: 495   bits: 10/9
c ---[ 395]---> Adder-cost: 35   maxlim: 402   bits: 10/9
c ---[ 394]---> Adder-cost: 57   maxlim: 455   bits: 10/9
c ---[ 393]---> Adder-cost: 57   maxlim: 450   bits: 10/9
c ---[ 392]---> Adder-cost: 30   maxlim: 294   bits: 10/9
c ---[ 391]---> Adder-cost: 35   maxlim: 249   bits: 9/8
c ---[ 389]---> Adder-cost: 36   maxlim: 394   bits: 10/9
c ---[ 388]---> Adder-cost: 30   maxlim: 382   bits: 10/9
c ---[ 386]---> Adder-cost: 33   maxlim: 289   bits: 10/9
c ---[ 385]---> Adder-cost: 57   maxlim: 409   bits: 10/9
c ---[ 384]---> Adder-cost: 40   maxlim: 437   bits: 10/9
c ---[ 383]---> Adder-cost: 32   maxlim: 412   bits: 10/9
c ---[ 382]---> Adder-cost: 32   maxlim: 218   bits: 9/8
c ---[ 381]---> Adder-cost: 50   maxlim: 739   bits: 11/10
c ---[ 380]---> Adder-cost: 60   maxlim: 166   bits: 9/8
c ---[ 379]---> Adder-cost: 38   maxlim: 688   bits: 11/10
c ---[ 378]---> Adder-cost: 56   maxlim: 184   bits: 9/8
c ---[ 376]---> Adder-cost: 58   maxlim: 608   bits: 11/10
c ---[ 375]---> Adder-cost: 44   maxlim: 670   bits: 11/10
c ---[ 374]---> Adder-cost: 39   maxlim: 358   bits: 10/9
c ---[ 373]---> Adder-cost: 33   maxlim: 173   bits: 9/8
c ---[ 372]---> Adder-cost: 18   maxlim: 8   bits: 5/4
c ---[ 371]---> Adder-cost: 80   maxlim: 882   bits: 11/10
c ---[ 370]---> Adder-cost: 72   maxlim: 796   bits: 11/10
c ---[ 369]---> Adder-cost: 70   maxlim: 823   bits: 11/10
c ---[ 365]---> Adder-cost: 72   maxlim: 709   bits: 11/10
c ---[ 364]---> Adder-cost: 39   maxlim: 191   bits: 9/8
c ---[ 363]---> Adder-cost: 49   maxlim: 277   bits: 10/9
c ---[ 362]---> Adder-cost: 66   maxlim: 897   bits: 11/10
c ---[ 361]---> Adder-cost: 49   maxlim: 250   bits: 9/8
c ---[ 360]---> Adder-cost: 76   maxlim: 700   bits: 11/10
c ---[ 359]---> Adder-cost: 93   maxlim: 935   bits: 11/10
c ---[ 358]---> Adder-cost: 71   maxlim: 279   bits: 10/9
c ---[ 357]---> Adder-cost: 58   maxlim: 868   bits: 11/10
c ---[ 356]---> Adder-cost: 75   maxlim: 356   bits: 10/9
c ---[ 355]---> Adder-cost: 49   maxlim: 688   bits: 11/10
c ---[ 354]---> Adder-cost: 75   maxlim: 374   bits: 10/9
c ---[ 353]---> Adder-cost: 82   maxlim: 556   bits: 11/10
c ---[ 352]---> Adder-cost: 74   maxlim: 977   bits: 11/10
c ---[ 351]---> Adder-cost: 44   maxlim: 670   bits: 11/10
c ---[ 349]---> Adder-cost: 78   maxlim: 580   bits: 11/10
c ---[ 348]---> Adder-cost: 76   maxlim: 906   bits: 11/10
c ---[ 347]---> Adder-cost: 45   maxlim: 588   bits: 11/10
c ---[ 346]---> Adder-cost: 76   maxlim: 725   bits: 11/10
c ---[ 345]---> Adder-cost: 74   maxlim: 523   bits: 11/10
c ---[ 344]---> Adder-cost: 47   maxlim: 564   bits: 11/10
c ---[ 343]---> Adder-cost: 53   maxlim: 621   bits: 11/10
c ---[ 342]---> Adder-cost: 73   maxlim: 423   bits: 10/9
c ---[ 341]---> Adder-cost: 54   maxlim: 419   bits: 10/9
c ---[ 340]---> Adder-cost: 58   maxlim: 724   bits: 11/10
c ---[ 339]---> Adder-cost: 75   maxlim: 319   bits: 10/9
c ---[ 337]---> Adder-cost: 62   maxlim: 828   bits: 11/10
c ---[ 336]---> Adder-cost: 76   maxlim: 775   bits: 11/10
c ---[ 335]---> Adder-cost: 57   maxlim: 483   bits: 10/9
c ---[ 334]---> Adder-cost: 90   maxlim: 440   bits: 10/9
c ---[ 333]---> Adder-cost: 45   maxlim: 828   bits: 11/10
c ---[ 332]---> Adder-cost: 83   maxlim: 317   bits: 10/9
c ---[ 331]---> Adder-cost: 38   maxlim: 830   bits: 11/10
c ---[ 330]---> Adder-cost: 82   maxlim: 541   bits: 11/10
c ---[ 329]---> Adder-cost: 55   maxlim: 717   bits: 11/10
c ---[ 328]---> Adder-cost: 50   maxlim: 333   bits: 10/9
c ---[ 327]---> Adder-cost: 90   maxlim: 763   bits: 11/10
c ---[ 326]---> Adder-cost: 81   maxlim: 385   bits: 10/9
c ---[ 325]---> Adder-cost: 82   maxlim: 918   bits: 11/10
c ---[ 324]---> Adder-cost: 86   maxlim: 667   bits: 11/10
c ---[ 323]---> Adder-cost: 90   maxlim: 853   bits: 11/10
c ---[ 322]---> Adder-cost: 60   maxlim: 752   bits: 11/10
c ---[ 321]---> Adder-cost: 79   maxlim: 357   bits: 10/9
c ---[ 320]---> Adder-cost: 51   maxlim: 328   bits: 10/9
c ---[ 319]---> Adder-cost: 76   maxlim: 248   bits: 9/8
c ---[ 318]---> Adder-cost: 75   maxlim: 433   bits: 10/9
c ---[ 317]---> Adder-cost: 47   maxlim: 917   bits: 11/10
c ---[ 316]---> Adder-cost: 54   maxlim: 1026   bits: 12/11
c ---[ 315]---> Adder-cost: 61   maxlim: 470   bits: 10/9
c ---[ 314]---> Adder-cost: 61   maxlim: 374   bits: 10/9
c ---[ 313]---> Adder-cost: 51   maxlim: 813   bits: 11/10
c ---[ 312]---> Adder-cost: 51   maxlim: 284   bits: 10/9
c ---[ 311]---> Adder-cost: 96   maxlim: 438   bits: 10/9
c ---[ 310]---> Adder-cost: 82   maxlim: 840   bits: 11/10
c ---[ 309]---> Adder-cost: 67   maxlim: 323   bits: 10/9
c ---[ 308]---> Adder-cost: 81   maxlim: 379   bits: 10/9
c ---[ 307]---> Adder-cost: 92   maxlim: 1080   bits: 12/11
c ---[ 306]---> Adder-cost: 97   maxlim: 314   bits: 10/9
c ---[ 305]---> Adder-cost: 96   maxlim: 226   bits: 9/8
c ---[ 304]---> Adder-cost: 91   maxlim: 927   bits: 11/10
c ---[ 303]---> Adder-cost: 55   maxlim: 527   bits: 11/10
c ---[ 302]---> Adder-cost: 87   maxlim: 911   bits: 11/10
c ---[ 301]---> Adder-cost: 80   maxlim: 1070   bits: 12/11
c ---[ 300]---> Adder-cost: 88   maxlim: 484   bits: 10/9
c ---[ 299]---> Adder-cost: 85   maxlim: 943   bits: 11/10
c ---[ 298]---> Adder-cost: 96   maxlim: 793   bits: 11/10
c ---[ 297]---> Adder-cost: 92   maxlim: 749   bits: 11/10
c ---[ 296]---> Adder-cost: 95   maxlim: 947   bits: 11/10
c ---[ 295]---> Adder-cost: 80   maxlim: 479   bits: 10/9
c ---[ 294]---> Adder-cost: 46   maxlim: 192   bits: 9/8
c ---[ 293]---> Adder-cost: 58   maxlim: 393   bits: 10/9
c ---[ 292]---> Adder-cost: 101   maxlim: 1022   bits: 11/10
c ---[ 291]---> Adder-cost: 57   maxlim: 957   bits: 11/10
c ---[ 290]---> Adder-cost: 86   maxlim: 435   bits: 10/9
c ---[ 289]---> Adder-cost: 92   maxlim: 458   bits: 10/9
c ---[ 288]---> Adder-cost: 78   maxlim: 503   bits: 10/9
c ---[ 287]---> Adder-cost: 88   maxlim: 1056   bits: 12/11
c ---[ 286]---> Adder-cost: 96   maxlim: 753   bits: 11/10
c ---[ 285]---> Adder-cost: 75   maxlim: 350   bits: 10/9
c ---[ 284]---> Adder-cost: 41   maxlim: 759   bits: 11/10
c ---[ 283]---> Adder-cost: 45   maxlim: 262   bits: 10/9
c ---[ 282]---> Adder-cost: 89   maxlim: 268   bits: 10/9
c ---[ 281]---> Adder-cost: 98   maxlim: 1025   bits: 12/11
c ---[ 280]---> Adder-cost: 66   maxlim: 448   bits: 10/9
c ---[ 279]---> Adder-cost: 94   maxlim: 517   bits: 11/10
c ---[ 278]---> Adder-cost: 94   maxlim: 804   bits: 11/10
c ---[ 277]---> Adder-cost: 68   maxlim: 536   bits: 11/10
c ---[ 276]---> Adder-cost: 66   maxlim: 937   bits: 11/10
c ---[ 275]---> Adder-cost: 65   maxlim: 491   bits: 10/9
c ---[ 274]---> Adder-cost: 68   maxlim: 562   bits: 11/10
c ---[ 273]---> Adder-cost: 100   maxlim: 729   bits: 11/10
c ---[ 272]---> Adder-cost: 99   maxlim: 1006   bits: 11/10
c ---[ 271]---> Adder-cost: 67   maxlim: 971   bits: 11/10
c ---[ 270]---> Adder-cost: 64   maxlim: 1016   bits: 11/10
c ---[ 269]---> Adder-cost: 98   maxlim: 510   bits: 10/9
c ---[ 268]---> Adder-cost: 69   maxlim: 373   bits: 10/9
c ---[ 267]---> Adder-cost: 86   maxlim: 814   bits: 11/10
c ---[ 266]---> Adder-cost: 92   maxlim: 220   bits: 9/8
c ---[ 265]---> Adder-cost: 95   maxlim: 308   bits: 10/9
c ---[ 264]---> Adder-cost: 44   maxlim: 912   bits: 11/10
c ---[ 263]---> Adder-cost: 58   maxlim: 483   bits: 10/9
c ---[ 262]---> Adder-cost: 90   maxlim: 1159   bits: 12/11
c ---[ 261]---> Adder-cost: 60   maxlim: 862   bits: 11/10
c ---[ 260]---> Adder-cost: 97   maxlim: 961   bits: 11/10
c ---[ 259]---> Adder-cost: 96   maxlim: 468   bits: 10/9
c ---[ 258]---> Adder-cost: 83   maxlim: 965   bits: 11/10
c ---[ 257]---> Adder-cost: 82   maxlim: 665   bits: 11/10
c ---[ 256]---> Adder-cost: 66   maxlim: 532   bits: 11/10
c ---[ 255]---> Adder-cost: 58   maxlim: 818   bits: 11/10
c ---[ 254]---> Adder-cost: 57   maxlim: 480   bits: 10/9
c ---[ 253]---> Adder-cost: 58   maxlim: 939   bits: 11/10
c ---[ 252]---> Adder-cost: 74   maxlim: 626   bits: 11/10
c ---[ 251]---> Adder-cost: 56   maxlim: 417   bits: 10/9
c ---[ 250]---> Adder-cost: 51   maxlim: 278   bits: 10/9
c ---[ 249]---> Adder-cost: 55   maxlim: 324   bits: 10/9
c ---[ 248]---> Adder-cost: 71   maxlim: 977   bits: 11/10
c ---[ 247]---> Adder-cost: 57   maxlim: 354   bits: 10/9
c ---[ 246]---> Adder-cost: 60   maxlim: 236   bits: 9/8
c ---[ 245]---> Adder-cost: 65   maxlim: 1015   bits: 11/10
c ---[ 244]---> Adder-cost: 52   maxlim: 297   bits: 10/9
c ---[ 243]---> Adder-cost: 55   maxlim: 927   bits: 11/10
c ---[ 242]---> Adder-cost: 96   maxlim: 729   bits: 11/10
c ---[ 241]---> Adder-cost: 46   maxlim: 774   bits: 11/10
c ---[ 240]---> Adder-cost: 54   maxlim: 813   bits: 11/10
c ---[ 239]---> Adder-cost: 67   maxlim: 918   bits: 11/10
c ---[ 238]---> Adder-cost: 46   maxlim: 1175   bits: 12/11
c ---[ 237]---> Adder-cost: 48   maxlim: 457   bits: 10/9
c ---[ 236]---> Adder-cost: 64   maxlim: 556   bits: 11/10
c ---[ 235]---> Adder-cost: 52   maxlim: 632   bits: 11/10
c ---[ 234]---> Adder-cost: 65   maxlim: 669   bits: 11/10
c ---[ 233]---> Adder-cost: 54   maxlim: 1169   bits: 12/11
c ---[ 232]---> Adder-cost: 46   maxlim: 636   bits: 11/10
c ---[ 231]---> Adder-cost: 90   maxlim: 1089   bits: 12/11
c ---[ 230]---> Adder-cost: 100   maxlim: 1113   bits: 12/11
c ---[ 229]---> Adder-cost: 110   maxlim: 1326   bits: 12/11
c ---[ 228]---> Adder-cost: 61   maxlim: 375   bits: 10/9
c ---[ 227]---> Adder-cost: 97   maxlim: 262   bits: 10/9
c ---[ 226]---> Adder-cost: 98   maxlim: 492   bits: 10/9
c ---[ 225]---> Adder-cost: 48   maxlim: 972   bits: 11/10
c ---[ 224]---> Adder-cost: 98   maxlim: 586   bits: 11/10
c ---[ 223]---> Adder-cost: 96   maxlim: 1051   bits: 12/11
c ---[ 222]---> Adder-cost: 103   maxlim: 731   bits: 11/10
c ---[ 221]---> Adder-cost: 110   maxlim: 1480   bits: 12/11
c ---[ 219]---> Adder-cost: 99   maxlim: 885   bits: 11/10
c ---[ 217]---> Adder-cost: 96   maxlim: 469   bits: 10/9
c ---[ 216]---> Adder-cost: 102   maxlim: 1428   bits: 12/11
c ---[ 215]---> Adder-cost: 97   maxlim: 942   bits: 11/10
c ---[ 214]---> Adder-cost: 90   maxlim: 1152   bits: 12/11
c ---[ 213]---> Adder-cost: 92   maxlim: 479   bits: 10/9
c ---[ 212]---> Adder-cost: 100   maxlim: 1288   bits: 12/11
c ---[ 211]---> Adder-cost: 55   maxlim: 485   bits: 10/9
c ---[ 210]---> Adder-cost: 104   maxlim: 828   bits: 11/10
c ---[ 209]---> Adder-cost: 96   maxlim: 563   bits: 11/10
c ---[ 208]---> Adder-cost: 48   maxlim: 522   bits: 11/10
c ---[ 207]---> Adder-cost: 73   maxlim: 222   bits: 9/8
c ---[ 206]---> Adder-cost: 106   maxlim: 1442   bits: 12/11
c ---[ 205]---> Adder-cost: 67   maxlim: 189   bits: 9/8
c ---[ 204]---> Adder-cost: 104   maxlim: 1322   bits: 12/11
c ---[ 203]---> Adder-cost: 92   maxlim: 1081   bits: 12/11
c ---[ 202]---> Adder-cost: 54   maxlim: 299   bits: 10/9
c ---[ 201]---> Adder-cost: 92   maxlim: 839   bits: 11/10
c ---[ 200]---> Adder-cost: 104   maxlim: 1275   bits: 12/11
c ---[ 199]---> Adder-cost: 94   maxlim: 809   bits: 11/10
c ---[ 198]---> Adder-cost: 109   maxlim: 796   bits: 11/10
c ---[ 197]---> Adder-cost: 94   maxlim: 237   bits: 9/8
c ---[ 196]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[ 195]---> Adder-cost: 74   maxlim: 510   bits: 10/9
c ---[ 194]---> Adder-cost: 106   maxlim: 404   bits: 10/9
c ---[ 193]---> Adder-cost: 111   maxlim: 884   bits: 11/10
c ---[ 192]---> Adder-cost: 89   maxlim: 267   bits: 10/9
c ---[ 191]---> Adder-cost: 107   maxlim: 903   bits: 11/10
c ---[ 190]---> Adder-cost: 105   maxlim: 880   bits: 11/10
c ---[ 189]---> Adder-cost: 61   maxlim: 1103   bits: 12/11
c ---[ 188]---> Adder-cost: 99   maxlim: 278   bits: 10/9
c ---[ 187]---> Adder-cost: 52   maxlim: 257   bits: 10/9
c ---[ 186]---> Adder-cost: 53   maxlim: 1133   bits: 12/11
c ---[ 185]---> Adder-cost: 60   maxlim: 1057   bits: 12/11
c ---[ 184]---> Adder-cost: 53   maxlim: 312   bits: 10/9
c ---[ 183]---> Adder-cost: 61   maxlim: 383   bits: 10/9
c ---[ 182]---> Adder-cost: 60   maxlim: 491   bits: 10/9
c ---[ 181]---> Adder-cost: 63   maxlim: 608   bits: 11/10
c ---[ 180]---> Adder-cost: 69   maxlim: 193   bits: 9/8
c ---[ 179]---> Adder-cost: 64   maxlim: 480   bits: 10/9
c ---[ 178]---> Adder-cost: 65   maxlim: 529   bits: 11/10
c ---[ 177]---> Adder-cost: 68   maxlim: 489   bits: 10/9
c ---[ 176]---> Adder-cost: 71   maxlim: 944   bits: 11/10
c ---[ 175]---> Adder-cost: 63   maxlim: 921   bits: 11/10
c ---[ 174]---> Adder-cost: 53   maxlim: 1028   bits: 12/11
c ---[ 173]---> Adder-cost: 51   maxlim: 189   bits: 9/8
c ---[ 172]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[ 171]---> Adder-cost: 56   maxlim: 901   bits: 11/10
c ---[ 170]---> Adder-cost: 70   maxlim: 891   bits: 11/10
c ---[ 169]---> Adder-cost: 58   maxlim: 1041   bits: 12/11
c ---[ 168]---> Adder-cost: 61   maxlim: 268   bits: 10/9
c ---[ 167]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[ 166]---> Adder-cost: 69   maxlim: 776   bits: 11/10
c ---[ 165]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[ 164]---> Adder-cost: 56   maxlim: 627   bits: 11/10
c ---[ 163]---> Adder-cost: 62   maxlim: 186   bits: 8/8
c ---[ 162]---> Adder-cost: 108   maxlim: 1031   bits: 12/11
c ---[ 161]---> Adder-cost: 117   maxlim: 920   bits: 11/10
c ---[ 159]---> Adder-cost: 108   maxlim: 652   bits: 11/10
c ---[ 158]---> Adder-cost: 108   maxlim: 1192   bits: 12/11
c ---[ 157]---> Adder-cost: 120   maxlim: 1139   bits: 12/11
c ---[ 156]---> Adder-cost: 77   maxlim: 654   bits: 11/10
c ---[ 154]---> Adder-cost: 127   maxlim: 754   bits: 11/10
c ---[ 153]---> Adder-cost: 94   maxlim: 260   bits: 10/9
c ---[ 152]---> Adder-cost: 118   maxlim: 1222   bits: 12/11
c ---[ 151]---> Adder-cost: 121   maxlim: 1011   bits: 11/10
c ---[ 150]---> Adder-cost: 77   maxlim: 469   bits: 10/9
c ---[ 149]---> Adder-cost: 95   maxlim: 195   bits: 9/8
c ---[ 148]---> Adder-cost: 55   maxlim: 308   bits: 10/9
c ---[ 147]---> Adder-cost: 74   maxlim: 766   bits: 11/10
c ---[ 146]---> Adder-cost: 61   maxlim: 563   bits: 11/10
c ---[ 145]---> Adder-cost: 116   maxlim: 1157   bits: 12/11
c ---[ 143]---> Adder-cost: 71   maxlim: 823   bits: 11/10
c ---[ 142]---> Adder-cost: 66   maxlim: 1238   bits: 12/11
c ---[ 141]---> Adder-cost: 61   maxlim: 1303   bits: 12/11
c ---[ 140]---> Adder-cost: 127   maxlim: 923   bits: 11/10
c ---[ 139]---> Adder-cost: 115   maxlim: 183   bits: 9/8
c ---[ 138]---> Adder-cost: 81   maxlim: 686   bits: 11/10
c ---[ 137]---> Adder-cost: 82   maxlim: 1426   bits: 12/11
c ---[ 136]---> Adder-cost: 112   maxlim: 1040   bits: 12/11
c ---[ 135]---> Adder-cost: 119   maxlim: 921   bits: 11/10
c ---[ 134]---> Adder-cost: 126   maxlim: 1206   bits: 12/11
c ---[ 133]---> Adder-cost: 75   maxlim: 644   bits: 11/10
c ---[ 131]---> Adder-cost: 110   maxlim: 621   bits: 11/10
c ---[ 130]---> Adder-cost: 109   maxlim: 648   bits: 11/10
c ---[ 129]---> Adder-cost: 116   maxlim: 1229   bits: 12/11
c ---[ 127]---> Adder-cost: 75   maxlim: 944   bits: 11/10
c ---[ 126]---> Adder-cost: 114   maxlim: 1417   bits: 12/11
c ---[ 125]---> Adder-cost: 107   maxlim: 859   bits: 11/10
c ---[ 124]---> Adder-cost: 121   maxlim: 861   bits: 11/10
c ---[ 123]---> Adder-cost: 120   maxlim: 1259   bits: 12/11
c ---[ 122]---> Adder-cost: 122   maxlim: 494   bits: 10/9
c ---[ 121]---> Adder-cost: 109   maxlim: 640   bits: 11/10
c ---[ 120]---> Adder-cost: 75   maxlim: 942   bits: 11/10
c ---[ 119]---> Adder-cost: 66   maxlim: 729   bits: 11/10
c ---[ 118]---> Adder-cost: 71   maxlim: 208   bits: 9/8
c ---[ 117]---> Adder-cost: 77   maxlim: 585   bits: 11/10
c ---[ 116]---> Adder-cost: 52   maxlim: 731   bits: 11/10
c ---[ 115]---> Adder-cost: 75   maxlim: 950   bits: 11/10
c ---[ 114]---> Adder-cost: 66   maxlim: 1131   bits: 12/11
c ---[ 112]---> Adder-cost: 121   maxlim: 695   bits: 11/10
c ---[ 111]---> Adder-cost: 121   maxlim: 608   bits: 11/10
c ---[ 109]---> Adder-cost: 130   maxlim: 1058   bits: 12/11
c ---[ 108]---> Adder-cost: 89   maxlim: 659   bits: 11/10
c ---[ 107]---> Adder-cost: 126   maxlim: 1299   bits: 12/11
c ---[ 106]---> Adder-cost: 119   maxlim: 944   bits: 11/10
c ---[ 105]---> Adder-cost: 118   maxlim: 1452   bits: 12/11
c ---[ 103]---> Adder-cost: 120   maxlim: 1305   bits: 12/11
c ---[ 102]---> Adder-cost: 54   maxlim: 672   bits: 11/10
c ---[ 101]---> Adder-cost: 122   maxlim: 1206   bits: 12/11
c ---[ 100]---> Adder-cost: 70   maxlim: 921   bits: 11/10
c ---[  99]---> Adder-cost: 128   maxlim: 1266   bits: 12/11
c ---[  98]---> Adder-cost: 75   maxlim: 309   bits: 10/9
c ---[  97]---> Adder-cost: 125   maxlim: 869   bits: 11/10
c ---[  96]---> Adder-cost: 124   maxlim: 1229   bits: 12/11
c ---[  94]---> Adder-cost: 90   maxlim: 418   bits: 10/9
c ---[  93]---> Adder-cost: 82   maxlim: 775   bits: 11/10
c ---[  91]---> Adder-cost: 72   maxlim: 1159   bits: 12/11
c ---[  90]---> Adder-cost: 136   maxlim: 1555   bits: 12/11
c ---[  89]---> Adder-cost: 138   maxlim: 1309   bits: 12/11
c ---[  87]---> Adder-cost: 128   maxlim: 1404   bits: 12/11
c ---[  86]---> Adder-cost: 135   maxlim: 1010   bits: 11/10
c ---[  85]---> Adder-cost: 128   maxlim: 224   bits: 9/8
c ---[  84]---> Adder-cost: 134   maxlim: 191   bits: 9/8
c ---[  83]---> Adder-cost: 130   maxlim: 332   bits: 10/9
c ---[  82]---> Adder-cost: 141   maxlim: 299   bits: 10/9
c ---[  81]---> Adder-cost: 131   maxlim: 711   bits: 11/10
c ---[  80]---> Adder-cost: 144   maxlim: 1597   bits: 12/11
c ---[  79]---> Adder-cost: 139   maxlim: 709   bits: 11/10
c ---[  77]---> Adder-cost: 136   maxlim: 1325   bits: 12/11
c ---[  76]---> Adder-cost: 136   maxlim: 1573   bits: 12/11
c ---[  75]---> Adder-cost: 133   maxlim: 666   bits: 11/10
c ---[  74]---> Adder-cost: 134   maxlim: 1552   bits: 12/11
c ---[  73]---> Adder-cost: 133   maxlim: 664   bits: 11/10
c ---[  72]---> Adder-cost: 81   maxlim: 1651   bits: 12/11
c ---[  71]---> Adder-cost: 90   maxlim: 1497   bits: 12/11
c ---[  70]---> Adder-cost: 69   maxlim: 1759   bits: 12/11
c ---[  69]---> Adder-cost: 80   maxlim: 1605   bits: 12/11
c ---[  68]---> Adder-cost: 71   maxlim: 719   bits: 11/10
c ---[  67]---> Adder-cost: 76   maxlim: 325   bits: 10/9
c ---[  66]---> Adder-cost: 128   maxlim: 1252   bits: 12/11
c ---[  65]---> Adder-cost: 88   maxlim: 443   bits: 10/9
c ---[  64]---> Adder-cost: 87   maxlim: 197   bits: 9/8
c ---[  63]---> Adder-cost: 82   maxlim: 981   bits: 11/10
c ---[  61]---> Adder-cost: 87   maxlim: 1043   bits: 12/11
c ---[  60]---> Adder-cost: 128   maxlim: 1234   bits: 12/11
c ---[  59]---> Adder-cost: 71   maxlim: 427   bits: 10/9
c ---[  57]---> Adder-cost: 65   maxlim: 1026   bits: 12/11
c ---[  56]---> Adder-cost: 75   maxlim: 200   bits: 9/8
c ---[  55]---> Adder-cost: 77   maxlim: 1088   bits: 12/11
c ---[  54]---> Adder-cost: 143   maxlim: 642   bits: 11/10
c ---[  53]---> Adder-cost: 94   maxlim: 1264   bits: 12/11
c ---[  52]---> Adder-cost: 147   maxlim: 438   bits: 10/9
c ---[  51]---> Adder-cost: 82   maxlim: 1468   bits: 12/11
c ---[  50]---> Adder-cost: 148   maxlim: 1356   bits: 12/11
c ---[  49]---> Adder-cost: 138   maxlim: 1560   bits: 12/11
c ---[  48]---> Adder-cost: 76   maxlim: 556   bits: 11/10
c ---[  47]---> Adder-cost: 84   maxlim: 352   bits: 10/9
c ---[  46]---> Adder-cost: 157   maxlim: 725   bits: 11/10
c ---[  45]---> Adder-cost: 160   maxlim: 1481   bits: 12/11
c ---[  44]---> Adder-cost: 93   maxlim: 1367   bits: 12/11
c ---[  43]---> Adder-cost: 94   maxlim: 611   bits: 11/10
c ---[  42]---> Adder-cost: 162   maxlim: 1715   bits: 12/11
c ---[  41]---> Adder-cost: 101   maxlim: 544   bits: 11/10
c ---[  40]---> Adder-cost: 170   maxlim: 1914   bits: 12/11
c ---[  39]---> Adder-cost: 87   maxlim: 345   bits: 10/9
c ---[  38]---> Adder-cost: 63   maxlim: 31   bits: 6/5
c ---[  37]---> Adder-cost: 66   maxlim: 32   bits: 7/6
c ---[  36]---> Adder-cost: 168   maxlim: 399   bits: 10/9
c ---[  35]---> Adder-cost: 80   maxlim: 39   bits: 7/6
c ---[  34]---> Adder-cost: 92   maxlim: 45   bits: 7/6
c ---[  33]---> Adder-cost: 120   maxlim: 59   bits: 7/6
c ---[  32]---> Adder-cost: 307   maxlim: 274   bits: 10/9
c ---[  31]---> Adder-cost: 426   maxlim: 1316   bits: 11/11
c ---[  30]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  29]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  28]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  27]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  25]---> Adder-cost: 542   maxlim: 1513   bits: 11/11
c ---[  24]---> Adder-cost: 533   maxlim: 98   bits: 8/7
c ---[  23]---> Adder-cost: 378   maxlim: 188   bits: 9/8
c ---[  22]---> Adder-cost: 1938   maxlim: 571   bits: 11/10
c ---[  21]---> Adder-cost: 19   maxlim: 57   bits: 7/6
c ---[  20]---> Adder-cost: 38   maxlim: 82   bits: 8/7
c ---[  19]---> Adder-cost: 39   maxlim: 129   bits: 9/8
c ---[  18]---> Adder-cost: 15   maxlim: 47   bits: 7/6
c ---[  17]---> Adder-cost: 31   maxlim: 133   bits: 9/8
c ---[  16]---> Adder-cost: 35   maxlim: 142   bits: 9/8
c ---[  15]---> Adder-cost: 15   maxlim: 56   bits: 7/6
c ---[  14]---> Adder-cost: 46   maxlim: 164   bits: 9/8
c ---[  13]---> Adder-cost: 59   maxlim: 184   bits: 9/8
c ---[  12]---> Adder-cost: 46   maxlim: 151   bits: 9/8
c ---[  11]---> Adder-cost: 36   maxlim: 88   bits: 8/7
c ---[  10]---> Adder-cost: 37   maxlim: 72   bits: 8/7
c ---[   9]---> Adder-cost: 49   maxlim: 95   bits: 8/7
c ---[   8]---> Adder-cost: 65   maxlim: 125   bits: 8/7
c ---[   7]---> Adder-cost: 47   maxlim: 95   bits: 8/7
c ---[   6]---> Adder-cost: 41   maxlim: 72   bits: 8/7
c ---[   5]---> Adder-cost: 73   maxlim: 132   bits: 9/8
c ---[   4]---> Adder-cost: 67   maxlim: 153   bits: 9/8
c ---[   3]---> Adder-cost: 78   maxlim: 118   bits: 8/7
c ---[   2]---> Adder-cost: 54   maxlim: 100   bits: 8/7
c ---[   1]---> Adder-cost: 82   maxlim: 155   bits: 9/8
c ---[   0]---> Adder-cost: 78   maxlim: 179   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  222910   790277 |   74303       0        0     nan |  0.000 % |
c |       100 |  222898   790243 |   81733      97      577     5.9 |  5.895 % |
c |       250 |  222888   790215 |   89906     246     1518     6.2 |  5.900 % |
c |       475 |  222888   790215 |   98897     471     2972     6.3 |  5.900 % |
c |       812 |  222870   790164 |  108787     805     4915     6.1 |  5.908 % |
c |      1318 |  222864   790147 |  119665    1310     8181     6.2 |  5.911 % |
c |      2077 |  222831   790049 |  131632    2065    13701     6.6 |  5.926 % |
c |      3216 |  222819   790015 |  144795    3202    20141     6.3 |  5.931 % |
c |      4925 |  222801   789964 |  159275    4908    32918     6.7 |  5.938 % |
c |      7487 |  222735   789756 |  175202    7451    58483     7.8 |  5.958 % |
c |     11332 |  222672   789557 |  192722   11283    98092     8.7 |  5.976 % |
c |     17098 |  222537   789133 |  211995   17022   175564    10.3 |  6.026 % |
c |     25747 |  222377   788591 |  233194   25634   292663    11.4 |  6.076 % |
c |     38723 |  222210   788079 |  256514   38569   462880    12.0 |  6.139 % |
c |     58185 |  222055   787581 |  282165   58002   939157    16.2 |  6.189 % |
c |     87378 |  221804   786773 |  310382   87096  1286834    14.8 |  6.254 % |
c |    131167 |  221051   784154 |  341420  130324  2177439    16.7 |  6.382 % |
c |    196851 |  220523   782331 |  375562  195357  4807351    24.6 |  6.477 % |
c |    295379 |  220414   781942 |  413118  293790 20288118    69.1 |  6.490 % |
c ==============================================================================
c [1mFound solution: 119948[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11276   maxlim: 201883   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    323219 |  299133  1063067 |   99711  321578 20748338    64.5 |  6.490 % |
c |    323319 |  299133  1063067 |  109682   29907   281133     9.4 |  5.082 % |
c |    323469 |  299133  1063067 |  120650   30057   282229     9.4 |  5.082 % |
c |    323695 |  299133  1063067 |  132715   30283   284482     9.4 |  5.082 % |
c |    324032 |  299133  1063067 |  145986   30620   288256     9.4 |  5.082 % |
c |    324538 |  299133  1063067 |  160585   31126   294109     9.4 |  5.082 % |
c |    325298 |  299133  1063067 |  176644   31886   302047     9.5 |  5.082 % |
c |    326437 |  299133  1063067 |  194308   33025   314412     9.5 |  5.082 % |
c |    328145 |  299133  1063067 |  213739   34733   331304     9.5 |  5.082 % |
c |    330708 |  299133  1063067 |  235113   37296   360180     9.7 |  5.082 % |
c |    334554 |  299133  1063067 |  258624   41142   403032     9.8 |  5.082 % |
c |    340320 |  299100  1062952 |  284487   46897   475310    10.1 |  5.088 % |
c |    348969 |  299091  1062921 |  312935   55545   589099    10.6 |  5.090 % |
c |    361943 |  299058  1062806 |  344229   68511   760505    11.1 |  5.096 % |
c |    381409 |  299046  1062767 |  378652   87974  1239140    14.1 |  5.098 % |
c |    410601 |  299016  1062666 |  416517  117148  1606684    13.7 |  5.104 % |
c |    454392 |  299001  1062613 |  458169  160935  3572990    22.2 |  5.106 % |
c |    520077 |  298947  1062423 |  503986  226600  4520189    19.9 |  5.113 % |
c |    618604 |  298920  1062336 |  554384  325122  7868683    24.2 |  5.119 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 x1 -x2 -x3 -x4 x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 x32 -x33 -x34 x35 -x36 -x37 -x38 -x39 x40 x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 x72 -x73 -x74 -x75 x76 -x77 -x78 -x79 x80 -x81 -x82 -x83 x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 x92 -x93 -x94 x95 x96 -x97 -x98 -x99 -x100 x101 -x102 x103 x104 -x105 -x106 x107 -x108 -x109 -x110 -x111 -x112 -x113 x114 -x115 x116 x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 x141 x142 -x143 x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 x188 -x189 -x190 -x191 x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 x202 x203 -x204 -x205 -x206 x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 x222 x223 x224 x225 -x226 -x227 -x228 -x229 x230 x231 x232 x233 -x234 -x235 -x236 -x237 -x238 x239 -x240 -x241 -x242 -x243 -x244 -x245 x246 -x247 -x248 x249 -x250 -x251 -x252 -x253 x254 -x255 -x256 -x257 -x258 -x259 -x260 x261 -x262 -x263 -x264 -x265 -x266 x267 -x268 x269 x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 x283 -x284 x285 -x286 -x287 -x288 -x289 x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 x311 -x312 -x313 x314 -x315 x316 x317 -x318 x319 x320 x321 x322 x323 -x324 -x325 -x326 -x327 x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 x345 -x346 -x347 -x348 -x349 -x350 x351 -x352 -x353 -x354 -x355 -x356 -x357 x358 -x359 -x360 -x361 x362 -x363 -x364 x365 -x366 -x367 -x368 x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 x395 x396 x397 -x398 -x399 -x400 -x401 x402 -x403 x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 x436 -x437 -x438 -x439 x440 -x441 -x442 -x443 x444 x445 -x446 -x447 x448 -x449 x450 -x451 x452 -x453 -x454 -x455 x456 -x457 -x458 -x459 -x460 -x461 -x462 x463 -x464 -x465 -x466 x467 -x468 -x469 -x470 x471 x472 -x473 -x474 x475 -x476 x477 x478 -x479 -x480 -x481 -x482 -x483 x484 -x485 -x486 x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 x499 x500 -x501 -x502 x503 -x504 x505 -x506 -x507 x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 x544 -x545 -x546 -x547 -x548 -x549 -x550 x551 x552 -x553 -x554 -x555 -x556 -x557 -x558 x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 x569 -x570 -x571 x572 -x573 -x574 -x575 x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 x585 -x586 -x587 -x588 -x589 x590 -x591 -x592 x593 -x594 -x595 -x596 -x597 -x598 -x599 x600 -x601 -x602 -x603 -x604 -x605 x606 -x607 -x608 -x609 x610 -x611 -x612 -x613 x614 -x615 -x616 x617 -x618 x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 x629 -x630 -x631 -x632 -x633 -x634 -x635 x636 -x637 -x638 -x639 -x640 x641 -x642 -x643 -x644 x645 -x646 x647 -x648 -x649 x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 x658 x659 -x660 x661 -x662 x663 -x664 -x665 -x666 x667 -x668 -x669 x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 x699 -x700 -x701 -x702 -x703 -x704 x705 x706 -x707 -x708 -x709 -x710 x711 x712 -x713 -x714 -x715 -x716 x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 x738 x739 -x740 -x741 x742 -x743 -x744 -x745 x746 x747 -x748 -x749 -x750 -x751 x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 x764 -x765 x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 x810 -x811 x812 -x813 -x814 -x815 -x816 -x817 x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 x829 -x830 -x831 -x832 -x833 -x834 -x835 x836 x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 x869 x870 -x871 -x872 -x873 -x874 -x875 -x876 x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 x887 -x888 -x889 -x890 -x891 x892 -x893 x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 x902 -x903 -x904 -x905 -x906 -x907 x908 x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 x918 x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 x973 -x974 -x975 -x976 x977 -x978 -x979 -x980 -x981 -x982 -x983 x984 -x985 -x986 -x987 -x988 -x989 x990 -x991 -x992 -x993 -x994 x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 x1019 -x1020 -x1021 -x1022 -x1023 x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 x1037 -x1038 x1039 -x1040 -x1041 -x1042 -x1043 x1044 -x1045 x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 x1067 x1068 x1069 x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 x1078 -x1079 -x1080 -x1081 x1082 x1083 -x1084 -x1085 -x1086 x1087 x1088 x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 x1135 -x1136 x1137 -x1138 -x1139 x1140 -x1141 -x1142 -x1143 -x1144 x1145 -x1146 x1147 -x1148 -x1149 x1150 x1151 x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 x1159 x1160 -x1161 x1162 -x1163 x1164 x1165 x1166 -x1167 x1168 -x1169 -x1170 x1171 -x1172 -x1173 x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 x1200 x1201 x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 x1215 -x1216 x1217 -x1218 -x1219 -x1220 -x1221 x1222 -x1223 -x1224 -x1225 -x1226 -x1227 x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 x1243 -x1244 -x1245 -x1246 -x1247 -x1248 x1249 -x1250 x1251 -x1252 -x1253 -x1254 -x1255 -x1256 x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 x1276 -x1277 x1278 -x1279 -x1280 -x1281 -x1282 x1283 -x1284 -x1285 x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 x1295 x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 x1318 -x1319 x1320 x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 x1330 x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 x1338 x1339 -x1340 -x1341 -x1342 -x1343 -x1344 x1345 x1346 -x1347 -x1348 x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 x1363 -x1364 -x1365 x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 x1389 -x1390 x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 x1400 -x1401 x1402 -x1403 -x1404 -x1405 x1406 -x1407 x1408 x1409 -x1410 -x1411 x1412 -x1413 x1414 -x1415 -x1416 -x1417 x1418 -x1419 -x1420 x1421 x1422 -x1423 -x1424 -x1425 -x1426 -x1427 x1428 -x1429 -x1430 x1431 -x1432 -x1433 -x1434 -x1435 x1436 x1437 x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 x1450 x1451 -x1452 x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 x1465 -x1466 -x1467 -x1468 -x1469 x1470 -x1471 -x1472 -x1473 x1474 -x1475 x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 x1490 -x1491 -x1492 -x1493 -x1494 x1495 -x1496 -x1497 -x1498 -x1499 -x1500 x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 x1511 x1512 x1513 -x1514 x1515 -x1516 -x1517 -x1518 -x1519 x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 x1533 -x1534 x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 x1564 x1565 -x1566 -x1567 -x1568 x1569 x1570 x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 x1602 x1603 -x1604 -x1605 -x1606 -x1607 x1608 -x1609 -x1610 -x1611 x1612 -x1613 -x1614 x1615 -x1616 -x1617 -x1618 -x1619 x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 x1638 -x1639 -x1640 -x1641 x1642 -x1643 -x1644 x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 x1654 -x1655 -x1656 -x1657 x1658 x1659 -x1660 -x1661 -x1662 -x1663 x1664 -x1665 x1666 x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 x1727 -x1728 -x1729 -x1730 -x1731 x1732 -x1733 -x1734 x1735 -x1736 -x1737 -x1738 -x1739 x1740 -x1741 x1742 -x1743 x1744 -x1745 x1746 -x1747 x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 x1781 -x1782 -x1783 -x1784 x1785 -x1786 x1787 -x1788 -x1789 -x1790 x1791 -x1792 x1793 -x1794 -x1795 -x1796 -x1797 -x1798 x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 x1806 x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 x1823 -x1824 -x1825 -x1826 -x1827 -x1828 x1829 -x1830 -x1831 -x1832 -x1833 x1834 x1835 x1836 x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 x1848 x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 x1857 x1858 x1859 -x1860 -x1861 -x1862 x1863 x1864 -x1865 -x1866 -x1867 -x1868 -x1869 x1870 -x1871 -x1872 -x1873 -x1874 -x1875 x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 x1900 x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 x1914 -x1915 -x1916 -x1917 x1918 -x1919 x1920 -x1921 x1922 -x1923 x1924 x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 x1974 -x1975 x1976 -x1977 -x1978 -x1979 x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 x2004 -x2005 -x2006 -x2007 -x2008 -x2009 x2010 -x2011 -x2012 -x2013 -x2014 -x2015 x2016 -x2017 -x2018 x2019 -x2020 x2021 -x2022 -x2023 -x2024 -x2025 -x2026 x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 x2038 -x2039 -x2040 x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 x2072 -x2073 -x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 x2082 -x2083 -x2084 -x2085 -x2086 -x2087 x2088 -x2089 -x2090 x2091 -x2092 -x2093 -x2094 -x2095 x2096 -x2097 -x2098 -x2099 x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 x2126 -x2127 -x2128 x2129 -x2130 -x2131 -x2132 x2133 x2134 -x2135 -x2136 -x2137 x2138 -x2139 x2140 -x2141 x2142 -x2143 x2144 -x2145 x2146 x2147 x2148 x2149 -x2150 x2151 x2152 x2153 x2154 x2155 x2156 x2157 x2158 x2159 -x2160 x2161 x2162 -x2163 -x2164 -x2165 -x2643 -x2644 -x2640 -x2641 -x2635 -x2636 -x2632 -x2633 -x2629 x2630 -x2626 -x2627 -x2623 -x2624 -x2618 -x2619 -x2614 x2615 -x2611 -x2612 -x2608 -x2609 -x2477 -x2478 -x2474 -x2475 x2471 -x2472 -x2467 -x2468 -x2463 -x2464 -x2555 x2556 -x2560 -x2561 -x2564 -x2565 -x2568 -x2569 -x2572 -x2573 x2583 -x2584 -x2587 -x2588 -x2590 -x2591 -x2593 x2594 -x2597 -x2598 -x2604 -x2605 -x2507 -x2508 x2504 -x2505 -x2501 x2502 -x2498 -x2499 -x2494 -x2495 -x2490 x2491 -x2485 -x2486 -x2480 -x2481 -x2458 x2459 -x2453 -x2454 -x2448 -x2449 -x2444 x2445 -x2437 -x2438 -x2432 -x2433 -x2425 -x2426 -x2419 -x2420 -x2413 -x2414 -x2405 -x2406 -x2399 -x2400 -x2378 -x2379 -x2371 x2372 -x2366 -x2367 x2363 -x2364 -x2360 -x2361 -x2357 -x2358 -x2352 -x2353 -x2348 x2349 -x2345 -x2346 -x2342 -x2343 -x2331 -x2332 -x2328 x2329 -x2325 -x2326 -x2322 -x2323 x2175 -x2176 -x2171 -x2172 -x2250 -x2251 -x2263 -x2264 -x2266 x2267 x2269 -x2270 -x2272 -x2273 x2276 -x2277 -x2284 -x2285 -x2287 -x2288 -x2290 -x2291 -x2293 -x2294 x2296 -x2297 -x2307 -x2308 -x2310 -x2311 x2313 -x2314 -x2317 -x2318 -x2392 -x2393 -x2386 x2387 x2235 -x2236 -x2231 -x2232 -x2227 -x2228 x2223 -x2224 -x2219 -x2220 x2214 -x2215 x2202 -x2203 -x2198 -x2199 -x2194 -x2195 -x2191 -x2192 x2187 -x2188 -x2183 -x2184 -x2179 -x2180 x2166 -x2167 -x2246 -x2247 -x2242 -x2243 -x2239 -x2240 -x2578 -x2404 -x2258 -x2208 -x2647 -x2256 -x2257 -x2212 x2190 -x2193 -x2390 -x2435 -x2752 -x2753 -x2301 -x2170 -x2169 -x2173 -x2174 x2218 -x2217 x2221 -x2222 -x2238 -x2241 -x2336 -x2305 x2648 -x2649 -x2340 -x2337 -x2302 -x2754 -x2750 -x2751 -x2245 -x2237 x2216 -x2197 -x2189 -x2168 x2391 -x2389 x2394 -x2397 x2395 -x2396 -x2398 -x2376 x2375 -x2377 -x2374 -x2380 -x2384 -x2382 -x2383 -x2381 -x2385 -x2338 -x2339 -x2303 -x2304 x2559 -x2558 -x2562 -x2563 -x2225 x2226 -x2177 -x2178 -x2607 -x2610 -x2628 -x2586 -x2589 -x2489 -x2488 -x2492 -x2493 -x2462 -x2461 x2465 -x2466 x2452 -x2455 -x2436 -x2439 -x2442 -x2440 -x2441 -x2443 -x2424 -x2423 -x2422 -x2427 -x2430 -x2428 -x2429 -x2431 -x2412 -x2415 -x2416 -x2204 -x2205 -x2233 -x2234 -x2298 -x2185 -x2186 x2252 -x2253 -x2456 -x2457 x2417 x2418 -x2275 x2278 -x2279 -x2702 x2703 -x2704 -x2292 -x2320 -x2321 -x2295 -x2566 -x2658 -x2659 -x2660 -x2663 -x2662 -x2661 -x2664 -x2403 -x2407 -x2410 -x2408 -x2409 -x2402 -x2411 -x2631 -x2280 -x2282 -x2281 x2283 -x2274 -x2271 -x2670 x2669 -x2672 -x2671 -x2673 -x2674 -x2675 -x2676 -x2679 -x2678 -x2677 -x2680 -x2312 -x2685 -x2686 -x2687 -x2362 -x2592 -x2369 -x2370 -x2613 -x2700 -x2701 -x2355 -x2356 -x2654 -x2653 -x2656 -x2655 -x2657 -x2543 -x2544 x2447 -x2450 -x2451 -x2697 -x2698 -x2699 -x2551 -x2552 -x2710 -x2709 -x2712 -x2711 -x2713 -x2726 -x2725 -x2728 x2727 -x2729#### 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.68 0.92 0.86 2/54 3505
Raw data (stat): 3505 (runsolver) R 3504 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487725999 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.73 0.92 0.86 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 4961 0 0 0 987 11 0 0 25 0 1 0 487725999 23040000 4786 4294967295 134512640 134672761 3221224576 3221223776 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5625 4786 603 41 0 5584 0
vsize: 22500
[startup+20.0019 s]
Raw data (loadavg): 0.77 0.92 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 5292 0 0 0 1985 13 0 0 25 0 1 0 487725999 24440832 5117 4294967295 134512640 134672761 3221224576 3221223648 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5117 603 41 0 5926 0
vsize: 23868
[startup+30.0021 s]
Raw data (loadavg): 0.80 0.93 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 5635 0 0 0 2983 14 0 0 25 0 1 0 487725999 25903104 5460 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6324 5460 603 41 0 6283 0
vsize: 25296
[startup+40.002 s]
Raw data (loadavg): 0.83 0.93 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 6136 0 0 0 3981 16 0 0 25 0 1 0 487725999 27914240 5961 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6815 5961 603 41 0 6774 0
vsize: 27260
[startup+50.0027 s]
Raw data (loadavg): 0.86 0.93 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 6480 0 0 0 4981 16 0 0 25 0 1 0 487725999 29274112 6305 4294967295 134512640 134672761 3221224576 3221223728 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7147 6305 603 41 0 7106 0
vsize: 28588
[startup+60.0031 s]
Raw data (loadavg): 0.88 0.93 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 6719 0 0 0 5979 18 0 0 25 0 1 0 487725999 30470144 6544 4294967295 134512640 134672761 3221224576 3221223700 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7439 6544 603 41 0 7398 0
vsize: 29756
[startup+70.0031 s]
Raw data (loadavg): 0.90 0.93 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 6893 0 0 0 6979 18 0 0 25 0 1 0 487725999 31137792 6718 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7602 6718 603 41 0 7561 0
vsize: 30408
[startup+80.0028 s]
Raw data (loadavg): 0.91 0.94 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 7172 0 0 0 7978 20 0 0 25 0 1 0 487725999 32210944 6997 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7864 6997 603 41 0 7823 0
vsize: 31456
[startup+90.0032 s]
Raw data (loadavg): 0.93 0.94 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 7496 0 0 0 8978 20 0 0 25 0 1 0 487725999 33415168 7321 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8158 7321 603 41 0 8117 0
vsize: 32632
[startup+100.003 s]
Raw data (loadavg): 0.94 0.94 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 7728 0 0 0 9977 21 0 0 25 0 1 0 487725999 34353152 7553 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8387 7553 603 41 0 8346 0
vsize: 33548
[startup+110.004 s]
Raw data (loadavg): 0.95 0.94 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 8232 0 0 0 10976 22 0 0 25 0 1 0 487725999 36372480 8057 4294967295 134512640 134672761 3221224576 3221223712 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8880 8057 603 41 0 8839 0
vsize: 35520
[startup+120.004 s]
Raw data (loadavg): 0.95 0.94 0.87 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 8515 0 0 0 11976 23 0 0 25 0 1 0 487725999 38105088 8340 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9303 8340 603 41 0 9262 0
vsize: 37212
[startup+130.004 s]
Raw data (loadavg): 0.96 0.94 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 9699 0 0 0 12973 26 0 0 25 0 1 0 487725999 42934272 9524 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10482 9524 603 41 0 10441 0
vsize: 41928
[startup+140.005 s]
Raw data (loadavg): 0.97 0.94 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 10076 0 0 0 13972 27 0 0 25 0 1 0 487725999 44417024 9901 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10844 9901 603 41 0 10803 0
vsize: 43376
[startup+150.005 s]
Raw data (loadavg): 0.97 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 10648 0 0 0 14971 28 0 0 25 0 1 0 487725999 46690304 10473 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11399 10473 603 41 0 11358 0
vsize: 45596
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 10837 0 0 0 15970 29 0 0 25 0 1 0 487725999 47497216 10662 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11596 10662 603 41 0 11555 0
vsize: 46384
[startup+170.006 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 11011 0 0 0 16970 30 0 0 25 0 1 0 487725999 48173056 10836 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11761 10836 603 41 0 11720 0
vsize: 47044
[startup+180.006 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 11213 0 0 0 17970 30 0 0 25 0 1 0 487725999 48844800 11038 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11038 603 41 0 11884 0
vsize: 47700
[startup+190.007 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 11496 0 0 0 18970 31 0 0 25 0 1 0 487725999 50057216 11321 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12221 11321 603 41 0 12180 0
vsize: 48884
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 11660 0 0 0 19969 31 0 0 25 0 1 0 487725999 50733056 11485 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12386 11485 603 41 0 12345 0
vsize: 49544
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 11946 0 0 0 20968 32 0 0 25 0 1 0 487725999 51810304 11771 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12649 11771 603 41 0 12608 0
vsize: 50596
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 12385 0 0 0 21967 33 0 0 25 0 1 0 487725999 53555200 12210 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13075 12211 603 41 0 13034 0
vsize: 52300
[startup+230.007 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 12839 0 0 0 22966 35 0 0 25 0 1 0 487725999 55439360 12664 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13535 12664 603 41 0 13494 0
vsize: 54140
[startup+240.008 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 13149 0 0 0 23965 35 0 0 25 0 1 0 487725999 56639488 12974 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13828 12974 603 41 0 13787 0
vsize: 55312
[startup+250.008 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 14277 0 0 0 24963 38 0 0 25 0 1 0 487725999 61218816 14102 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14946 14102 603 41 0 14905 0
vsize: 59784
[startup+260.009 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 15153 0 0 0 25961 40 0 0 25 0 1 0 487725999 64847872 14978 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15832 14978 603 41 0 15791 0
vsize: 63328
[startup+270.008 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 15905 0 0 0 26958 43 0 0 25 0 1 0 487725999 67960832 15730 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16592 15730 603 41 0 16551 0
vsize: 66368
[startup+280.008 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 16624 0 0 0 27957 45 0 0 25 0 1 0 487725999 70795264 16449 4294967295 134512640 134672761 3221224576 3221223680 134555216 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17284 16449 603 41 0 17243 0
vsize: 69136
[startup+290.009 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 17306 0 0 0 28955 47 0 0 25 0 1 0 487725999 73617408 17131 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17973 17131 603 41 0 17932 0
vsize: 71892
[startup+300.008 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 17954 0 0 0 29953 49 0 0 25 0 1 0 487725999 76296192 17779 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18627 17779 603 41 0 18586 0
vsize: 74508
[startup+310.009 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 18612 0 0 0 30952 50 0 0 25 0 1 0 487725999 78970880 18437 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19280 18438 603 41 0 19239 0
vsize: 77120
[startup+320.01 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 19241 0 0 0 31950 53 0 0 25 0 1 0 487725999 81522688 19066 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19903 19066 603 41 0 19862 0
vsize: 79612
[startup+330.009 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 19824 0 0 0 32947 56 0 0 25 0 1 0 487725999 83947520 19649 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20495 19649 603 41 0 20454 0
vsize: 81980
[startup+340.009 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 20366 0 0 0 33946 57 0 0 25 0 1 0 487725999 86097920 20191 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21020 20191 603 41 0 20979 0
vsize: 84080
[startup+350.009 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 20935 0 0 0 34944 58 0 0 25 0 1 0 487725999 88412160 20760 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21585 20760 603 41 0 21544 0
vsize: 86340
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 21459 0 0 0 35944 59 0 0 25 0 1 0 487725999 90558464 21284 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22109 21284 603 41 0 22068 0
vsize: 88436
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 21974 0 0 0 36942 61 0 0 25 0 1 0 487725999 93761536 21799 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22891 21799 603 41 0 22850 0
vsize: 91564
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 22448 0 0 0 37941 63 0 0 25 0 1 0 487725999 95789056 22273 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23386 22273 603 41 0 23345 0
vsize: 93544
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 22922 0 0 0 38940 63 0 0 25 0 1 0 487725999 97705984 22747 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23854 22747 603 41 0 23813 0
vsize: 95416
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 23332 0 0 0 39939 65 0 0 25 0 1 0 487725999 99479552 23157 4294967295 134512640 134672761 3221224576 3221223728 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 23157 603 41 0 24246 0
vsize: 97148
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 23767 0 0 0 40938 66 0 0 25 0 1 0 487725999 101281792 23592 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24727 23592 603 41 0 24686 0
vsize: 98908
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 24224 0 0 0 41937 67 0 0 25 0 1 0 487725999 103161856 24049 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25186 24049 603 41 0 25145 0
vsize: 100744
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 24664 0 0 0 42936 69 0 0 25 0 1 0 487725999 104906752 24489 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25612 24489 603 41 0 25571 0
vsize: 102448
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 25081 0 0 0 43935 70 0 0 25 0 1 0 487725999 106655744 24906 4294967295 134512640 134672761 3221224576 3221223760 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26039 24906 603 41 0 25998 0
vsize: 104156
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 25550 0 0 0 44934 71 0 0 25 0 1 0 487725999 108535808 25375 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26498 25375 603 41 0 26457 0
vsize: 105992
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 25977 0 0 0 45932 73 0 0 25 0 1 0 487725999 110276608 25802 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26923 25802 603 41 0 26882 0
vsize: 107692
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 26370 0 0 0 46931 74 0 0 25 0 1 0 487725999 111894528 26195 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27318 26195 603 41 0 27277 0
vsize: 109272
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 26773 0 0 0 47931 75 0 0 25 0 1 0 487725999 113504256 26598 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27711 26598 603 41 0 27670 0
vsize: 110844
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 27168 0 0 0 48930 76 0 0 25 0 1 0 487725999 115126272 26993 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28107 26993 603 41 0 28066 0
vsize: 112428
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 27532 0 0 0 49929 77 0 0 25 0 1 0 487725999 116600832 27357 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28467 27357 603 41 0 28426 0
vsize: 113868
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 27882 0 0 0 50929 77 0 0 25 0 1 0 487725999 118083584 27707 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28829 27707 603 41 0 28788 0
vsize: 115316
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 28180 0 0 0 51927 78 0 0 25 0 1 0 487725999 119222272 28005 4294967295 134512640 134672761 3221224576 3221223792 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 28005 603 41 0 29066 0
vsize: 116428
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 28433 0 0 0 52925 80 0 0 25 0 1 0 487725999 120303616 28258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29371 28258 603 41 0 29330 0
vsize: 117484
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 28644 0 0 0 53925 80 0 0 25 0 1 0 487725999 121122816 28469 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29571 28469 603 41 0 29530 0
vsize: 118284
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 28799 0 0 0 54925 81 0 0 25 0 1 0 487725999 121794560 28624 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29735 28624 603 41 0 29694 0
vsize: 118940
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30134 0 0 0 55923 83 0 0 25 0 1 0 487725999 127115264 29959 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29959 603 41 0 30993 0
vsize: 124136
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30134 0 0 0 56923 83 0 0 25 0 1 0 487725999 127115264 29959 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29959 603 41 0 30993 0
vsize: 124136
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 57923 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 58923 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 59923 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223728 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 60924 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 61924 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 62924 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30139 0 0 0 63924 83 0 0 25 0 1 0 487725999 127115264 29964 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29964 603 41 0 30993 0
vsize: 124136
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30141 0 0 0 64924 83 0 0 25 0 1 0 487725999 127115264 29966 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29966 603 41 0 30993 0
vsize: 124136
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 65925 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 66925 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 67925 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 68925 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 69925 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 70926 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 71926 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 72926 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 73926 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 74926 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 75927 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 76927 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 77927 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 78927 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 79927 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 80928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 81928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 82928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 83928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223728 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 84928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 85929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 86928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 87928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 88928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 89928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 90928 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 91929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 92929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 93929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 94929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 95929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 96929 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 97930 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 98930 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 99930 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 100930 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 101930 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 102930 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 103931 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 104931 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30142 0 0 0 105931 83 0 0 25 0 1 0 487725999 127115264 29967 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29967 603 41 0 30993 0
vsize: 124136
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30145 0 0 0 106931 83 0 0 25 0 1 0 487725999 127115264 29970 4294967295 134512640 134672761 3221224576 3221223744 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29970 603 41 0 30993 0
vsize: 124136
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30147 0 0 0 107931 83 0 0 25 0 1 0 487725999 127115264 29972 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29972 603 41 0 30993 0
vsize: 124136
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30151 0 0 0 108931 83 0 0 25 0 1 0 487725999 127115264 29976 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29976 603 41 0 30993 0
vsize: 124136
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30155 0 0 0 109931 83 0 0 25 0 1 0 487725999 127115264 29980 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29980 603 41 0 30993 0
vsize: 124136
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30159 0 0 0 110931 84 0 0 25 0 1 0 487725999 127115264 29984 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29984 603 41 0 30993 0
vsize: 124136
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30161 0 0 0 111931 84 0 0 25 0 1 0 487725999 127115264 29986 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29986 603 41 0 30993 0
vsize: 124136
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30164 0 0 0 112932 84 0 0 25 0 1 0 487725999 127115264 29989 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29989 603 41 0 30993 0
vsize: 124136
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30167 0 0 0 113932 84 0 0 25 0 1 0 487725999 127115264 29992 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29992 603 41 0 30993 0
vsize: 124136
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30170 0 0 0 114932 84 0 0 25 0 1 0 487725999 127115264 29995 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29995 603 41 0 30993 0
vsize: 124136
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30173 0 0 0 115932 84 0 0 25 0 1 0 487725999 127115264 29998 4294967295 134512640 134672761 3221224576 3221223700 134566151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 29998 603 41 0 30993 0
vsize: 124136
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30176 0 0 0 116932 84 0 0 25 0 1 0 487725999 127115264 30001 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 30001 603 41 0 30993 0
vsize: 124136
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30179 0 0 0 117933 84 0 0 25 0 1 0 487725999 127115264 30004 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 30004 603 41 0 30993 0
vsize: 124136
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30182 0 0 0 118933 84 0 0 25 0 1 0 487725999 127115264 30007 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 30007 603 41 0 30993 0
vsize: 124136
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3505
Raw data (stat): 3505 (minisat+) R 3504 26298 26297 0 -1 0 30188 0 0 0 119933 84 0 0 25 0 1 0 487725999 127115264 30013 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31034 30013 603 41 0 30993 0
vsize: 124136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3505
Raw data (stat): 3505 (minisat+) Z 3504 26298 26297 0 -1 12 30191 0 0 0 119933 89 0 0 25 0 1 0 487725999 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.24
CPU user time (s): 1199.34
CPU system time (s): 0.897863
CPU usage (%): 100.012
Max. virtual memory (Kb): 124136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####