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/miplib2003/normalized-mps-v2-13-7-danoint.opb
MD5SUM	32dd768e34cdc0e1cb04afadbe97060d
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.36179
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 15438

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        744840 kB
Buffers:         28176 kB
Cached:         238656 kB
SwapCached:          0 kB
Active:          34016 kB
Inactive:       235612 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        744588 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14476 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:45:12 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 17508 7 1200.34 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: (none)
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: 8   maxlim: 5   bits: 3/3
c ---[ 823]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 821]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 819]---> Adder-cost: 330   maxlim: 89081   bits: 18/17
c ---[ 817]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 815]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 813]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 811]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 809]---> Adder-cost: 322   maxlim: 96505   bits: 18/17
c ---[ 807]---> Adder-cost: 330   maxlim: 88697   bits: 18/17
c ---[ 805]---> Adder-cost: 323   maxlim: 64889   bits: 17/16
c ---[ 803]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 801]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 799]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 797]---> Adder-cost: 314   maxlim: 72825   bits: 17/17
c ---[ 795]---> Adder-cost: 314   maxlim: 72569   bits: 17/17
c ---[ 793]---> Adder-cost: 314   maxlim: 71801   bits: 17/17
c ---[ 791]---> Adder-cost: 314   maxlim: 72185   bits: 17/17
c ---[ 789]---> Adder-cost: 312   maxlim: 64761   bits: 17/16
c ---[ 787]---> Adder-cost: 312   maxlim: 64377   bits: 17/16
c ---[ 785]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 783]---> Adder-cost: 312   maxlim: 63737   bits: 17/16
c ---[ 781]---> Adder-cost: 312   maxlim: 64249   bits: 17/16
c ---[ 779]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 777]---> Adder-cost: 312   maxlim: 63993   bits: 17/16
c ---[ 775]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 773]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 771]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 769]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 767]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 765]---> Adder-cost: 312   maxlim: 56057   bits: 17/16
c ---[ 763]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 761]---> Adder-cost: 312   maxlim: 55545   bits: 17/16
c ---[ 760]---> Adder-cost: 187   maxlim: 1019782   bits: 21/20
c ---[ 758]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 757]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 756]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 755]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 754]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 753]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 752]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 751]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 750]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 749]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 748]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 746]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 745]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 744]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 743]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 742]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 741]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 740]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 739]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 738]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 737]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 736]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 734]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 733]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 732]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 731]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 730]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 729]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 728]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 727]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 726]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 725]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 724]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 722]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 721]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 720]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 719]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 718]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 717]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 716]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 715]---> Adder-cost: 183   maxlim: 1019782   bits: 21/20
c ---[ 714]---> Adder-cost: 183   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 ---[ 710]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
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 ---[ 698]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
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: 16   maxlim: 16382   bits: 15/14
c ---[ 691]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 690]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 689]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 688]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 686]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 685]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 684]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 683]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 682]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 681]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 680]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 679]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 678]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 677]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 676]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 674]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 672]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 671]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 670]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 669]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 668]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 667]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 666]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 665]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 664]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 663]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 662]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 660]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 659]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 658]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 657]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 656]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 655]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 654]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 653]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 652]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 651]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 650]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 648]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 647]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 646]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 645]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 644]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 643]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 642]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 641]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 640]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 639]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 638]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 636]---> Adder-cost: 194   maxlim: 32767   bits: 16/15
c ---[ 635]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 634]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 633]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 632]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 631]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 630]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 629]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 628]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 627]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 626]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 624]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 623]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 622]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 621]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 620]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 619]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 618]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 617]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 616]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 615]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 614]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 612]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 611]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 610]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 609]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 608]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 607]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 606]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 605]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 604]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 603]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 602]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 600]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 599]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 598]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 597]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 596]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 595]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 594]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 593]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 592]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 591]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 590]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 588]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 587]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 586]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 585]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 584]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 583]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 582]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 581]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 580]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 579]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 578]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 576]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 575]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 574]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 573]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 572]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 571]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 570]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 569]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 568]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 567]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 566]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 564]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 563]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 562]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 561]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 560]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 559]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 558]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 557]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 556]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 555]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 554]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 552]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 550]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 549]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 548]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 547]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 546]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 545]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 544]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 543]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 542]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 541]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 540]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 538]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 537]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 536]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 535]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 534]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 533]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 532]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 531]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 530]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 529]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 528]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 526]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 525]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 524]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 523]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 522]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 521]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 520]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 519]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 518]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 517]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 516]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 514]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 513]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 512]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 511]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 510]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 509]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 508]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 507]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 506]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 505]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 504]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 502]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 501]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 500]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 499]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 498]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 497]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 496]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 495]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 494]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 493]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 492]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 490]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 489]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 488]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 487]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 486]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 485]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 484]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 483]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 482]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 481]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 480]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 478]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 477]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 476]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 475]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 474]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 473]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 472]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 471]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 470]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 469]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 468]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 466]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 465]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 464]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 463]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 462]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 461]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 460]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 459]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 458]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 457]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 456]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 454]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 453]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 452]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 451]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 450]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 449]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 448]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 447]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 446]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 445]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 444]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 442]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 441]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 440]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 439]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 438]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 437]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 436]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 435]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 434]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 433]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 432]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 430]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 428]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 427]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 426]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 425]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 424]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 423]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 422]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 421]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 420]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 419]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 418]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 416]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 415]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 414]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 413]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 412]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 411]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 410]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 409]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 408]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 407]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 406]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 404]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 403]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 402]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 401]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 400]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 399]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 398]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 397]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 396]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 395]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 394]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 392]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 391]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 390]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 389]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 388]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 387]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 386]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 385]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 384]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 383]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 382]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 380]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 379]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 378]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 377]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 376]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 375]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 374]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 373]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 372]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 371]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 370]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 368]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 367]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 366]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 365]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 364]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 363]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 362]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 361]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 360]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 359]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 358]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 356]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[ 355]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 354]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 353]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 352]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 351]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 350]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 349]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 348]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 347]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 346]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 344]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 343]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 342]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 341]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 340]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 339]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 338]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 337]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 336]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 335]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 334]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 332]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 331]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 330]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 329]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 328]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 327]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 326]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 325]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 324]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 323]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 322]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 320]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 319]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 318]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 317]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 316]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 315]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 314]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 313]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 312]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 311]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 310]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 308]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 306]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 305]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 304]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 303]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 302]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 301]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 300]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 299]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 298]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 297]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 296]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 294]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 293]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 292]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 291]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 290]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 289]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 288]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 287]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 286]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 285]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 284]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 282]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 281]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 280]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 279]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 278]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 277]---> Adder-cost: 8   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: 14   maxlim: 16382   bits: 15/14
c ---[ 273]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 272]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 270]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 269]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 268]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 267]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 266]---> Adder-cost: 10   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: 10   maxlim: 8190   bits: 14/13
c ---[ 261]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 260]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 258]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 257]---> Adder-cost: 10   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: 16   maxlim: 16382   bits: 15/14
c ---[ 253]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 252]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 251]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 250]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 249]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 248]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 246]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 245]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 244]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 243]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 242]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 241]---> Adder-cost: 10   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: 16   maxlim: 16382   bits: 15/14
c ---[ 237]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 236]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 234]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 233]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 232]---> Adder-cost: 10   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: 16   maxlim: 16382   bits: 15/14
c ---[ 228]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 227]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 226]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 225]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 224]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 222]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 221]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 220]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 219]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 218]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 217]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 216]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 215]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 213]---> Adder-cost: 1336   maxlim: 1048575   bits: 21/20
c ---[ 211]---> Adder-cost: 1384   maxlim: 1048575   bits: 21/20
c ---[ 209]---> Adder-cost: 1286   maxlim: 524287   bits: 20/19
c ---[ 207]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 205]---> Adder-cost: 1193   maxlim: 524287   bits: 20/19
c ---[ 203]---> Adder-cost: 1180   maxlim: 1048575   bits: 21/20
c ---[ 201]---> Adder-cost: 1145   maxlim: 524287   bits: 20/19
c ---[ 199]---> Adder-cost: 1137   maxlim: 524287   bits: 20/19
c ---[ 197]---> Adder-cost: 1129   maxlim: 524287   bits: 20/19
c ---[ 190]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 185]---> Adder-cost: 208   maxlim: 17663   bits: 16/15
c ---[ 182]---> Adder-cost: 208   maxlim: 18559   bits: 16/15
c ---[ 179]---> Adder-cost: 208   maxlim: 24447   bits: 16/15
c ---[ 176]---> Adder-cost: 208   maxlim: 24447   bits: 16/15
c ---[ 174]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 172]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 169]---> Adder-cost: 208   maxlim: 17791   bits: 16/15
c ---[ 166]---> Adder-cost: 208   maxlim: 17151   bits: 16/15
c ---[ 163]---> Adder-cost: 208   maxlim: 24703   bits: 16/15
c ---[ 160]---> Adder-cost: 208   maxlim: 24191   bits: 16/15
c ---[ 158]---> Adder-cost: 150   maxlim: 16382   bits: 15/14
c ---[ 156]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 155]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 154]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 153]---> Adder-cost: 141   maxlim: 16382   bits: 15/14
c ---[ 152]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 151]---> Adder-cost: 150   maxlim: 16382   bits: 15/14
c ---[ 150]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 149]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 148]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 147]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 146]---> Adder-cost: 148   maxlim: 16382   bits: 15/14
c ---[ 144]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 143]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 142]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 141]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 140]---> Adder-cost: 114   maxlim: 8190   bits: 14/13
c ---[ 139]---> Adder-cost: 114   maxlim: 8190   bits: 14/13
c ---[ 138]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 137]---> Adder-cost: 138   maxlim: 8190   bits: 14/13
c ---[ 136]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 135]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 134]---> Adder-cost: 136   maxlim: 8190   bits: 14/13
c ---[ 132]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 131]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 130]---> Adder-cost: 160   maxlim: 8190   bits: 14/13
c ---[ 129]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 128]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[ 127]---> Adder-cost: 164   maxlim: 8190   bits: 14/13
c ---[ 126]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 125]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[ 124]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 123]---> Adder-cost: 141   maxlim: 16382   bits: 15/14
c ---[ 122]---> Adder-cost: 167   maxlim: 16382   bits: 15/14
c ---[ 120]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 119]---> Adder-cost: 152   maxlim: 16382   bits: 15/14
c ---[ 118]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 117]---> Adder-cost: 169   maxlim: 16382   bits: 15/14
c ---[ 116]---> Adder-cost: 180   maxlim: 16382   bits: 15/14
c ---[ 115]---> Adder-cost: 122   maxlim: 16382   bits: 15/14
c ---[ 114]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 113]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 112]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 111]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 110]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 108]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[ 107]---> Adder-cost: 167   maxlim: 16382   bits: 15/14
c ---[ 106]---> Adder-cost: 115   maxlim: 16382   bits: 15/14
c ---[ 105]---> Adder-cost: 145   maxlim: 16382   bits: 15/14
c ---[ 104]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[ 103]---> Adder-cost: 143   maxlim: 16382   bits: 15/14
c ---[ 102]---> Adder-cost: 169   maxlim: 16382   bits: 15/14
c ---[ 101]---> Adder-cost: 167   maxlim: 16382   bits: 15/14
c ---[ 100]---> Adder-cost: 171   maxlim: 16382   bits: 15/14
c ---[  99]---> Adder-cost: 94   maxlim: 8190   bits: 14/13
c ---[  98]---> Adder-cost: 140   maxlim: 8190   bits: 14/13
c ---[  96]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[  95]---> Adder-cost: 158   maxlim: 8190   bits: 14/13
c ---[  94]---> Adder-cost: 138   maxlim: 8190   bits: 14/13
c ---[  93]---> Adder-cost: 164   maxlim: 8190   bits: 14/13
c ---[  92]---> Adder-cost: 166   maxlim: 8190   bits: 14/13
c ---[  91]---> Adder-cost: 164   maxlim: 8190   bits: 14/13
c ---[  89]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[  87]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[  85]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[  83]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[  81]---> Adder-cost: 187   maxlim: 32767   bits: 16/15
c ---[  79]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[  77]---> Adder-cost: 192   maxlim: 32767   bits: 16/15
c ---[  75]---> Adder-cost: 272   maxlim: 80633   bits: 18/17
c ---[  73]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[  71]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[  69]---> Adder-cost: 296   maxlim: 88569   bits: 18/17
c ---[  67]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[  65]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[  63]---> Adder-cost: 283   maxlim: 88441   bits: 18/17
c ---[  61]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[  59]---> Adder-cost: 280   maxlim: 112889   bits: 18/17
c ---[  57]---> Adder-cost: 336   maxlim: 112761   bits: 18/17
c ---[  55]---> Adder-cost: 336   maxlim: 113017   bits: 18/17
c ---[  53]---> Adder-cost: 308   maxlim: 113145   bits: 18/17
c ---[  51]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[  49]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[  47]---> Adder-cost: 294   maxlim: 113529   bits: 18/17
c ---[  45]---> Adder-cost: 260   maxlim: 55673   bits: 17/16
c ---[  43]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[  41]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[  39]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[  37]---> Adder-cost: 286   maxlim: 56569   bits: 17/16
c ---[  35]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[  33]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[  31]---> Adder-cost: 273   maxlim: 56313   bits: 17/16
c ---[  29]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[  27]---> Adder-cost: 286   maxlim: 56313   bits: 17/16
c ---[  25]---> Adder-cost: 286   maxlim: 55417   bits: 17/16
c ---[  23]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[  21]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[  19]---> Adder-cost: 286   maxlim: 55929   bits: 17/16
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: 48   maxlim: 19711   bits: 16/15
c ---[  14]---> Adder-cost: 46   maxlim: 21887   bits: 16/15
c ---[  13]---> Adder-cost: 44   maxlim: 16767   bits: 16/15
c ---[  12]---> Adder-cost: 48   maxlim: 16895   bits: 16/15
c ---[  11]---> Adder-cost: 46   maxlim: 20223   bits: 16/15
c ---[  10]---> Adder-cost: 48   maxlim: 18559   bits: 16/15
c ---[   9]---> Adder-cost: 46   maxlim: 17407   bits: 16/15
c ---[   8]---> Adder-cost: 47   maxlim: 16255   bits: 15/14
c ---[   7]---> Adder-cost: 54   maxlim: 17662   bits: 16/15
c ---[   6]---> Adder-cost: 54   maxlim: 18558   bits: 16/15
c ---[   5]---> Adder-cost: 59   maxlim: 24446   bits: 16/15
c ---[   4]---> Adder-cost: 59   maxlim: 24446   bits: 16/15
c ---[   3]---> Adder-cost: 54   maxlim: 17790   bits: 16/15
c ---[   2]---> Adder-cost: 54   maxlim: 17150   bits: 16/15
c ---[   1]---> Adder-cost: 59   maxlim: 24702   bits: 16/15
c ---[   0]---> Adder-cost: 59   maxlim: 24190   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  418745  1521216 |  139581       0        0     nan |  0.000 % |
c |       100 |  418745  1521216 |  153539     100      278     2.8 | 17.539 % |
c |       252 |  418737  1521190 |  168893     251      909     3.6 | 17.540 % |
c |       477 |  418713  1521112 |  185782     473     1802     3.8 | 17.544 % |
c |       814 |  418681  1521008 |  204360     806     3052     3.8 | 17.549 % |
c |      1320 |  418665  1520956 |  224796    1310     5347     4.1 | 17.551 % |
c |      2079 |  418600  1520749 |  247276    2062     9499     4.6 | 17.563 % |
c |      3218 |  418520  1520489 |  272003    3191    17667     5.5 | 17.576 % |
c |      4927 |  418464  1520307 |  299204    4893    33022     6.7 | 17.584 % |
c |      7489 |  418360  1519969 |  329124    7442    51610     6.9 | 17.600 % |
c |     11333 |  418198  1519461 |  362037   11270    80700     7.2 | 17.634 % |
c |     17100 |  418184  1519417 |  398240   17035   249636    14.7 | 17.637 % |
c |     25749 |  418159  1519334 |  438064   25553   592993    23.2 | 17.640 % |
c |     38725 |  418143  1519282 |  481871   38527  1645243    42.7 | 17.643 % |
c |     58187 |  418126  1519225 |  530058   57858  3599962    62.2 | 17.645 % |
c |     87379 |  418080  1519077 |  583064   87044  4726767    54.3 | 17.653 % |
c |    131168 |  417981  1518758 |  641370  130818  6916828    52.9 | 17.669 % |
c |    196852 |  417939  1518624 |  705508  196496 13009383    66.2 | 17.677 % |
c |    295378 |  417923  1518572 |  776058  295020 32790212   111.1 | 17.680 % |
c |    443171 |  417909  1518528 |  853664  442811 47693698   107.7 | 17.682 % |
#### 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.92 0.97 0.91 2/54 32651
Raw data (stat): 32651 (runsolver) R 32650 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483955210 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.0004 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 9325 0 0 0 975 24 0 0 25 0 1 0 483955210 44642304 8932 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10899 8932 603 41 0 10858 0
vsize: 43596
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 9513 0 0 0 1974 25 0 0 25 0 1 0 483955210 45449216 9120 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 9120 603 41 0 11055 0
vsize: 44384
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 10017 0 0 0 2972 27 0 0 25 0 1 0 483955210 47489024 9624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11594 9624 603 41 0 11553 0
vsize: 46376
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 10691 0 0 0 3970 29 0 0 25 0 1 0 483955210 50188288 10298 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12253 10298 603 41 0 12212 0
vsize: 49012
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 11623 0 0 0 4967 32 0 0 25 0 1 0 483955210 54083584 11230 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13204 11230 603 41 0 13163 0
vsize: 52816
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 12194 0 0 0 5964 35 0 0 25 0 1 0 483955210 56381440 11801 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13765 11801 603 41 0 13724 0
vsize: 55060
[startup+70.0267 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 13066 0 0 0 6964 38 0 0 25 0 1 0 483955210 59883520 12673 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 12673 603 41 0 14579 0
vsize: 58480
[startup+80.0443 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 13794 0 0 0 7962 41 0 0 25 0 1 0 483955210 62853120 13401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15345 13401 603 41 0 15304 0
vsize: 61380
[startup+90.0438 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 14111 0 0 0 8961 42 0 0 25 0 1 0 483955210 64466944 13718 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15739 13718 603 41 0 15698 0
vsize: 62956
[startup+100.045 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 14888 0 0 0 9959 44 0 0 25 0 1 0 483955210 67571712 14495 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16497 14495 603 41 0 16456 0
vsize: 65988
[startup+110.045 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 15249 0 0 0 10958 46 0 0 25 0 1 0 483955210 69083136 14856 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16866 14856 603 41 0 16825 0
vsize: 67464
[startup+120.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 15507 0 0 0 11958 47 0 0 25 0 1 0 483955210 70090752 15114 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17112 15114 603 41 0 17071 0
vsize: 68448
[startup+130.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 15834 0 0 0 12957 48 0 0 25 0 1 0 483955210 71438336 15441 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17441 15441 603 41 0 17400 0
vsize: 69764
[startup+140.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 16274 0 0 0 13955 49 0 0 25 0 1 0 483955210 73183232 15881 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17867 15881 603 41 0 17826 0
vsize: 71468
[startup+150.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 16743 0 0 0 14954 51 0 0 25 0 1 0 483955210 75071488 16350 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18328 16350 603 41 0 18287 0
vsize: 73312
[startup+160.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 17835 0 0 0 15951 54 0 0 25 0 1 0 483955210 79519744 17442 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19414 17442 603 41 0 19373 0
vsize: 77656
[startup+170.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 18361 0 0 0 16950 55 0 0 25 0 1 0 483955210 82194432 17968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20067 17968 603 41 0 20026 0
vsize: 80268
[startup+180.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 18733 0 0 0 17948 57 0 0 25 0 1 0 483955210 83677184 18340 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20429 18340 603 41 0 20388 0
vsize: 81716
[startup+190.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 19214 0 0 0 18946 59 0 0 25 0 1 0 483955210 85561344 18821 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20889 18821 603 41 0 20848 0
vsize: 83556
[startup+200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 19605 0 0 0 19944 61 0 0 25 0 1 0 483955210 87179264 19212 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21284 19212 603 41 0 21243 0
vsize: 85136
[startup+210.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 20354 0 0 0 20941 65 0 0 25 0 1 0 483955210 90275840 19961 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22040 19961 603 41 0 21999 0
vsize: 88160
[startup+220.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 21053 0 0 0 21938 67 0 0 25 0 1 0 483955210 93106176 20660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22731 20660 603 41 0 22690 0
vsize: 90924
[startup+230.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 21738 0 0 0 22936 70 0 0 25 0 1 0 483955210 95797248 21345 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23388 21345 603 41 0 23347 0
vsize: 93552
[startup+240.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 22210 0 0 0 23934 72 0 0 25 0 1 0 483955210 97808384 21817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23879 21817 603 41 0 23838 0
vsize: 95516
[startup+250.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 22760 0 0 0 24932 74 0 0 25 0 1 0 483955210 99966976 22367 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24406 22367 603 41 0 24365 0
vsize: 97624
[startup+260.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 23196 0 0 0 25930 76 0 0 25 0 1 0 483955210 101838848 22803 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24863 22803 603 41 0 24822 0
vsize: 99452
[startup+270.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 23563 0 0 0 26929 77 0 0 25 0 1 0 483955210 103321600 23170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25225 23170 603 41 0 25184 0
vsize: 100900
[startup+280.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 24322 0 0 0 27927 79 0 0 25 0 1 0 483955210 106405888 23929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25978 23929 603 41 0 25937 0
vsize: 103912
[startup+290.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 24808 0 0 0 28925 81 0 0 25 0 1 0 483955210 108290048 24415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26438 24415 603 41 0 26397 0
vsize: 105752
[startup+300.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 25494 0 0 0 29924 83 0 0 25 0 1 0 483955210 111124480 25101 4294967295 134512640 134672761 3221224544 3221223692 134565968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27130 25101 603 41 0 27089 0
vsize: 108520
[startup+310.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 26178 0 0 0 30922 85 0 0 25 0 1 0 483955210 113950720 25785 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27820 25785 603 41 0 27779 0
vsize: 111280
[startup+320.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 26771 0 0 0 31921 86 0 0 25 0 1 0 483955210 116248576 26378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28381 26378 603 41 0 28340 0
vsize: 113524
[startup+330.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 27369 0 0 0 32919 89 0 0 25 0 1 0 483955210 118808576 26976 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29006 26976 603 41 0 28965 0
vsize: 116024
[startup+340.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 28040 0 0 0 33916 91 0 0 25 0 1 0 483955210 121491456 27647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29661 27647 603 41 0 29620 0
vsize: 118644
[startup+350.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 28524 0 0 0 34915 93 0 0 25 0 1 0 483955210 123506688 28131 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30153 28131 603 41 0 30112 0
vsize: 120612
[startup+360.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 29021 0 0 0 35913 95 0 0 25 0 1 0 483955210 125517824 28628 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30644 28628 603 41 0 30603 0
vsize: 122576
[startup+370.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 29528 0 0 0 36912 96 0 0 25 0 1 0 483955210 127537152 29135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31137 29135 603 41 0 31096 0
vsize: 124548
[startup+380.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 30081 0 0 0 37911 98 0 0 25 0 1 0 483955210 129810432 29688 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31692 29688 603 41 0 31651 0
vsize: 126768
[startup+390.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 30586 0 0 0 38909 99 0 0 25 0 1 0 483955210 131960832 30193 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32217 30193 603 41 0 32176 0
vsize: 128868
[startup+400.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 31127 0 0 0 39907 101 0 0 25 0 1 0 483955210 134119424 30734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32744 30734 603 41 0 32703 0
vsize: 130976
[startup+410.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 31645 0 0 0 40906 102 0 0 25 0 1 0 483955210 136265728 31252 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33268 31252 603 41 0 33227 0
vsize: 133072
[startup+420.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 32127 0 0 0 41905 103 0 0 25 0 1 0 483955210 138272768 31734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33758 31734 603 41 0 33717 0
vsize: 135032
[startup+430.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 32637 0 0 0 42904 105 0 0 25 0 1 0 483955210 140283904 32244 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34249 32244 603 41 0 34208 0
vsize: 136996
[startup+440.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 33110 0 0 0 43902 107 0 0 25 0 1 0 483955210 142286848 32717 4294967295 134512640 134672761 3221224544 3221223728 134559607 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34738 32717 603 41 0 34697 0
vsize: 138952
[startup+450.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 33623 0 0 0 44900 109 0 0 25 0 1 0 483955210 144297984 33230 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35229 33230 603 41 0 35188 0
vsize: 140916
[startup+460.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 34154 0 0 0 45899 110 0 0 25 0 1 0 483955210 146444288 33761 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35753 33761 603 41 0 35712 0
vsize: 143012
[startup+470.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 34713 0 0 0 46897 113 0 0 25 0 1 0 483955210 148742144 34320 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36314 34320 603 41 0 36273 0
vsize: 145256
[startup+480.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 35264 0 0 0 47896 114 0 0 25 0 1 0 483955210 151072768 34871 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36883 34871 603 41 0 36842 0
vsize: 147532
[startup+490.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 35806 0 0 0 48894 115 0 0 25 0 1 0 483955210 153210880 35413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37405 35413 603 41 0 37364 0
vsize: 149620
[startup+500.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 36306 0 0 0 49893 117 0 0 25 0 1 0 483955210 155357184 35913 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37929 35913 603 41 0 37888 0
vsize: 151716
[startup+510.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 36808 0 0 0 50891 119 0 0 25 0 1 0 483955210 157380608 36415 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38423 36415 603 41 0 38382 0
vsize: 153692
[startup+520.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 37328 0 0 0 51890 120 0 0 25 0 1 0 483955210 159514624 36935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38944 36935 603 41 0 38903 0
vsize: 155776
[startup+530.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 37786 0 0 0 52888 122 0 0 25 0 1 0 483955210 161398784 37393 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39404 37393 603 41 0 39363 0
vsize: 157616
[startup+540.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 38245 0 0 0 53887 124 0 0 25 0 1 0 483955210 163270656 37852 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39861 37852 603 41 0 39820 0
vsize: 159444
[startup+550.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 38683 0 0 0 54884 127 0 0 25 0 1 0 483955210 166191104 38290 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40574 38290 603 41 0 40533 0
vsize: 162296
[startup+560.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 39140 0 0 0 55882 129 0 0 25 0 1 0 483955210 168050688 38747 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41028 38747 603 41 0 40987 0
vsize: 164112
[startup+570.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 39626 0 0 0 56880 131 0 0 25 0 1 0 483955210 170070016 39233 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41521 39233 603 41 0 41480 0
vsize: 166084
[startup+580.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 40076 0 0 0 57880 132 0 0 25 0 1 0 483955210 171921408 39683 4294967295 134512640 134672761 3221224544 3221223728 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41973 39683 603 41 0 41932 0
vsize: 167892
[startup+590.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 40491 0 0 0 58879 133 0 0 25 0 1 0 483955210 173531136 40098 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42366 40098 603 41 0 42325 0
vsize: 169464
[startup+600.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 40908 0 0 0 59878 134 0 0 25 0 1 0 483955210 175259648 40515 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42788 40515 603 41 0 42747 0
vsize: 171152
[startup+610.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 41352 0 0 0 60876 135 0 0 25 0 1 0 483955210 177123328 40959 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43243 40959 603 41 0 43202 0
vsize: 172972
[startup+620.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 41804 0 0 0 61876 136 0 0 25 0 1 0 483955210 178987008 41411 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43698 41411 603 41 0 43657 0
vsize: 174792
[startup+630.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 42254 0 0 0 62875 137 0 0 25 0 1 0 483955210 180871168 41861 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44158 41861 603 41 0 44117 0
vsize: 176632
[startup+640.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 42640 0 0 0 63874 138 0 0 25 0 1 0 483955210 182341632 42247 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44517 42247 603 41 0 44476 0
vsize: 178068
[startup+650.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 43055 0 0 0 64873 139 0 0 25 0 1 0 483955210 184094720 42662 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44945 42662 603 41 0 44904 0
vsize: 179780
[startup+660.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 43344 0 0 0 65873 140 0 0 25 0 1 0 483955210 185315328 42951 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45243 42951 603 41 0 45202 0
vsize: 180972
[startup+670.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 43558 0 0 0 66873 140 0 0 25 0 1 0 483955210 186126336 43165 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45441 43165 603 41 0 45400 0
vsize: 181764
[startup+680.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 43884 0 0 0 67872 141 0 0 25 0 1 0 483955210 187473920 43491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45770 43491 603 41 0 45729 0
vsize: 183080
[startup+690.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 44299 0 0 0 68871 142 0 0 25 0 1 0 483955210 189214720 43906 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46195 43906 603 41 0 46154 0
vsize: 184780
[startup+700.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 44671 0 0 0 69871 143 0 0 25 0 1 0 483955210 190697472 44278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46557 44278 603 41 0 46516 0
vsize: 186228
[startup+710.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 45069 0 0 0 70871 144 0 0 25 0 1 0 483955210 192303104 44676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46949 44676 603 41 0 46908 0
vsize: 187796
[startup+720.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 45321 0 0 0 71870 144 0 0 25 0 1 0 483955210 193376256 44928 4294967295 134512640 134672761 3221224544 3221223728 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47211 44928 603 41 0 47170 0
vsize: 188844
[startup+730.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 45611 0 0 0 72870 145 0 0 25 0 1 0 483955210 194461696 45218 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47476 45218 603 41 0 47435 0
vsize: 189904
[startup+740.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 45892 0 0 0 73869 146 0 0 25 0 1 0 483955210 195670016 45499 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47771 45499 603 41 0 47730 0
vsize: 191084
[startup+750.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 46098 0 0 0 74869 146 0 0 25 0 1 0 483955210 196481024 45705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47969 45705 603 41 0 47928 0
vsize: 191876
[startup+760.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 46343 0 0 0 75868 147 0 0 25 0 1 0 483955210 197554176 45950 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48231 45950 603 41 0 48190 0
vsize: 192924
[startup+770.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 46584 0 0 0 76868 147 0 0 25 0 1 0 483955210 198492160 46191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48460 46191 603 41 0 48419 0
vsize: 193840
[startup+780.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 46824 0 0 0 77867 148 0 0 25 0 1 0 483955210 199438336 46431 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48691 46431 603 41 0 48650 0
vsize: 194764
[startup+790.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 47227 0 0 0 78867 149 0 0 25 0 1 0 483955210 201060352 46834 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49087 46834 603 41 0 49046 0
vsize: 196348
[startup+800.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 47973 0 0 0 79864 151 0 0 25 0 1 0 483955210 204165120 47580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49845 47581 603 41 0 49804 0
vsize: 199380
[startup+810.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 48903 0 0 0 80862 154 0 0 25 0 1 0 483955210 207937536 48510 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50766 48510 603 41 0 50725 0
vsize: 203064
[startup+820.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 49533 0 0 0 81861 155 0 0 25 0 1 0 483955210 210505728 49140 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51393 49140 603 41 0 51352 0
vsize: 205572
[startup+830.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 50518 0 0 0 82858 158 0 0 25 0 1 0 483955210 214532096 50125 4294967295 134512640 134672761 3221224544 3221223728 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52376 50125 603 41 0 52335 0
vsize: 209504
[startup+840.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 51336 0 0 0 83856 161 0 0 25 0 1 0 483955210 217776128 50943 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53168 50943 603 41 0 53127 0
vsize: 212672
[startup+850.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 52117 0 0 0 84853 163 0 0 25 0 1 0 483955210 221003776 51724 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53956 51724 603 41 0 53915 0
vsize: 215824
[startup+860.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 52797 0 0 0 85851 165 0 0 25 0 1 0 483955210 223813632 52404 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54642 52404 603 41 0 54601 0
vsize: 218568
[startup+870.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 53468 0 0 0 86850 167 0 0 25 0 1 0 483955210 226488320 53075 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55295 53075 603 41 0 55254 0
vsize: 221180
[startup+880.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 53766 0 0 0 87850 167 0 0 25 0 1 0 483955210 227708928 53373 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55593 53373 603 41 0 55552 0
vsize: 222372
[startup+890.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 54154 0 0 0 88848 169 0 0 25 0 1 0 483955210 229351424 53761 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55994 53761 603 41 0 55953 0
vsize: 223976
[startup+900.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 54561 0 0 0 89848 170 0 0 25 0 1 0 483955210 230973440 54168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56390 54168 603 41 0 56349 0
vsize: 225560
[startup+910.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 54904 0 0 0 90847 170 0 0 25 0 1 0 483955210 232321024 54511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56719 54511 603 41 0 56678 0
vsize: 226876
[startup+920.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 55540 0 0 0 91845 172 0 0 25 0 1 0 483955210 234995712 55147 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57372 55147 603 41 0 57331 0
vsize: 229488
[startup+930.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 56193 0 0 0 92844 174 0 0 25 0 1 0 483955210 237678592 55800 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58027 55800 603 41 0 57986 0
vsize: 232108
[startup+940.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 56450 0 0 0 93844 174 0 0 25 0 1 0 483955210 238620672 56057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58257 56057 603 41 0 58216 0
vsize: 233028
[startup+950.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 56770 0 0 0 94844 174 0 0 25 0 1 0 483955210 239972352 56377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58587 56377 603 41 0 58546 0
vsize: 234348
[startup+960.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 57053 0 0 0 95843 175 0 0 25 0 1 0 483955210 241061888 56660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58853 56660 603 41 0 58812 0
vsize: 235412
[startup+970.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 57316 0 0 0 96842 176 0 0 25 0 1 0 483955210 242139136 56923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59116 56923 603 41 0 59075 0
vsize: 236464
[startup+980.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 57609 0 0 0 97841 177 0 0 25 0 1 0 483955210 243343360 57216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59410 57216 603 41 0 59369 0
vsize: 237640
[startup+990.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 57881 0 0 0 98841 178 0 0 25 0 1 0 483955210 244547584 57488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59704 57488 603 41 0 59663 0
vsize: 238816
[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 58147 0 0 0 99841 178 0 0 25 0 1 0 483955210 245620736 57754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59966 57754 603 41 0 59925 0
vsize: 239864
[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 58394 0 0 0 100840 179 0 0 25 0 1 0 483955210 246566912 58001 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60197 58001 603 41 0 60156 0
vsize: 240788
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 58752 0 0 0 101839 180 0 0 25 0 1 0 483955210 248045568 58359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60558 58359 603 41 0 60517 0
vsize: 242232
[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 59129 0 0 0 102838 181 0 0 25 0 1 0 483955210 249524224 58736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60919 58736 603 41 0 60878 0
vsize: 243676
[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 59529 0 0 0 103837 183 0 0 25 0 1 0 483955210 251142144 59136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61314 59136 603 41 0 61273 0
vsize: 245256
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 59952 0 0 0 104836 184 0 0 25 0 1 0 483955210 252891136 59559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61741 59559 603 41 0 61700 0
vsize: 246964
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 60370 0 0 0 105835 185 0 0 25 0 1 0 483955210 254648320 59977 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62170 59977 603 41 0 62129 0
vsize: 248680
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 60710 0 0 0 106834 186 0 0 25 0 1 0 483955210 256000000 60317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62500 60317 603 41 0 62459 0
vsize: 250000
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 60844 0 0 0 107834 186 0 0 25 0 1 0 483955210 256540672 60451 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62632 60451 603 41 0 62591 0
vsize: 250528
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 61032 0 0 0 108834 187 0 0 25 0 1 0 483955210 257343488 60639 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62828 60639 603 41 0 62787 0
vsize: 251312
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 61518 0 0 0 109833 188 0 0 25 0 1 0 483955210 259362816 61125 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63321 61125 603 41 0 63280 0
vsize: 253284
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 61871 0 0 0 110830 190 0 0 25 0 1 0 483955210 260706304 61478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63649 61478 603 41 0 63608 0
vsize: 254596
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 62155 0 0 0 111829 191 0 0 25 0 1 0 483955210 261935104 61762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63949 61762 603 41 0 63908 0
vsize: 255796
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 62446 0 0 0 112829 192 0 0 25 0 1 0 483955210 263147520 62053 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64245 62053 603 41 0 64204 0
vsize: 256980
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 62806 0 0 0 113828 193 0 0 25 0 1 0 483955210 264622080 62413 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64605 62413 603 41 0 64564 0
vsize: 258420
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 63211 0 0 0 114827 193 0 0 25 0 1 0 483955210 266215424 62818 4294967295 134512640 134672761 3221224544 3221223728 134559604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64994 62818 603 41 0 64953 0
vsize: 259976
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 63768 0 0 0 115826 195 0 0 25 0 1 0 483955210 268509184 63375 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65554 63375 603 41 0 65513 0
vsize: 262216
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 64472 0 0 0 116825 196 0 0 25 0 1 0 483955210 271327232 64079 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66242 64079 603 41 0 66201 0
vsize: 264968
[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 65116 0 0 0 117823 198 0 0 25 0 1 0 483955210 273989632 64723 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66892 64723 603 41 0 66851 0
vsize: 267568
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 65682 0 0 0 118822 199 0 0 25 0 1 0 483955210 276275200 65289 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67450 65289 603 41 0 67409 0
vsize: 269800
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32651
Raw data (stat): 32651 (minisat+) R 32650 5897 5896 0 -1 0 66197 0 0 0 119821 200 0 0 25 0 1 0 483955210 278425600 65804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67975 65804 603 41 0 67934 0
vsize: 271900
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32651
Raw data (stat): 32651 (minisat+) Z 32650 5897 5896 0 -1 12 66199 0 0 0 119821 212 0 0 25 0 1 0 483955210 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.23
CPU time (s): 1200.34
CPU user time (s): 1198.21
CPU system time (s): 2.12868
CPU usage (%): 100.01
Max. virtual memory (Kb): 271900
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####