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/MIPLIB/miplib3/normalized-mps-v2-13-7-danoint.opb
MD5SUM	bf9bbda6f586f0b888182a433f63f010
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	13107200
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	52829966
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.39179
Number of variables	9304
Total number of constraints	728
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	72
Number of constraints which are nor clauses,nor cardinality constraints	656
Minimum length of a constraint	1
Maximum length of a constraint	1000
Trace number 15190

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 03:18:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18275 boxname=wulflinc29 idbench=1406 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf9bbda6f586f0b888182a433f63f010  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-danoint.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-danoint.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-danoint.opb
IDLAUNCH: 18275
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        855548 kB
Buffers:         10896 kB
Cached:         140144 kB
SwapCached:        464 kB
Active:          44152 kB
Inactive:       109092 kB
HighTotal:      131008 kB
HighFree:         1204 kB
LowTotal:       903652 kB
LowFree:        854344 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20364 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:38:43 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 18275 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: ppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssss
c ---[ 833]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 832]---> Adder-cost: 26   maxlim: 7422   bits: 14/13
c ---[ 831]---> Adder-cost: 26   maxlim: 7422   bits: 14/13
c ---[ 828]---> Adder-cost: 26   maxlim: 7678   bits: 14/13
c ---[ 827]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 825]---> Adder-cost: 328   maxlim: 80633   bits: 18/17
c ---[ 823]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[ 821]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 819]---> Adder-cost: 322   maxlim: 88569   bits: 18/17
c ---[ 817]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 815]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 813]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 811]---> Adder-cost: 336   maxlim: 112889   bits: 18/17
c ---[ 809]---> Adder-cost: 336   maxlim: 112761   bits: 18/17
c ---[ 807]---> Adder-cost: 336   maxlim: 113017   bits: 18/17
c ---[ 805]---> Adder-cost: 336   maxlim: 113145   bits: 18/17
c ---[ 803]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 801]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 799]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 797]---> Adder-cost: 312   maxlim: 55673   bits: 17/16
c ---[ 795]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 793]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 791]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 789]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 787]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 785]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 783]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 781]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 779]---> Adder-cost: 312   maxlim: 55417   bits: 17/16
c ---[ 777]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 775]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 773]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 771]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 769]---> Adder-cost: 330   maxlim: 89081   bits: 18/17
c ---[ 767]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 765]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 763]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 761]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 759]---> Adder-cost: 322   maxlim: 96505   bits: 18/17
c ---[ 757]---> Adder-cost: 330   maxlim: 88697   bits: 18/17
c ---[ 755]---> Adder-cost: 323   maxlim: 64889   bits: 17/16
c ---[ 753]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 751]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 749]---> Adder-cost: 314   maxlim: 72825   bits: 17/17
c ---[ 747]---> Adder-cost: 314   maxlim: 72569   bits: 17/17
c ---[ 745]---> Adder-cost: 314   maxlim: 71801   bits: 17/17
c ---[ 743]---> Adder-cost: 314   maxlim: 72185   bits: 17/17
c ---[ 741]---> Adder-cost: 312   maxlim: 64761   bits: 17/16
c ---[ 739]---> Adder-cost: 312   maxlim: 64377   bits: 17/16
c ---[ 737]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 735]---> Adder-cost: 312   maxlim: 63737   bits: 17/16
c ---[ 733]---> Adder-cost: 312   maxlim: 64249   bits: 17/16
c ---[ 731]---> Adder-cost: 312   maxlim: 63993   bits: 17/16
c ---[ 729]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 727]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 725]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 723]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 721]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 719]---> Adder-cost: 312   maxlim: 56057   bits: 17/16
c ---[ 717]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 715]---> Adder-cost: 312   maxlim: 55545   bits: 17/16
c ---[ 714]---> Adder-cost: 187   maxlim: 1019782   bits: 21/20
c ---[ 713]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 712]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 711]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 710]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 709]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 708]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 707]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 706]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 705]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 704]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 703]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 702]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 701]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 700]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 699]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 698]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 697]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 696]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 695]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 694]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 693]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 692]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 691]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 690]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 689]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 688]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 687]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 686]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 685]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 684]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 683]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 682]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 681]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 680]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 679]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 678]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 677]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 676]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 675]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 674]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 673]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 672]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 671]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 670]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 669]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 668]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 667]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 666]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 665]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 664]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 663]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 662]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 661]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 660]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 659]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 657]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 655]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 653]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 651]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 649]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 647]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 645]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 643]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 641]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 639]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 637]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 635]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 633]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 631]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 629]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 627]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 625]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 623]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 621]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 619]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 617]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 615]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 613]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 611]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 609]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 607]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 605]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 603]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 601]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 599]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 597]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 595]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 593]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 591]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 589]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 587]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 585]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 583]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 581]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 579]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 577]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 575]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 573]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 571]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 569]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 567]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 565]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 563]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 561]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 559]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 557]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 555]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 553]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 551]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 549]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 547]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 545]---> Adder-cost: 1225   maxlim: 1048575   bits: 21/20
c ---[ 543]---> Adder-cost: 1243   maxlim: 1048575   bits: 21/20
c ---[ 541]---> Adder-cost: 1155   maxlim: 524287   bits: 20/19
c ---[ 539]---> Adder-cost: 1155   maxlim: 524287   bits: 20/19
c ---[ 537]---> Adder-cost: 1180   maxlim: 1048575   bits: 21/20
c ---[ 535]---> Adder-cost: 1145   maxlim: 524287   bits: 20/19
c ---[ 533]---> Adder-cost: 1137   maxlim: 524287   bits: 20/19
c ---[ 531]---> Adder-cost: 1129   maxlim: 524287   bits: 20/19
c ---[ 529]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 527]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 525]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 523]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 521]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 519]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 517]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 515]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 513]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 511]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 509]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 507]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 505]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 503]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 501]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 499]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 498]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 497]---> Adder-cost: 154   maxlim: 16382   bits: 15/14
c ---[ 496]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 495]---> Adder-cost: 141   maxlim: 16382   bits: 15/14
c ---[ 494]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 493]---> Adder-cost: 178   maxlim: 16382   bits: 15/14
c ---[ 492]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 491]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 490]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 489]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 488]---> Adder-cost: 148   maxlim: 16382   bits: 15/14
c ---[ 487]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 486]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 485]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 484]---> Adder-cost: 114   maxlim: 8190   bits: 14/13
c ---[ 483]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 482]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 481]---> Adder-cost: 138   maxlim: 8190   bits: 14/13
c ---[ 480]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 479]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 478]---> Adder-cost: 160   maxlim: 8190   bits: 14/13
c ---[ 477]---> Adder-cost: 114   maxlim: 8190   bits: 14/13
c ---[ 476]---> Adder-cost: 134   maxlim: 8190   bits: 14/13
c ---[ 475]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 474]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 473]---> Adder-cost: 164   maxlim: 8190   bits: 14/13
c ---[ 472]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 471]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 470]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 469]---> Adder-cost: 141   maxlim: 16382   bits: 15/14
c ---[ 468]---> Adder-cost: 167   maxlim: 16382   bits: 15/14
c ---[ 467]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 466]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 465]---> Adder-cost: 169   maxlim: 16382   bits: 15/14
c ---[ 464]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 463]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 462]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 461]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 460]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 459]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 458]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 457]---> Adder-cost: 167   maxlim: 16382   bits: 15/14
c ---[ 456]---> Adder-cost: 115   maxlim: 16382   bits: 15/14
c ---[ 455]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 454]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 453]---> Adder-cost: 143   maxlim: 16382   bits: 15/14
c ---[ 452]---> Adder-cost: 169   maxlim: 16382   bits: 15/14
c ---[ 451]---> Adder-cost: 167   maxlim: 16382   bits: 15/14
c ---[ 450]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 449]---> Adder-cost: 94   maxlim: 8190   bits: 14/13
c ---[ 448]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 447]---> Adder-cost: 158   maxlim: 8190   bits: 14/13
c ---[ 446]---> Adder-cost: 138   maxlim: 8190   bits: 14/13
c ---[ 445]---> Adder-cost: 164   maxlim: 8190   bits: 14/13
c ---[ 444]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 443]---> Adder-cost: 164   maxlim: 8190   bits: 14/13
c ---[ 441]---> Adder-cost: 208   maxlim: 17663   bits: 16/15
c ---[ 439]---> Adder-cost: 208   maxlim: 18559   bits: 16/15
c ---[ 437]---> Adder-cost: 208   maxlim: 24447   bits: 16/15
c ---[ 435]---> Adder-cost: 208   maxlim: 24447   bits: 16/15
c ---[ 433]---> Adder-cost: 208   maxlim: 17791   bits: 16/15
c ---[ 431]---> Adder-cost: 208   maxlim: 17151   bits: 16/15
c ---[ 429]---> Adder-cost: 208   maxlim: 24703   bits: 16/15
c ---[ 427]---> Adder-cost: 208   maxlim: 24191   bits: 16/15
c ---[ 410]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 409]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 408]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 407]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 406]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 405]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 404]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 403]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 402]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 401]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 400]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 399]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 398]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 397]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 396]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 395]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 394]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 393]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 392]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 391]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 390]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 389]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 388]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 387]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 386]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 385]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 384]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 383]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 382]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 381]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 380]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 379]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 378]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 377]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 376]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 375]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 374]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 373]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 372]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 371]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 370]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 369]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 368]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 367]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 366]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 365]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 364]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 363]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 362]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 361]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 360]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 359]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 358]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 357]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 356]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 355]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 354]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 353]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 352]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 351]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 350]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 349]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 348]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 347]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 346]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 345]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 344]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 343]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 342]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 341]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 340]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 339]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 338]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 337]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 336]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 335]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 334]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 333]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 332]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 331]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 330]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 329]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 328]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 327]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 326]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 325]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 324]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 323]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 322]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 321]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 320]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 319]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 318]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 317]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 316]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 315]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 314]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 313]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 312]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 311]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 310]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 309]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 308]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 307]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 306]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 305]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 304]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 303]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 302]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 301]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 300]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 299]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 298]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 297]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 296]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 295]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 294]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 293]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 292]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 291]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 290]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 289]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 288]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 287]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 286]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 285]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 284]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 283]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 282]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 281]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 280]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 279]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 278]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 277]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 276]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 275]---> Adder-cost: 8   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: 12   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: 6   maxlim: 8190   bits: 14/13
c ---[ 262]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 261]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 260]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 259]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 258]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 257]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 256]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 255]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 254]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 253]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 252]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 251]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 250]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 249]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 248]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 247]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 246]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 245]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 244]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 243]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 242]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 241]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 240]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 239]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 238]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 237]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 236]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 235]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 234]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 233]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 232]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 231]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 230]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 229]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 228]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 227]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 226]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 225]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 224]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 223]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 222]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 221]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 220]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 219]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 218]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 217]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 216]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 215]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 214]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 213]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 212]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 211]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 210]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 209]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 208]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 207]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 206]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 205]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 204]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 203]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 202]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 201]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 200]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 199]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 198]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 197]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 196]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 195]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 194]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 193]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 192]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 191]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 190]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 189]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 188]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 187]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 186]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 185]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 184]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 183]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 182]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 181]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 180]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 179]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 178]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 177]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 176]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 175]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 174]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 173]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 172]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 171]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 170]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 169]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 168]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 167]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 166]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 165]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 164]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 163]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 162]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 161]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 160]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 159]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 158]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 157]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 156]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 155]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 154]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 153]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 152]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 151]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 150]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 149]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 148]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 147]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 146]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 145]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 144]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 143]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 142]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 141]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
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: 16   maxlim: 16382   bits: 15/14
c ---[ 134]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 133]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 132]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 131]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 130]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 129]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
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: 10   maxlim: 8190   bits: 14/13
c ---[ 121]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 120]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 119]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 118]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 117]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 116]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 115]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 114]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 113]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 112]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 111]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 110]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 109]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 108]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 107]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 106]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 105]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 104]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 103]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 102]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 101]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 100]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  99]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  98]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
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: 12   maxlim: 8190   bits: 14/13
c ---[  90]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  89]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  88]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  87]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  86]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  85]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  84]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  83]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  82]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  81]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  80]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  79]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  78]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  77]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  76]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  75]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  74]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  73]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  72]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  71]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  70]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  69]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  68]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  67]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  66]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  65]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  64]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  63]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  62]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  61]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  60]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  59]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  58]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  57]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  56]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  55]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  54]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  53]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  52]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  51]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  50]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  49]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  48]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  47]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  46]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  45]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  44]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  43]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  42]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  41]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  40]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  39]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  38]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  37]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  36]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  35]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  34]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  33]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  32]---> Adder-cost: 6   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: 20   maxlim: 638   bits: 11/10
c ---[  17]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[  16]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  15]---> Adder-cost: 54   maxlim: 17662   bits: 16/15
c ---[  14]---> Adder-cost: 54   maxlim: 18558   bits: 16/15
c ---[  13]---> Adder-cost: 59   maxlim: 24446   bits: 16/15
c ---[  12]---> Adder-cost: 59   maxlim: 24446   bits: 16/15
c ---[  11]---> Adder-cost: 54   maxlim: 17790   bits: 16/15
c ---[  10]---> Adder-cost: 54   maxlim: 17150   bits: 16/15
c ---[   9]---> Adder-cost: 59   maxlim: 24702   bits: 16/15
c ---[   8]---> Adder-cost: 59   maxlim: 24190   bits: 16/15
c ---[   7]---> Adder-cost: 48   maxlim: 19711   bits: 16/15
c ---[   6]---> Adder-cost: 46   maxlim: 21887   bits: 16/15
c ---[   5]---> Adder-cost: 44   maxlim: 16767   bits: 16/15
c ---[   4]---> Adder-cost: 48   maxlim: 16895   bits: 16/15
c ---[   3]---> Adder-cost: 46   maxlim: 20223   bits: 16/15
c ---[   2]---> Adder-cost: 48   maxlim: 18559   bits: 16/15
c ---[   1]---> Adder-cost: 46   maxlim: 17407   bits: 16/15
c ---[   0]---> Adder-cost: 47   maxlim: 16255   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  420830  1528383 |  140276       0        0     nan |  0.000 % |
c |       100 |  420830  1528383 |  154303     100      362     3.6 | 17.471 % |
c |       250 |  420822  1528357 |  169733     249     1009     4.1 | 17.472 % |
c |       475 |  420806  1528305 |  186707     472     3162     6.7 | 17.475 % |
c |       813 |  420806  1528305 |  205378     810     6230     7.7 | 17.475 % |
c |      1319 |  420798  1528279 |  225915    1315    11910     9.1 | 17.476 % |
c |      2078 |  420790  1528253 |  248507    2073    21942    10.6 | 17.477 % |
c |      3217 |  420790  1528253 |  273358    3212    34193    10.6 | 17.477 % |
c |      4926 |  420782  1528227 |  300694    4920    51425    10.5 | 17.479 % |
c |      7488 |  420774  1528201 |  330763    7481   107859    14.4 | 17.480 % |
c |     11332 |  420733  1528072 |  363839   11321   203552    18.0 | 17.488 % |
c |     17099 |  420677  1527890 |  400223   17081   298346    17.5 | 17.497 % |
c |     25748 |  420645  1527786 |  440246   25726   599719    23.3 | 17.502 % |
c |     38724 |  420469  1527214 |  484270   38680  1329467    34.4 | 17.529 % |
c |     58185 |  420420  1527053 |  532697   58068  5370828    92.5 | 17.536 % |
c |     87377 |  420312  1526705 |  585967   87246  6942325    79.6 | 17.553 % |
c |    131167 |  420304  1526679 |  644564  131035 11700083    89.3 | 17.554 % |
c |    196851 |  420017  1525752 |  709020  196683 15905643    80.9 | 17.601 % |
c |    295377 |  419849  1525216 |  779922  295190 21384222    72.4 | 17.631 % |
c |    443166 |  419801  1525060 |  857915  442973 35189306    79.4 | 17.639 % |
#### 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.86 0.94 0.90 2/54 21721
Raw data (stat): 21721 (runsolver) R 21720 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541779081 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 9794 0 0 0 973 25 0 0 25 0 1 0 541779081 46411776 9401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11331 9401 603 41 0 11290 0
vsize: 45324
[startup+20.0005 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 10036 0 0 0 1971 26 0 0 25 0 1 0 541779081 47386624 9643 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11569 9643 603 41 0 11528 0
vsize: 46276
[startup+30.0026 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 10290 0 0 0 2971 27 0 0 25 0 1 0 541779081 48529408 9897 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11848 9897 603 41 0 11807 0
vsize: 47392
[startup+40.0046 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 10727 0 0 0 3969 28 0 0 25 0 1 0 541779081 50270208 10334 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12273 10335 603 41 0 12232 0
vsize: 49092
[startup+50.0079 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 11254 0 0 0 4968 29 0 0 25 0 1 0 541779081 52551680 10861 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12830 10861 603 41 0 12789 0
vsize: 51320
[startup+60.008 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 11674 0 0 0 5967 30 0 0 25 0 1 0 541779081 54169600 11281 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13225 11281 603 41 0 13184 0
vsize: 52900
[startup+70.0087 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 12587 0 0 0 6964 33 0 0 25 0 1 0 541779081 57892864 12194 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14134 12194 603 41 0 14093 0
vsize: 56536
[startup+80.0093 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 13434 0 0 0 7962 36 0 0 25 0 1 0 541779081 61366272 13041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14982 13041 603 41 0 14941 0
vsize: 59928
[startup+90.0091 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 14195 0 0 0 8960 38 0 0 25 0 1 0 541779081 64565248 13802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15763 13802 603 41 0 15722 0
vsize: 63052
[startup+100.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 14911 0 0 0 9958 40 0 0 25 0 1 0 541779081 67493888 14518 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16478 14518 603 41 0 16437 0
vsize: 65912
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 3/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 15565 0 0 0 10957 42 0 0 25 0 1 0 541779081 70156288 15172 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17128 15172 603 41 0 17087 0
vsize: 68512
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 16170 0 0 0 11956 43 0 0 25 0 1 0 541779081 72568832 15777 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17717 15777 603 41 0 17676 0
vsize: 70868
[startup+130.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 16506 0 0 0 12955 44 0 0 25 0 1 0 541779081 74178560 16113 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18110 16113 603 41 0 18069 0
vsize: 72440
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 16761 0 0 0 13954 45 0 0 25 0 1 0 541779081 75255808 16368 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18373 16368 603 41 0 18332 0
vsize: 73492
[startup+150.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 17300 0 0 0 14952 47 0 0 25 0 1 0 541779081 77414400 16907 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18900 16907 603 41 0 18859 0
vsize: 75600
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 17578 0 0 0 15951 48 0 0 25 0 1 0 541779081 78487552 17185 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 17185 603 41 0 19121 0
vsize: 76648
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 18600 0 0 0 16949 51 0 0 25 0 1 0 541779081 82665472 18207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20182 18207 603 41 0 20141 0
vsize: 80728
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 19265 0 0 0 17947 53 0 0 25 0 1 0 541779081 85360640 18872 4294967295 134512640 134672761 3221224544 3221223728 134559079 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20840 18872 603 41 0 20799 0
vsize: 83360
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 19762 0 0 0 18946 54 0 0 25 0 1 0 541779081 87379968 19369 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21333 19369 603 41 0 21292 0
vsize: 85332
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 20239 0 0 0 19944 56 0 0 25 0 1 0 541779081 89264128 19846 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21793 19846 603 41 0 21752 0
vsize: 87172
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 20795 0 0 0 20943 58 0 0 25 0 1 0 541779081 91549696 20402 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22351 20402 603 41 0 22310 0
vsize: 89404
[startup+220.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 21220 0 0 0 21942 59 0 0 25 0 1 0 541779081 93290496 20827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22776 20827 603 41 0 22735 0
vsize: 91104
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 21851 0 0 0 22940 60 0 0 25 0 1 0 541779081 95846400 21458 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23400 21458 603 41 0 23359 0
vsize: 93600
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 22218 0 0 0 23939 61 0 0 25 0 1 0 541779081 97329152 21825 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23762 21825 603 41 0 23721 0
vsize: 95048
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 22586 0 0 0 24939 63 0 0 25 0 1 0 541779081 98803712 22193 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24122 22193 603 41 0 24081 0
vsize: 96488
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 22814 0 0 0 25937 64 0 0 25 0 1 0 541779081 100274176 22421 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24481 22421 603 41 0 24440 0
vsize: 97924
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 22900 0 0 0 26937 64 0 0 25 0 1 0 541779081 100679680 22507 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24580 22507 603 41 0 24539 0
vsize: 98320
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 22937 0 0 0 27937 64 0 0 25 0 1 0 541779081 100810752 22544 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24612 22544 603 41 0 24571 0
vsize: 98448
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 23493 0 0 0 28935 66 0 0 25 0 1 0 541779081 102965248 23100 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25138 23100 603 41 0 25097 0
vsize: 100552
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 24321 0 0 0 29931 70 0 0 25 0 1 0 541779081 106311680 23928 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25955 23928 603 41 0 25914 0
vsize: 103820
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 25016 0 0 0 30930 71 0 0 25 0 1 0 541779081 109268992 24623 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26677 24623 603 41 0 26636 0
vsize: 106708
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 25277 0 0 0 31929 72 0 0 25 0 1 0 541779081 110215168 24884 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26908 24884 603 41 0 26867 0
vsize: 107632
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 25590 0 0 0 32929 73 0 0 25 0 1 0 541779081 111566848 25197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27238 25197 603 41 0 27197 0
vsize: 108952
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 26186 0 0 0 33928 74 0 0 25 0 1 0 541779081 113991680 25793 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27830 25793 603 41 0 27789 0
vsize: 111320
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 26859 0 0 0 34926 76 0 0 25 0 1 0 541779081 116674560 26466 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28485 26466 603 41 0 28444 0
vsize: 113940
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 27160 0 0 0 35925 77 0 0 25 0 1 0 541779081 117891072 26767 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28782 26767 603 41 0 28741 0
vsize: 115128
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 27331 0 0 0 36925 78 0 0 25 0 1 0 541779081 118566912 26938 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28947 26938 603 41 0 28906 0
vsize: 115788
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 27525 0 0 0 37925 78 0 0 25 0 1 0 541779081 119377920 27132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29145 27132 603 41 0 29104 0
vsize: 116580
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 27912 0 0 0 38923 79 0 0 25 0 1 0 541779081 120856576 27519 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29506 27519 603 41 0 29465 0
vsize: 118024
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 28242 0 0 0 39922 80 0 0 25 0 1 0 541779081 122208256 27849 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29836 27849 603 41 0 29795 0
vsize: 119344
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 29387 0 0 0 40919 83 0 0 25 0 1 0 541779081 126922752 28994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30987 28994 603 41 0 30946 0
vsize: 123948
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 30381 0 0 0 41917 86 0 0 25 0 1 0 541779081 130981888 29988 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31978 29988 603 41 0 31937 0
vsize: 127912
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 31088 0 0 0 42915 89 0 0 25 0 1 0 541779081 133857280 30695 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32680 30695 603 41 0 32639 0
vsize: 130720
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 31232 0 0 0 43914 89 0 0 25 0 1 0 541779081 134397952 30839 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32812 30839 603 41 0 32771 0
vsize: 131248
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 31446 0 0 0 44913 90 0 0 25 0 1 0 541779081 135208960 31053 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33010 31053 603 41 0 32969 0
vsize: 132040
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 31640 0 0 0 45913 91 0 0 25 0 1 0 541779081 136019968 31247 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33208 31247 603 41 0 33167 0
vsize: 132832
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 32170 0 0 0 46912 92 0 0 25 0 1 0 541779081 139227136 31777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33991 31777 603 41 0 33950 0
vsize: 135964
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 32355 0 0 0 47912 92 0 0 25 0 1 0 541779081 139902976 31962 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34156 31962 603 41 0 34115 0
vsize: 136624
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 32536 0 0 0 48911 93 0 0 25 0 1 0 541779081 140701696 32143 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34351 32143 603 41 0 34310 0
vsize: 137404
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 32704 0 0 0 49911 93 0 0 25 0 1 0 541779081 141377536 32311 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34516 32311 603 41 0 34475 0
vsize: 138064
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 32857 0 0 0 50911 93 0 0 25 0 1 0 541779081 141918208 32464 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34648 32464 603 41 0 34607 0
vsize: 138592
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 33272 0 0 0 51910 94 0 0 25 0 1 0 541779081 143667200 32879 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35075 32879 603 41 0 35034 0
vsize: 140300
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 33747 0 0 0 52909 96 0 0 25 0 1 0 541779081 145543168 33354 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35533 33354 603 41 0 35492 0
vsize: 142132
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34015 0 0 0 53908 97 0 0 25 0 1 0 541779081 146620416 33622 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35796 33622 603 41 0 35755 0
vsize: 143184
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34212 0 0 0 54908 97 0 0 25 0 1 0 541779081 147427328 33819 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35993 33819 603 41 0 35952 0
vsize: 143972
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34284 0 0 0 55907 98 0 0 25 0 1 0 541779081 147697664 33891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36059 33891 603 41 0 36018 0
vsize: 144236
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34355 0 0 0 56907 98 0 0 25 0 1 0 541779081 147968000 33962 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36125 33962 603 41 0 36084 0
vsize: 144500
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34422 0 0 0 57907 98 0 0 25 0 1 0 541779081 148238336 34029 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36191 34029 603 41 0 36150 0
vsize: 144764
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34511 0 0 0 58907 98 0 0 25 0 1 0 541779081 148639744 34118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36289 34118 603 41 0 36248 0
vsize: 145156
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34593 0 0 0 59907 99 0 0 25 0 1 0 541779081 148905984 34200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36354 34200 603 41 0 36313 0
vsize: 145416
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34674 0 0 0 60906 99 0 0 25 0 1 0 541779081 149307392 34281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36452 34281 603 41 0 36411 0
vsize: 145808
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34751 0 0 0 61906 100 0 0 25 0 1 0 541779081 149581824 34358 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36519 34358 603 41 0 36478 0
vsize: 146076
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 34829 0 0 0 62906 100 0 0 25 0 1 0 541779081 149983232 34436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36617 34436 603 41 0 36576 0
vsize: 146468
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 35111 0 0 0 63906 100 0 0 25 0 1 0 541779081 151060480 34718 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36880 34718 603 41 0 36839 0
vsize: 147520
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 35644 0 0 0 64905 102 0 0 25 0 1 0 541779081 153202688 35251 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37403 35251 603 41 0 37362 0
vsize: 149612
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 36077 0 0 0 65903 103 0 0 25 0 1 0 541779081 154955776 35684 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37831 35684 603 41 0 37790 0
vsize: 151324
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 37026 0 0 0 66902 105 0 0 25 0 1 0 541779081 158846976 36633 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38781 36633 603 41 0 38740 0
vsize: 155124
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 38076 0 0 0 67898 109 0 0 25 0 1 0 541779081 163131392 37683 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39827 37683 603 41 0 39786 0
vsize: 159308
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 38894 0 0 0 68896 111 0 0 25 0 1 0 541779081 166490112 38501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40647 38501 603 41 0 40606 0
vsize: 162588
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 39503 0 0 0 69895 113 0 0 25 0 1 0 541779081 168914944 39110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41239 39110 603 41 0 41198 0
vsize: 164956
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 40355 0 0 0 70892 116 0 0 25 0 1 0 541779081 172425216 39962 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42096 39962 603 41 0 42055 0
vsize: 168384
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 41046 0 0 0 71890 118 0 0 25 0 1 0 541779081 175120384 40653 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42754 40654 603 41 0 42713 0
vsize: 171016
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 41509 0 0 0 72888 120 0 0 25 0 1 0 541779081 177016832 41116 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43217 41116 603 41 0 43176 0
vsize: 172868
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 41999 0 0 0 73887 121 0 0 25 0 1 0 541779081 179032064 41606 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43709 41606 603 41 0 43668 0
vsize: 174836
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 42609 0 0 0 74885 123 0 0 25 0 1 0 541779081 181579776 42216 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44331 42216 603 41 0 44290 0
vsize: 177324
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 43203 0 0 0 75883 125 0 0 25 0 1 0 541779081 183992320 42810 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44920 42810 603 41 0 44879 0
vsize: 179680
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 43718 0 0 0 76883 126 0 0 25 0 1 0 541779081 186007552 43325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45412 43325 603 41 0 45371 0
vsize: 181648
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 44091 0 0 0 77882 127 0 0 25 0 1 0 541779081 187617280 43698 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45805 43698 603 41 0 45764 0
vsize: 183220
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 44598 0 0 0 78880 129 0 0 25 0 1 0 541779081 189628416 44205 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46296 44205 603 41 0 46255 0
vsize: 185184
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 45304 0 0 0 79878 132 0 0 25 0 1 0 541779081 192450560 44911 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46985 44911 603 41 0 46944 0
vsize: 187940
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 46107 0 0 0 80876 133 0 0 25 0 1 0 541779081 195665920 45714 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47770 45714 603 41 0 47729 0
vsize: 191080
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 46964 0 0 0 81875 135 0 0 25 0 1 0 541779081 199163904 46571 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48624 46571 603 41 0 48583 0
vsize: 194496
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 47393 0 0 0 82874 136 0 0 25 0 1 0 541779081 200908800 47000 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49050 47000 603 41 0 49009 0
vsize: 196200
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 47995 0 0 0 83873 137 0 0 25 0 1 0 541779081 203321344 47602 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49639 47602 603 41 0 49598 0
vsize: 198556
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 48611 0 0 0 84871 140 0 0 25 0 1 0 541779081 205848576 48218 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50256 48218 603 41 0 50215 0
vsize: 201024
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 48947 0 0 0 85870 141 0 0 25 0 1 0 541779081 207187968 48554 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50583 48554 603 41 0 50542 0
vsize: 202332
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 49294 0 0 0 86869 142 0 0 25 0 1 0 541779081 208662528 48901 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50943 48901 603 41 0 50902 0
vsize: 203772
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 49458 0 0 0 87869 142 0 0 25 0 1 0 541779081 209330176 49065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51106 49065 603 41 0 51065 0
vsize: 204424
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 49830 0 0 0 88866 144 0 0 25 0 1 0 541779081 210808832 49437 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51467 49437 603 41 0 51426 0
vsize: 205868
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 50385 0 0 0 89865 145 0 0 25 0 1 0 541779081 213086208 49992 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52023 49992 603 41 0 51982 0
vsize: 208092
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 51282 0 0 0 90863 147 0 0 25 0 1 0 541779081 216727552 50889 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52912 50889 603 41 0 52871 0
vsize: 211648
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 52130 0 0 0 91861 150 0 0 25 0 1 0 541779081 220229632 51737 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53767 51737 603 41 0 53726 0
vsize: 215068
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 52917 0 0 0 92859 152 0 0 25 0 1 0 541779081 223461376 52524 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54556 52524 603 41 0 54515 0
vsize: 218224
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 53659 0 0 0 93857 154 0 0 25 0 1 0 541779081 226426880 53266 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55280 53266 603 41 0 55239 0
vsize: 221120
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 54193 0 0 0 94856 156 0 0 25 0 1 0 541779081 228577280 53800 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55805 53800 603 41 0 55764 0
vsize: 223220
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 54333 0 0 0 95855 156 0 0 25 0 1 0 541779081 229113856 53940 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55936 53940 603 41 0 55895 0
vsize: 223744
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 54538 0 0 0 96855 157 0 0 25 0 1 0 541779081 230060032 54145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56167 54145 603 41 0 56126 0
vsize: 224668
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 54889 0 0 0 97854 158 0 0 25 0 1 0 541779081 231399424 54496 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56494 54496 603 41 0 56453 0
vsize: 225976
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 55186 0 0 0 98853 159 0 0 25 0 1 0 541779081 232595456 54793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56786 54793 603 41 0 56745 0
vsize: 227144
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 55415 0 0 0 99852 160 0 0 25 0 1 0 541779081 233537536 55022 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57016 55022 603 41 0 56975 0
vsize: 228064
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 55750 0 0 0 100851 161 0 0 25 0 1 0 541779081 234889216 55357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57346 55357 603 41 0 57305 0
vsize: 229384
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 56002 0 0 0 101851 162 0 0 25 0 1 0 541779081 235835392 55609 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57577 55609 603 41 0 57536 0
vsize: 230308
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 56429 0 0 0 102849 164 0 0 25 0 1 0 541779081 237584384 56036 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58004 56036 603 41 0 57963 0
vsize: 232016
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 56863 0 0 0 103848 165 0 0 25 0 1 0 541779081 239325184 56470 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58429 56470 603 41 0 58388 0
vsize: 233716
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 57310 0 0 0 104846 167 0 0 25 0 1 0 541779081 241213440 56917 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58890 56917 603 41 0 58849 0
vsize: 235560
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 57752 0 0 0 105845 168 0 0 25 0 1 0 541779081 242958336 57359 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59316 57359 603 41 0 59275 0
vsize: 237264
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 58160 0 0 0 106845 169 0 0 25 0 1 0 541779081 244695040 57767 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59740 57767 603 41 0 59699 0
vsize: 238960
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 58597 0 0 0 107844 170 0 0 25 0 1 0 541779081 248528896 58204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60676 58204 603 41 0 60635 0
vsize: 242704
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 59035 0 0 0 108843 171 0 0 25 0 1 0 541779081 250404864 58642 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61134 58642 603 41 0 61093 0
vsize: 244536
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 59439 0 0 0 109842 172 0 0 25 0 1 0 541779081 252026880 59046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61530 59046 603 41 0 61489 0
vsize: 246120
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 59841 0 0 0 110841 173 0 0 25 0 1 0 541779081 253644800 59448 4294967295 134512640 134672761 3221224544 3221223648 134560523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61925 59449 603 41 0 61884 0
vsize: 247700
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 60193 0 0 0 111841 174 0 0 25 0 1 0 541779081 255119360 59800 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62285 59800 603 41 0 62244 0
vsize: 249140
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 60655 0 0 0 112840 174 0 0 25 0 1 0 541779081 256999424 60262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62744 60262 603 41 0 62703 0
vsize: 250976
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 61018 0 0 0 113841 175 0 0 25 0 1 0 541779081 258338816 60625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63071 60625 603 41 0 63030 0
vsize: 252284
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 61629 0 0 0 114839 176 0 0 25 0 1 0 541779081 260886528 61236 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63693 61236 603 41 0 63652 0
vsize: 254772
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 62152 0 0 0 115838 178 0 0 25 0 1 0 541779081 263024640 61759 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64215 61759 603 41 0 64174 0
vsize: 256860
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 62642 0 0 0 116836 180 0 0 25 0 1 0 541779081 265035776 62249 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64706 62249 603 41 0 64665 0
vsize: 258824
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 63116 0 0 0 117835 181 0 0 25 0 1 0 541779081 266903552 62723 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65162 62723 603 41 0 65121 0
vsize: 260648
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 63559 0 0 0 118835 182 0 0 25 0 1 0 541779081 268812288 63166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65628 63166 603 41 0 65587 0
vsize: 262512
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21721
Raw data (stat): 21721 (minisat+) R 21720 27222 27221 0 -1 0 63956 0 0 0 119834 183 0 0 25 0 1 0 541779081 270434304 63563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66024 63563 603 41 0 65983 0
vsize: 264096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 21721
Raw data (stat): 21721 (minisat+) Z 21720 27222 27221 0 -1 12 63958 0 0 0 119834 195 0 0 24 0 1 0 541779081 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.18
CPU time (s): 1200.3
CPU user time (s): 1198.35
CPU system time (s): 1.9547
CPU usage (%): 100.01
Max. virtual memory (Kb): 264096
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####