PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

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

General information on the benchmark

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

Trace number 16066

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        318620 kB
Buffers:         37976 kB
Cached:         636788 kB
SwapCached:          0 kB
Active:         190268 kB
Inactive:       487352 kB
HighTotal:      131008 kB
HighFree:        18396 kB
LowTotal:       903652 kB
LowFree:        300224 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            32624 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:32:08 (client local time) WITH STATUS 0 IN 4.32834 SECONDS
stats: 15683 7 4.32834 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 665 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[ 667]---> Adder-cost: 1514   maxlim: 182446   bits: 18/18
c ---[ 666]---> Adder-cost: 1514   maxlim: 103596   bits: 17/17
c ---[ 665]---> Adder-cost: 1168   maxlim: 90177   bits: 17/17
c ---[ 663]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 659]---> Adder-cost: 256   maxlim: 2167   bits: 13/12
c ---[ 657]---> Adder-cost: 256   maxlim: 2295   bits: 13/12
c ---[ 655]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 647]---> Adder-cost: 496   maxlim: 4335   bits: 13/13
c ---[ 645]---> Adder-cost: 528   maxlim: 4335   bits: 14/13
c ---[ 643]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 639]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 637]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 635]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 631]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 629]---> Adder-cost: 336   maxlim: 2805   bits: 13/12
c ---[ 627]---> BDD-cost:   22
c ---[ 625]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 623]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 621]---> Adder-cost: 632   maxlim: 5228   bits: 14/13
c ---[ 619]---> Adder-cost: 600   maxlim: 4845   bits: 14/13
c ---[ 617]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 832   maxlim: 6375   bits: 14/13
c ---[ 607]---> Adder-cost: 848   maxlim: 6758   bits: 14/13
c ---[ 605]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 585]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[ 583]---> Adder-cost: 224   maxlim: 2040   bits: 12/11
c ---[ 581]---> Adder-cost: 464   maxlim: 3825   bits: 13/12
c ---[ 579]---> Adder-cost: 480   maxlim: 4080   bits: 13/12
c ---[ 577]---> BDD-cost:   64
c ---[ 576]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[ 571]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 570]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 568]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> BDD-cost:   67
c ---[ 564]---> BDD-cost:   67
c ---[ 563]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 7
c ---[ 561]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 1654     Base: 2 2 2 2 2 2 2 7
c ---[ 559]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 7
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   67
c ---[ 556]---> BDD-cost:   67
c ---[ 555]---> BDD-cost:   68
c ---[ 554]---> BDD-cost:   67
c ---[ 553]---> BDD-cost:   67
c ---[ 552]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost:  854     Base: 2 2 2 2 2 2 2 7
c ---[ 546]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 544]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 543]---> Adder-cost: 167   maxlim: 1529   bits: 12/11
c ---[ 542]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 7
c ---[ 541]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 7
c ---[ 540]---> Adder-cost: 217   maxlim: 2039   bits: 12/11
c ---[ 539]---> Adder-cost: 230   maxlim: 1911   bits: 12/11
c ---[ 538]---> Adder-cost: 230   maxlim: 2039   bits: 12/11
c ---[ 537]---> Adder-cost: 217   maxlim: 2294   bits: 13/12
c ---[ 536]---> Adder-cost: 224   maxlim: 2166   bits: 13/12
c ---[ 535]---> Adder-cost: 240   maxlim: 2294   bits: 13/12
c ---[ 534]---> Adder-cost: 262   maxlim: 3059   bits: 13/12
c ---[ 533]---> Adder-cost: 295   maxlim: 2931   bits: 13/12
c ---[ 532]---> Adder-cost: 311   maxlim: 3059   bits: 13/12
c ---[ 531]---> Adder-cost: 346   maxlim: 3314   bits: 13/12
c ---[ 530]---> Adder-cost: 361   maxlim: 3186   bits: 13/12
c ---[ 529]---> Adder-cost: 361   maxlim: 3314   bits: 13/12
c ---[ 528]---> Adder-cost: 346   maxlim: 3569   bits: 13/12
c ---[ 527]---> Adder-cost: 377   maxlim: 3441   bits: 13/12
c ---[ 526]---> Adder-cost: 393   maxlim: 3569   bits: 13/12
c ---[ 525]---> Adder-cost: 304   maxlim: 3824   bits: 13/12
c ---[ 524]---> Adder-cost: 323   maxlim: 3696   bits: 13/12
c ---[ 523]---> Adder-cost: 405   maxlim: 3824   bits: 13/12
c ---[ 522]---> BDD-cost:   68
c ---[ 521]---> BDD-cost:   67
c ---[ 520]---> BDD-cost:   67
c ---[ 519]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 513]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 511]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 7
c ---[ 509]---> BDD-cost:   67
c ---[ 508]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 167   maxlim: 1784   bits: 12/11
c ---[ 506]---> Sorter-cost: 1753     Base: 2 2 2 2 2 2 2 7
c ---[ 505]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 504]---> Adder-cost: 199   maxlim: 2294   bits: 13/12
c ---[ 503]---> Adder-cost: 214   maxlim: 2294   bits: 13/12
c ---[ 502]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 7
c ---[ 501]---> Adder-cost: 225   maxlim: 2549   bits: 13/12
c ---[ 500]---> Adder-cost: 240   maxlim: 2549   bits: 13/12
c ---[ 499]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> BDD-cost:   68
c ---[ 496]---> BDD-cost:   67
c ---[ 495]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1359     Base: 2 2 2 2 2 2 2 7
c ---[ 493]---> Adder-cost: 185   maxlim: 1274   bits: 12/11
c ---[ 492]---> Adder-cost: 196   maxlim: 1274   bits: 12/11
c ---[ 491]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> BDD-cost:   68
c ---[ 489]---> BDD-cost:   67
c ---[ 488]---> BDD-cost:   67
c ---[ 487]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  456     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 481]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 479]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 478]---> Adder-cost: 135   maxlim: 1274   bits: 12/11
c ---[ 477]---> Sorter-cost: 1722     Base: 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1722     Base: 2 2 2 2 2 2 2 7
c ---[ 475]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 7
c ---[ 471]---> Adder-cost: 149   maxlim: 764   bits: 11/10
c ---[ 470]---> BDD-cost:   67
c ---[ 469]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Adder-cost: 249   maxlim: 1784   bits: 12/11
c ---[ 467]---> Adder-cost: 230   maxlim: 1657   bits: 12/11
c ---[ 466]---> Adder-cost: 210   maxlim: 2039   bits: 12/11
c ---[ 465]---> Adder-cost: 206   maxlim: 1912   bits: 12/11
c ---[ 464]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 463]---> Adder-cost: 297   maxlim: 2167   bits: 13/12
c ---[ 462]---> Adder-cost: 294   maxlim: 2422   bits: 13/12
c ---[ 461]---> Adder-cost: 286   maxlim: 2677   bits: 13/12
c ---[ 460]---> Adder-cost: 269   maxlim: 2422   bits: 13/12
c ---[ 459]---> Sorter-cost: 1587     Base: 2 2 2 2 2 2 2 7
c ---[ 458]---> Adder-cost: 426   maxlim: 2804   bits: 13/12
c ---[ 457]---> Adder-cost: 456   maxlim: 3186   bits: 13/12
c ---[ 456]---> Adder-cost: 439   maxlim: 3059   bits: 13/12
c ---[ 455]---> BDD-cost:   66
c ---[ 454]---> BDD-cost:   65
c ---[ 453]---> BDD-cost:   67
c ---[ 452]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> BDD-cost:   68
c ---[ 446]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 442]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:  475     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 438]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 7
c ---[ 437]---> Adder-cost: 185   maxlim: 1912   bits: 12/11
c ---[ 436]---> Adder-cost: 200   maxlim: 2167   bits: 13/12
c ---[ 435]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 434]---> Adder-cost: 266   maxlim: 2677   bits: 13/12
c ---[ 433]---> Adder-cost: 279   maxlim: 2932   bits: 13/12
c ---[ 432]---> Adder-cost: 256   maxlim: 2677   bits: 13/12
c ---[ 431]---> Adder-cost: 314   maxlim: 2932   bits: 13/12
c ---[ 430]---> Adder-cost: 309   maxlim: 3187   bits: 13/12
c ---[ 429]---> Adder-cost: 222   maxlim: 3187   bits: 13/12
c ---[ 428]---> Adder-cost: 296   maxlim: 3569   bits: 13/12
c ---[ 427]---> Adder-cost: 339   maxlim: 3952   bits: 13/12
c ---[ 426]---> Adder-cost: 287   maxlim: 3442   bits: 13/12
c ---[ 425]---> Adder-cost: 258   maxlim: 3442   bits: 13/12
c ---[ 424]---> Adder-cost: 422   maxlim: 4079   bits: 13/12
c ---[ 423]---> Adder-cost: 442   maxlim: 4462   bits: 14/13
c ---[ 422]---> Adder-cost: 391   maxlim: 3952   bits: 13/12
c ---[ 421]---> Adder-cost: 421   maxlim: 4844   bits: 14/13
c ---[ 420]---> Adder-cost: 420   maxlim: 5227   bits: 14/13
c ---[ 419]---> Adder-cost: 490   maxlim: 4462   bits: 14/13
c ---[ 418]---> Adder-cost: 493   maxlim: 5609   bits: 14/13
c ---[ 417]---> Adder-cost: 470   maxlim: 5992   bits: 14/13
c ---[ 416]---> Adder-cost: 496   maxlim: 5227   bits: 14/13
c ---[ 415]---> Adder-cost: 553   maxlim: 5864   bits: 14/13
c ---[ 414]---> Adder-cost: 562   maxlim: 6247   bits: 14/13
c ---[ 413]---> Adder-cost: 610   maxlim: 5482   bits: 14/13
c ---[ 412]---> Adder-cost: 597   maxlim: 6119   bits: 14/13
c ---[ 411]---> Adder-cost: 598   maxlim: 6502   bits: 14/13
c ---[ 410]---> Adder-cost: 564   maxlim: 5737   bits: 14/13
c ---[ 409]---> BDD-cost:   27
c ---[ 408]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> BDD-cost:   67
c ---[ 406]---> BDD-cost:   67
c ---[ 405]---> BDD-cost:   68
c ---[ 404]---> BDD-cost:   67
c ---[ 403]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 7
c ---[ 399]---> BDD-cost:   68
c ---[ 398]---> BDD-cost:   67
c ---[ 397]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> BDD-cost:   67
c ---[ 394]---> BDD-cost:   66
c ---[ 393]---> BDD-cost:   65
c ---[ 392]---> BDD-cost:   67
c ---[ 391]---> BDD-cost:   66
c ---[ 390]---> BDD-cost:   65
c ---[ 389]---> BDD-cost:   67
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> BDD-cost:   68
c ---[ 383]---> BDD-cost:   67
c ---[ 382]---> BDD-cost:   67
c ---[ 381]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 7
c ---[ 377]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 7
c ---[ 376]---> BDD-cost:   67
c ---[ 374]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Adder-cost: 167   maxlim: 1275   bits: 12/11
c ---[ 370]---> Adder-cost: 184   maxlim: 1274   bits: 12/11
c ---[ 369]---> Adder-cost: 185   maxlim: 1785   bits: 12/11
c ---[ 368]---> Adder-cost: 182   maxlim: 1784   bits: 12/11
c ---[ 367]---> Adder-cost: 233   maxlim: 2040   bits: 12/11
c ---[ 366]---> Adder-cost: 240   maxlim: 2039   bits: 12/11
c ---[ 365]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 7
c ---[ 364]---> Adder-cost: 228   maxlim: 2295   bits: 13/12
c ---[ 363]---> Adder-cost: 245   maxlim: 2294   bits: 13/12
c ---[ 362]---> Adder-cost: 410   maxlim: 2294   bits: 13/12
c ---[ 361]---> Adder-cost: 409   maxlim: 2549   bits: 13/12
c ---[ 360]---> Adder-cost: 304   maxlim: 2549   bits: 13/12
c ---[ 359]---> Adder-cost: 335   maxlim: 2804   bits: 13/12
c ---[ 358]---> BDD-cost:   65
c ---[ 357]---> BDD-cost:   67
c ---[ 355]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   35
c ---[ 351]---> BDD-cost:   35
c ---[ 349]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   35
c ---[ 343]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   35
c ---[ 333]---> BDD-cost:   35
c ---[ 331]---> BDD-cost:   35
c ---[ 329]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 323]---> BDD-cost:   35
c ---[ 321]---> BDD-cost:   35
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   35
c ---[ 313]---> BDD-cost:   35
c ---[ 311]---> BDD-cost:   35
c ---[ 309]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   35
c ---[ 305]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   35
c ---[ 295]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   35
c ---[ 287]---> BDD-cost:   35
c ---[ 285]---> BDD-cost:   35
c ---[ 283]---> BDD-cost:   35
c ---[ 281]---> BDD-cost:   35
c ---[ 279]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   35
c ---[ 275]---> BDD-cost:   35
c ---[ 273]---> BDD-cost:   35
c ---[ 271]---> BDD-cost:   35
c ---[ 269]---> BDD-cost:   35
c ---[ 267]---> BDD-cost:   35
c ---[ 265]---> BDD-cost:   35
c ---[ 263]---> BDD-cost:   35
c ---[ 261]---> BDD-cost:   35
c ---[ 259]---> BDD-cost:   35
c ---[ 257]---> BDD-cost:   35
c ---[ 255]---> BDD-cost:   35
c ---[ 253]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   35
c ---[ 243]---> BDD-cost:   35
c ---[ 241]---> BDD-cost:   35
c ---[ 239]---> BDD-cost:   35
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   35
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 143]---> BDD-cost:   76
c ---[ 141]---> BDD-cost:   76
c ---[ 139]---> BDD-cost:   76
c ---[ 137]---> BDD-cost:   76
c ---[ 135]---> BDD-cost:   76
c ---[ 133]---> BDD-cost:   76
c ---[ 131]---> BDD-cost:   76
c ---[ 129]---> BDD-cost:   76
c ---[ 127]---> BDD-cost:   76
c ---[ 125]---> BDD-cost:   76
c ---[ 123]---> BDD-cost:   76
c ---[ 121]---> BDD-cost:   76
c ---[ 119]---> BDD-cost:   76
c ---[ 117]---> BDD-cost:   76
c ---[ 115]---> BDD-cost:   76
c ---[ 113]---> BDD-cost:   76
c ---[ 111]---> BDD-cost:   35
c ---[ 109]---> BDD-cost:   76
c ---[ 107]---> BDD-cost:   76
c ---[ 105]---> BDD-cost:   76
c ---[ 103]---> BDD-cost:   76
c ---[ 101]---> BDD-cost:   76
c ---[  99]---> BDD-cost:   76
c ---[  97]---> BDD-cost:   76
c ---[  95]---> BDD-cost:   76
c ---[  93]---> BDD-cost:   76
c ---[  91]---> BDD-cost:   76
c ---[  89]---> BDD-cost:   76
c ---[  87]---> BDD-cost:   76
c ---[  85]---> BDD-cost:   76
c ---[  83]---> BDD-cost:   76
c ---[  81]---> BDD-cost:   76
c ---[  79]---> BDD-cost:   76
c ---[  77]---> BDD-cost:   76
c ---[  75]---> BDD-cost:   76
c ---[  73]---> BDD-cost:   76
c ---[  71]---> BDD-cost:   76
c ---[  69]---> BDD-cost:   76
c ---[  67]---> BDD-cost:   76
c ---[  65]---> BDD-cost:   76
c ---[  63]---> BDD-cost:   76
c ---[  61]---> BDD-cost:   76
c ---[  59]---> BDD-cost:   76
c ---[  57]---> BDD-cost:   76
c ---[  55]---> BDD-cost:   76
c ---[  53]---> BDD-cost:   76
c ---[  51]---> BDD-cost:   76
c ---[  49]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  41]---> BDD-cost:   76
c ---[  39]---> BDD-cost:   76
c ---[  37]---> BDD-cost:   76
c ---[  35]---> BDD-cost:   76
c ---[  33]---> BDD-cost:   76
c ---[  31]---> BDD-cost:   35
c ---[  29]---> BDD-cost:   35
c ---[  27]---> BDD-cost:   76
c ---[  25]---> BDD-cost:   76
c ---[  23]---> BDD-cost:   76
c ---[  21]---> BDD-cost:   76
c ---[  19]---> BDD-cost:   76
c ---[  17]---> #### 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.85 0.94 0.94 2/54 24575
Raw data (stat): 24575 (runsolver) R 24574 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542947492 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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+4.34069 s]
Raw data (loadavg): 0.85 0.94 0.94 1/53 24575
Raw data (stat): 24575 (runsolver) R 24574 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542947492 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 4.34042
CPU time (s): 4.32834
CPU user time (s): 4.09238
CPU system time (s): 0.235964
CPU usage (%): 99.7218
Max. virtual memory (Kb): 1028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####