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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst2.opb
MD5SUM	3c3e6264ad2029dcb2dc81be78ef5988
Bench Category	optimization, medium integers (OPTMEDINT)
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	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	13633395
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	103.29
Number of variables	9183
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	40
Number of constraints which are nor clauses,nor cardinality constraints	592
Minimum length of a constraint	1
Maximum length of a constraint	260
Trace number 17569

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        794912 kB
Buffers:          2428 kB
Cached:         212044 kB
SwapCached:          0 kB
Active:          36804 kB
Inactive:       180792 kB
HighTotal:      131008 kB
HighFree:        63980 kB
LowTotal:       903652 kB
LowFree:        730932 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16392 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:01:33 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 19432 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 725 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 724]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 723]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 722]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 721]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 720]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 719]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 718]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 717]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 716]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 715]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 714]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 713]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 712]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 711]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 710]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 709]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 708]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 707]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 706]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 705]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 704]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 702]---> Adder-cost: 334   maxlim: 113401   bits: 18/17
c ---[ 700]---> Adder-cost: 334   maxlim: 113785   bits: 18/17
c ---[ 698]---> Adder-cost: 326   maxlim: 121209   bits: 18/17
c ---[ 696]---> Adder-cost: 326   maxlim: 121337   bits: 18/17
c ---[ 694]---> Adder-cost: 334   maxlim: 113017   bits: 18/17
c ---[ 692]---> Adder-cost: 343   maxlim: 97529   bits: 18/17
c ---[ 690]---> Adder-cost: 334   maxlim: 113017   bits: 18/17
c ---[ 688]---> Adder-cost: 338   maxlim: 162041   bits: 18/18
c ---[ 686]---> Adder-cost: 338   maxlim: 161913   bits: 18/18
c ---[ 684]---> Adder-cost: 338   maxlim: 162169   bits: 18/18
c ---[ 682]---> Adder-cost: 338   maxlim: 162297   bits: 18/18
c ---[ 680]---> Adder-cost: 352   maxlim: 146297   bits: 19/18
c ---[ 678]---> Adder-cost: 352   maxlim: 146297   bits: 19/18
c ---[ 676]---> Adder-cost: 352   maxlim: 146297   bits: 19/18
c ---[ 674]---> Adder-cost: 314   maxlim: 80249   bits: 17/17
c ---[ 672]---> Adder-cost: 314   maxlim: 80761   bits: 17/17
c ---[ 670]---> Adder-cost: 314   maxlim: 80505   bits: 17/17
c ---[ 668]---> Adder-cost: 314   maxlim: 81145   bits: 17/17
c ---[ 666]---> Adder-cost: 328   maxlim: 73081   bits: 18/17
c ---[ 664]---> Adder-cost: 328   maxlim: 72313   bits: 18/17
c ---[ 662]---> Adder-cost: 328   maxlim: 72697   bits: 18/17
c ---[ 660]---> Adder-cost: 314   maxlim: 81017   bits: 17/17
c ---[ 658]---> Adder-cost: 314   maxlim: 80889   bits: 17/17
c ---[ 656]---> Adder-cost: 314   maxlim: 79993   bits: 17/17
c ---[ 654]---> Adder-cost: 314   maxlim: 81017   bits: 17/17
c ---[ 652]---> Adder-cost: 328   maxlim: 72953   bits: 18/17
c ---[ 650]---> Adder-cost: 328   maxlim: 72313   bits: 18/17
c ---[ 648]---> Adder-cost: 328   maxlim: 72569   bits: 18/17
c ---[ 646]---> Adder-cost: 334   maxlim: 113657   bits: 18/17
c ---[ 644]---> Adder-cost: 326   maxlim: 121337   bits: 18/17
c ---[ 642]---> Adder-cost: 326   maxlim: 121337   bits: 18/17
c ---[ 640]---> Adder-cost: 334   maxlim: 113529   bits: 18/17
c ---[ 638]---> Adder-cost: 343   maxlim: 97145   bits: 18/17
c ---[ 636]---> Adder-cost: 334   maxlim: 112889   bits: 18/17
c ---[ 634]---> Adder-cost: 334   maxlim: 113273   bits: 18/17
c ---[ 632]---> Adder-cost: 328   maxlim: 97657   bits: 18/17
c ---[ 630]---> Adder-cost: 322   maxlim: 105081   bits: 18/17
c ---[ 628]---> Adder-cost: 322   maxlim: 105081   bits: 18/17
c ---[ 626]---> Adder-cost: 322   maxlim: 105593   bits: 18/17
c ---[ 624]---> Adder-cost: 322   maxlim: 105337   bits: 18/17
c ---[ 622]---> Adder-cost: 328   maxlim: 96377   bits: 18/17
c ---[ 620]---> Adder-cost: 328   maxlim: 96761   bits: 18/17
c ---[ 618]---> Adder-cost: 320   maxlim: 97529   bits: 18/17
c ---[ 616]---> Adder-cost: 320   maxlim: 97145   bits: 18/17
c ---[ 614]---> Adder-cost: 320   maxlim: 97401   bits: 18/17
c ---[ 612]---> Adder-cost: 320   maxlim: 96505   bits: 18/17
c ---[ 610]---> Adder-cost: 320   maxlim: 97017   bits: 18/17
c ---[ 608]---> Adder-cost: 328   maxlim: 88569   bits: 18/17
c ---[ 606]---> Adder-cost: 328   maxlim: 89209   bits: 18/17
c ---[ 604]---> Adder-cost: 314   maxlim: 80505   bits: 17/17
c ---[ 602]---> Adder-cost: 314   maxlim: 81017   bits: 17/17
c ---[ 600]---> Adder-cost: 314   maxlim: 80889   bits: 17/17
c ---[ 598]---> Adder-cost: 314   maxlim: 81145   bits: 17/17
c ---[ 596]---> Adder-cost: 314   maxlim: 80633   bits: 17/17
c ---[ 594]---> Adder-cost: 328   maxlim: 73081   bits: 18/17
c ---[ 592]---> Adder-cost: 328   maxlim: 71929   bits: 18/17
c ---[ 591]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 590]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 589]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 588]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 587]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 586]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 585]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 584]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 583]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 582]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 581]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 580]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 579]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 578]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 577]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 576]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 575]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 574]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 573]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 572]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 571]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 570]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 569]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 568]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 567]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 566]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 565]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 564]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 563]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 562]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 561]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 560]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 559]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 558]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 557]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 556]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 555]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 554]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 553]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 552]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 551]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 550]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 549]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 548]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 547]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 546]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 545]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 544]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 543]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 542]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 541]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 540]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 539]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 538]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 537]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 536]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 534]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 532]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 530]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 528]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 526]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 524]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 522]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 520]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 518]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 516]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 514]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 512]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 510]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 508]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 506]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 504]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 502]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 500]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 498]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 496]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 494]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 492]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 490]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 488]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 486]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 484]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 482]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 480]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 478]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 476]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 474]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 472]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 470]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 468]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 466]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 464]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 462]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 460]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 458]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 456]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 454]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 452]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 450]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 448]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 446]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 444]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 442]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 440]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 438]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 436]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 434]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 432]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 430]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 428]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 426]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 424]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 422]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 420]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 418]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 416]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 414]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 412]---> Adder-cost: 28   maxlim: 894   bits: 11/10
c ---[ 410]---> Adder-cost: 28   maxlim: 894   bits: 11/10
c ---[ 408]---> Adder-cost: 28   maxlim: 894   bits: 11/10
c ---[ 406]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 402]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 400]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 398]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 396]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 394]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 392]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 391]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 390]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 389]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 388]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 387]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 386]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 385]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 384]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 383]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 382]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 381]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 380]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 379]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 378]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 377]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 376]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 375]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 374]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 373]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 372]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 371]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 370]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 369]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 368]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 367]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 366]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 365]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 364]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 363]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 362]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 361]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 360]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 359]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 358]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 357]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 356]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 355]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 354]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 353]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 352]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 351]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 350]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 349]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 348]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 347]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 346]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 345]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 344]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 343]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 342]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 341]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 340]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 339]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 338]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 337]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 336]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 335]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 334]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 333]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 332]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 331]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 330]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 329]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 328]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 327]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 326]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 325]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 324]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 323]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 322]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 321]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 320]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 319]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 318]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 317]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 316]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 315]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 314]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 313]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 312]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 311]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 310]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 309]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 308]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 307]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 306]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 305]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 304]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 303]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 302]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 301]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 300]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 299]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 298]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 297]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 296]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 295]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 294]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 293]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 292]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 291]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 290]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 289]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 288]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 287]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 286]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 285]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 284]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 283]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 282]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 281]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 280]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 279]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 278]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 277]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 276]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 275]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 274]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 273]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 272]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 271]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 270]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 269]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 268]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 267]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 266]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 265]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 264]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 263]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 262]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 261]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 260]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 259]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 258]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 257]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 256]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 255]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 254]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 253]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 252]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 251]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 250]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 249]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 248]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 247]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 246]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 245]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 244]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 243]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 242]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 241]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 240]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 239]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 238]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 237]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 236]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 235]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 234]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 233]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 232]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 231]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 230]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 229]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 228]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 227]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 226]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 225]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 224]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 223]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 222]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 221]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 220]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 219]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 218]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 217]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 216]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 215]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 214]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 213]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 212]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 211]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 210]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 209]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 208]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 207]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 206]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 205]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 204]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 203]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 202]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 201]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 200]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 199]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 198]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 197]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 196]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 195]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 194]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 193]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 192]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 191]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 190]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 189]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 188]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 187]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 186]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 185]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 184]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 183]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 182]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 181]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 180]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 179]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 178]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 177]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 176]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 175]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 174]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 173]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 172]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 171]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 170]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 169]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 168]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 167]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 166]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 165]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 164]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 163]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 162]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 161]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 160]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 159]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 158]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 157]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 156]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 155]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 154]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 153]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 152]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 151]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 150]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 149]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 148]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 147]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 146]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 145]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 144]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 143]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 142]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 141]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 140]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 139]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 138]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 137]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 136]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 135]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 134]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 133]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 132]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 131]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 130]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 129]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 128]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 127]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 126]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 125]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 124]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 123]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 122]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 121]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 120]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 119]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 118]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 117]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 116]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 115]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 114]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 113]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 112]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 111]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 110]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 109]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 108]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 107]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 106]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 105]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 104]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 103]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 102]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 101]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 100]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  99]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  98]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  97]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  96]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  95]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  94]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  93]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  92]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  91]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  90]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  89]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  88]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  87]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  86]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  85]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  84]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  83]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  82]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  81]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  80]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  79]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  78]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  77]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  76]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  75]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  74]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  73]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  72]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  71]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  70]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  69]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  68]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  67]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  66]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  65]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  64]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  63]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  62]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  61]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  60]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  59]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  58]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  57]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  56]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  55]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  54]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  53]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  52]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  51]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  50]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  49]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  48]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  47]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  46]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  45]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  44]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  43]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  42]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  41]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  40]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  39]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  38]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  37]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  36]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  35]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  34]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  33]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  32]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  31]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  30]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  29]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  28]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  27]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  26]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  25]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  24]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  23]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  22]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  21]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  20]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  19]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  18]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  17]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  16]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  15]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  14]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  13]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  12]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  11]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  10]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   9]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   8]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   7]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[   6]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[   5]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   4]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   3]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   2]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   1]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   0]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  295011  1078652 |   98337       0        0     nan |  0.000 % |
c |       101 |  295011  1078652 |  108170     101      643     6.4 | 21.292 % |
c |       253 |  295011  1078652 |  118987     252     2092     8.3 | 21.296 % |
c |       478 |  294996  1078605 |  130886     477     3694     7.7 | 21.296 % |
c |       815 |  294996  1078605 |  143975     814     6047     7.4 | 21.296 % |
c |      1321 |  294996  1078605 |  158372    1320     9950     7.5 | 21.296 % |
c |      2080 |  294988  1078579 |  174209    2078    15641     7.5 | 21.298 % |
c |      3219 |  294973  1078532 |  191630    3216    24246     7.5 | 21.303 % |
c |      4927 |  294973  1078532 |  210794    4924    56406    11.5 | 21.303 % |
c |      7492 |  294949  1078458 |  231873    7486   107672    14.4 | 21.309 % |
c |     11337 |  294941  1078432 |  255060   11330   203382    18.0 | 21.311 % |
c |     17103 |  294885  1078244 |  280566   17088   314357    18.4 | 21.320 % |
c |     25754 |  294853  1078144 |  308623   25735   526996    20.5 | 21.329 % |
c |     38730 |  294805  1077992 |  339485   38705   814801    21.1 | 21.340 % |
c |     58191 |  294714  1077699 |  373434   58148  1199146    20.6 | 21.364 % |
c |     87385 |  294586  1077261 |  410778   87265  1919736    22.0 | 21.386 % |
c |    131175 |  294522  1077047 |  451855  131039  3566645    27.2 | 21.397 % |
c |    196861 |  294410  1076675 |  497041  196674  5202639    26.5 | 21.418 % |
c |    295387 |  294288  1076269 |  546745  294539  9555996    32.4 | 21.441 % |
c |    443178 |  294240  1076105 |  601420  442160 24812686    56.1 | 21.450 % |
c |    664862 |  293900  1074949 |  661562   76960  1798641    23.4 | 21.503 % |
#### 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.88 0.94 0.94 2/56 26921
Raw data (stat): 26921 (runsolver) R 26920 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 429363033 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.90 0.94 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 7790 0 0 0 978 20 0 0 25 0 1 0 429363033 33468416 7398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8171 7398 603 41 0 8130 0
vsize: 32684
[startup+20.001 s]
Raw data (loadavg): 0.92 0.94 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 8235 0 0 0 1977 22 0 0 25 0 1 0 429363033 35233792 7843 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8602 7843 603 41 0 8561 0
vsize: 34408
[startup+30.0018 s]
Raw data (loadavg): 0.93 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 8546 0 0 0 2975 23 0 0 25 0 1 0 429363033 36704256 8154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8961 8154 603 41 0 8920 0
vsize: 35844
[startup+40.0016 s]
Raw data (loadavg): 0.94 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 8838 0 0 0 3974 25 0 0 25 0 1 0 429363033 37781504 8446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8446 603 41 0 9183 0
vsize: 36896
[startup+50.0024 s]
Raw data (loadavg): 0.95 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 9217 0 0 0 4973 26 0 0 25 0 1 0 429363033 39268352 8825 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9587 8825 603 41 0 9546 0
vsize: 38348
[startup+60.0026 s]
Raw data (loadavg): 0.95 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 9724 0 0 0 5971 28 0 0 25 0 1 0 429363033 41553920 9332 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10145 9332 603 41 0 10104 0
vsize: 40580
[startup+70.0029 s]
Raw data (loadavg): 0.96 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 10019 0 0 0 6970 29 0 0 25 0 1 0 429363033 42770432 9627 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10442 9627 603 41 0 10401 0
vsize: 41768
[startup+80.0037 s]
Raw data (loadavg): 0.97 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 10315 0 0 0 7970 30 0 0 25 0 1 0 429363033 43978752 9923 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10737 9923 603 41 0 10696 0
vsize: 42948
[startup+90.0035 s]
Raw data (loadavg): 0.97 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 10620 0 0 0 8969 31 0 0 25 0 1 0 429363033 45195264 10228 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11034 10228 603 41 0 10993 0
vsize: 44136
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 10967 0 0 0 9968 32 0 0 25 0 1 0 429363033 46542848 10575 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11363 10575 603 41 0 11322 0
vsize: 45452
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 11407 0 0 0 10967 33 0 0 25 0 1 0 429363033 48300032 11015 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11792 11015 603 41 0 11751 0
vsize: 47168
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 12101 0 0 0 11964 36 0 0 25 0 1 0 429363033 51134464 11709 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12484 11709 603 41 0 12443 0
vsize: 49936
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 12580 0 0 0 12963 37 0 0 25 0 1 0 429363033 53551104 12188 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13074 12188 603 41 0 13033 0
vsize: 52296
[startup+140.004 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 12872 0 0 0 13962 38 0 0 25 0 1 0 429363033 54763520 12480 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13370 12480 603 41 0 13329 0
vsize: 53480
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 13231 0 0 0 14960 41 0 0 25 0 1 0 429363033 56115200 12839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13700 12839 603 41 0 13659 0
vsize: 54800
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 13507 0 0 0 15959 42 0 0 25 0 1 0 429363033 57192448 13115 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13963 13115 603 41 0 13922 0
vsize: 55852
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 13820 0 0 0 16958 43 0 0 25 0 1 0 429363033 58535936 13428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14291 13428 603 41 0 14250 0
vsize: 57164
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 14122 0 0 0 17957 44 0 0 25 0 1 0 429363033 59744256 13730 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14586 13730 603 41 0 14545 0
vsize: 58344
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 14359 0 0 0 18957 45 0 0 25 0 1 0 429363033 60690432 13967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14817 13967 603 41 0 14776 0
vsize: 59268
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26921
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 14516 0 0 0 19956 45 0 0 25 0 1 0 429363033 61222912 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14947 14124 603 41 0 14906 0
vsize: 59788
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 14776 0 0 0 20956 46 0 0 25 0 1 0 429363033 62300160 14384 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15210 14384 603 41 0 15169 0
vsize: 60840
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 14973 0 0 0 21955 47 0 0 25 0 1 0 429363033 63111168 14581 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15408 14581 603 41 0 15367 0
vsize: 61632
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 15375 0 0 0 22954 48 0 0 25 0 1 0 429363033 64729088 14983 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15803 14983 603 41 0 15762 0
vsize: 63212
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 15552 0 0 0 23953 49 0 0 25 0 1 0 429363033 65400832 15160 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15967 15160 603 41 0 15926 0
vsize: 63868
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 15800 0 0 0 24952 50 0 0 25 0 1 0 429363033 66342912 15408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16197 15408 603 41 0 16156 0
vsize: 64788
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 16194 0 0 0 25951 51 0 0 25 0 1 0 429363033 67952640 15802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16590 15802 603 41 0 16549 0
vsize: 66360
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 16400 0 0 0 26950 53 0 0 25 0 1 0 429363033 68759552 16008 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16787 16008 603 41 0 16746 0
vsize: 67148
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 16596 0 0 0 27949 54 0 0 25 0 1 0 429363033 69554176 16204 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16981 16204 603 41 0 16940 0
vsize: 67924
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 17036 0 0 0 28948 55 0 0 25 0 1 0 429363033 71303168 16644 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17408 16644 603 41 0 17367 0
vsize: 69632
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 17285 0 0 0 29948 55 0 0 25 0 1 0 429363033 72376320 16893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17670 16893 603 41 0 17629 0
vsize: 70680
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 17643 0 0 0 30947 56 0 0 25 0 1 0 429363033 73854976 17251 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18031 17251 603 41 0 17990 0
vsize: 72124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 17918 0 0 0 31946 57 0 0 25 0 1 0 429363033 75980800 17526 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18550 17526 603 41 0 18509 0
vsize: 74200
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 18308 0 0 0 32945 58 0 0 25 0 1 0 429363033 77463552 17916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18912 17916 603 41 0 18871 0
vsize: 75648
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 18883 0 0 0 33944 60 0 0 25 0 1 0 429363033 79880192 18491 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19502 18491 603 41 0 19461 0
vsize: 78008
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 19679 0 0 0 34942 62 0 0 25 0 1 0 429363033 83095552 19287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20287 19287 603 41 0 20246 0
vsize: 81148
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 20099 0 0 0 35940 64 0 0 25 0 1 0 429363033 84828160 19707 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20710 19707 603 41 0 20669 0
vsize: 82840
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 20349 0 0 0 36940 64 0 0 25 0 1 0 429363033 85770240 19957 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20940 19957 603 41 0 20899 0
vsize: 83760
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 20893 0 0 0 37938 66 0 0 25 0 1 0 429363033 88047616 20501 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21496 20501 603 41 0 21455 0
vsize: 85984
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 21445 0 0 0 38936 68 0 0 25 0 1 0 429363033 90181632 21053 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22017 21053 603 41 0 21976 0
vsize: 88068
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 21952 0 0 0 39934 70 0 0 25 0 1 0 429363033 92327936 21560 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22541 21560 603 41 0 22500 0
vsize: 90164
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 22450 0 0 0 40933 71 0 0 25 0 1 0 429363033 94330880 22058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23030 22058 603 41 0 22989 0
vsize: 92120
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 22902 0 0 0 41932 73 0 0 25 0 1 0 429363033 96206848 22510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23488 22510 603 41 0 23447 0
vsize: 93952
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 23314 0 0 0 42931 74 0 0 25 0 1 0 429363033 97808384 22922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23879 22922 603 41 0 23838 0
vsize: 95516
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 23723 0 0 0 43929 75 0 0 25 0 1 0 429363033 99545088 23331 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24303 23331 603 41 0 24262 0
vsize: 97212
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 24144 0 0 0 44928 77 0 0 25 0 1 0 429363033 101281792 23752 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24727 23752 603 41 0 24686 0
vsize: 98908
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 24585 0 0 0 45927 78 0 0 25 0 1 0 429363033 103018496 24193 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25151 24193 603 41 0 25110 0
vsize: 100604
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 25046 0 0 0 46926 80 0 0 25 0 1 0 429363033 104886272 24654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25607 24654 603 41 0 25566 0
vsize: 102428
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 25473 0 0 0 47924 81 0 0 25 0 1 0 429363033 106631168 25081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26033 25081 603 41 0 25992 0
vsize: 104132
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 25851 0 0 0 48923 83 0 0 25 0 1 0 429363033 108244992 25459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26427 25459 603 41 0 26386 0
vsize: 105708
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26923
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 26192 0 0 0 49923 84 0 0 25 0 1 0 429363033 109649920 25800 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26770 25800 603 41 0 26729 0
vsize: 107080
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 26500 0 0 0 50922 86 0 0 25 0 1 0 429363033 110862336 26108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27066 26108 603 41 0 27025 0
vsize: 108264
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 26729 0 0 0 51921 86 0 0 25 0 1 0 429363033 111812608 26337 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27298 26337 603 41 0 27257 0
vsize: 109192
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 27045 0 0 0 52921 87 0 0 25 0 1 0 429363033 113156096 26653 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27626 26653 603 41 0 27585 0
vsize: 110504
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 27200 0 0 0 53921 87 0 0 25 0 1 0 429363033 113696768 26808 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27758 26808 603 41 0 27717 0
vsize: 111032
[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 27437 0 0 0 54921 88 0 0 25 0 1 0 429363033 114651136 27045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27991 27045 603 41 0 27950 0
vsize: 111964
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 27748 0 0 0 55920 88 0 0 25 0 1 0 429363033 115994624 27356 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28319 27356 603 41 0 28278 0
vsize: 113276
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 28416 0 0 0 56918 91 0 0 25 0 1 0 429363033 118669312 28024 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 28024 603 41 0 28931 0
vsize: 115888
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 29065 0 0 0 57916 92 0 0 25 0 1 0 429363033 121335808 28673 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29623 28673 603 41 0 29582 0
vsize: 118492
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 29701 0 0 0 58915 94 0 0 25 0 1 0 429363033 123871232 29309 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30242 29309 603 41 0 30201 0
vsize: 120968
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 30358 0 0 0 59913 95 0 0 25 0 1 0 429363033 126545920 29966 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30895 29966 603 41 0 30854 0
vsize: 123580
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 30976 0 0 0 60912 97 0 0 25 0 1 0 429363033 129097728 30584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31518 30584 603 41 0 31477 0
vsize: 126072
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 31331 0 0 0 61911 98 0 0 25 0 1 0 429363033 130441216 30939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31846 30939 603 41 0 31805 0
vsize: 127384
[startup+630.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 31817 0 0 0 62910 99 0 0 25 0 1 0 429363033 132448256 31425 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32336 31425 603 41 0 32295 0
vsize: 129344
[startup+640.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 32379 0 0 0 63908 101 0 0 25 0 1 0 429363033 134725632 31987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32892 31987 603 41 0 32851 0
vsize: 131568
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 33004 0 0 0 64907 103 0 0 25 0 1 0 429363033 137261056 32612 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33511 32612 603 41 0 33470 0
vsize: 134044
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 33594 0 0 0 65906 104 0 0 25 0 1 0 429363033 139673600 33202 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34100 33202 603 41 0 34059 0
vsize: 136400
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 33972 0 0 0 66905 105 0 0 25 0 1 0 429363033 141287424 33580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34494 33580 603 41 0 34453 0
vsize: 137976
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 34277 0 0 0 67904 106 0 0 25 0 1 0 429363033 142495744 33885 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34789 33885 603 41 0 34748 0
vsize: 139156
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 34518 0 0 0 68904 107 0 0 25 0 1 0 429363033 143437824 34126 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35019 34126 603 41 0 34978 0
vsize: 140076
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 34819 0 0 0 69903 107 0 0 25 0 1 0 429363033 144650240 34427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35315 34427 603 41 0 35274 0
vsize: 141260
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 35177 0 0 0 70903 108 0 0 25 0 1 0 429363033 146116608 34785 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35673 34785 603 41 0 35632 0
vsize: 142692
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 35469 0 0 0 71901 110 0 0 25 0 1 0 429363033 147341312 35077 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35972 35077 603 41 0 35931 0
vsize: 143888
[startup+730.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 35794 0 0 0 72900 111 0 0 25 0 1 0 429363033 148672512 35402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36297 35402 603 41 0 36256 0
vsize: 145188
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 36141 0 0 0 73899 112 0 0 25 0 1 0 429363033 150155264 35749 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36659 35749 603 41 0 36618 0
vsize: 146636
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 36435 0 0 0 74899 112 0 0 25 0 1 0 429363033 151252992 36043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36927 36043 603 41 0 36886 0
vsize: 147708
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 36819 0 0 0 75898 113 0 0 25 0 1 0 429363033 152870912 36427 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37322 36427 603 41 0 37281 0
vsize: 149288
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 37160 0 0 0 76897 114 0 0 25 0 1 0 429363033 154234880 36768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37655 36768 603 41 0 37614 0
vsize: 150620
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 37322 0 0 0 77897 115 0 0 25 0 1 0 429363033 154927104 36930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37824 36930 603 41 0 37783 0
vsize: 151296
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 37503 0 0 0 78897 115 0 0 25 0 1 0 429363033 155598848 37111 4294967295 134512640 134672761 3221224544 3221223600 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37988 37111 603 41 0 37947 0
vsize: 151952
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26925
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 37704 0 0 0 79896 116 0 0 25 0 1 0 429363033 156540928 37312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38218 37312 603 41 0 38177 0
vsize: 152872
[startup+810.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 37839 0 0 0 80895 117 0 0 25 0 1 0 429363033 157097984 37447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38354 37447 603 41 0 38313 0
vsize: 153416
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 37954 0 0 0 81895 117 0 0 25 0 1 0 429363033 157503488 37562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38453 37562 603 41 0 38412 0
vsize: 153812
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 38184 0 0 0 82894 118 0 0 25 0 1 0 429363033 158445568 37792 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38683 37792 603 41 0 38642 0
vsize: 154732
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 38243 0 0 0 83894 118 0 0 25 0 1 0 429363033 158715904 37851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38749 37851 603 41 0 38708 0
vsize: 154996
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 38386 0 0 0 84894 119 0 0 25 0 1 0 429363033 159252480 37994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38880 37994 603 41 0 38839 0
vsize: 155520
[startup+860.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 38550 0 0 0 85894 119 0 0 25 0 1 0 429363033 159920128 38158 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39043 38158 603 41 0 39002 0
vsize: 156172
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 39545 0 0 0 86891 122 0 0 25 0 1 0 429363033 163946496 39153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40026 39153 603 41 0 39985 0
vsize: 160104
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 40245 0 0 0 87889 124 0 0 25 0 1 0 429363033 166785024 39853 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40719 39853 603 41 0 40678 0
vsize: 162876
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 40844 0 0 0 88887 126 0 0 25 0 1 0 429363033 169340928 40452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41343 40452 603 41 0 41302 0
vsize: 165372
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 41175 0 0 0 89886 127 0 0 25 0 1 0 429363033 170680320 40783 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41670 40783 603 41 0 41629 0
vsize: 166680
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 41341 0 0 0 90886 127 0 0 25 0 1 0 429363033 171360256 40949 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41836 40949 603 41 0 41795 0
vsize: 167344
[startup+920.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 41604 0 0 0 91886 128 0 0 25 0 1 0 429363033 172437504 41212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42099 41212 603 41 0 42058 0
vsize: 168396
[startup+930.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 41761 0 0 0 92886 128 0 0 25 0 1 0 429363033 172969984 41369 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42229 41369 603 41 0 42188 0
vsize: 168916
[startup+940.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 41864 0 0 0 93885 129 0 0 25 0 1 0 429363033 173371392 41472 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42327 41472 603 41 0 42286 0
vsize: 169308
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 41931 0 0 0 94885 129 0 0 25 0 1 0 429363033 175738880 41539 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42905 41539 603 41 0 42864 0
vsize: 171620
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 42291 0 0 0 95885 130 0 0 25 0 1 0 429363033 177221632 41899 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43267 41899 603 41 0 43226 0
vsize: 173068
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 42422 0 0 0 96884 130 0 0 25 0 1 0 429363033 177758208 42030 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43398 42030 603 41 0 43357 0
vsize: 173592
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 42614 0 0 0 97884 131 0 0 25 0 1 0 429363033 178565120 42222 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43595 42222 603 41 0 43554 0
vsize: 174380
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 42915 0 0 0 98883 132 0 0 25 0 1 0 429363033 179642368 42523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43858 42523 603 41 0 43817 0
vsize: 175432
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 43282 0 0 0 99882 133 0 0 25 0 1 0 429363033 181145600 42890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44225 42890 603 41 0 44184 0
vsize: 176900
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 43424 0 0 0 100882 134 0 0 25 0 1 0 429363033 181682176 43032 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44356 43032 603 41 0 44315 0
vsize: 177424
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 43612 0 0 0 101881 134 0 0 25 0 1 0 429363033 182489088 43220 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44553 43220 603 41 0 44512 0
vsize: 178212
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 43972 0 0 0 102880 136 0 0 25 0 1 0 429363033 183980032 43580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44917 43580 603 41 0 44876 0
vsize: 179668
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 44231 0 0 0 103879 137 0 0 25 0 1 0 429363033 184918016 43839 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45146 43839 603 41 0 45105 0
vsize: 180584
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 44505 0 0 0 104879 137 0 0 25 0 1 0 429363033 186138624 44113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45444 44113 603 41 0 45403 0
vsize: 181776
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 44678 0 0 0 105879 138 0 0 25 0 1 0 429363033 186810368 44286 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45608 44286 603 41 0 45567 0
vsize: 182432
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 44799 0 0 0 106878 138 0 0 25 0 1 0 429363033 187215872 44407 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45707 44407 603 41 0 45666 0
vsize: 182828
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45004 0 0 0 107878 139 0 0 25 0 1 0 429363033 188018688 44612 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45903 44612 603 41 0 45862 0
vsize: 183612
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45216 0 0 0 108878 139 0 0 25 0 1 0 429363033 188960768 44824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46133 44824 603 41 0 46092 0
vsize: 184532
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26927
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 109877 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26929
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 110877 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26982
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 111878 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26982
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 112878 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26982
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 113878 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26982
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 114878 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26982
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 115878 139 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26984
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 116877 141 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26984
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 117877 141 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26986
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 118877 141 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 26986
Raw data (stat): 26921 (minisat+) R 26920 12452 12451 0 -1 0 45328 0 0 0 119877 141 0 0 25 0 1 0 429363033 189358080 44936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46230 44936 603 41 0 46189 0
vsize: 184920
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.94 1/56 26986
Raw data (stat): 26921 (minisat+) Z 26920 12452 12451 0 -1 12 45330 0 0 0 119877 149 0 0 25 0 1 0 429363033 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.27
CPU user time (s): 1198.77
CPU system time (s): 1.49977
CPU usage (%): 100.013
Max. virtual memory (Kb): 184920
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####