PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-bnl1.opb
MD5SUM	03a27b3b499acf5b0d4b0eee83413d97
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	19660
Biggest coefficient in the objective function	12635026227200
Number of bits for the biggest coefficient in the objective function	44
Sum of the numbers in the objective function	1038651120525150
Number of bits of the sum of numbers in the objective function	50
Biggest number in a constraint	12635026227200
Number of bits of the biggest number in a constraint	44
Biggest sum of numbers in a constraint	1038651120525150
Number of bits of the biggest sum of numbers	50
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.202968
Number of variables	23500
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	632
Minimum length of a constraint	20
Maximum length of a constraint	1520
Trace number 31012

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        919880 kB
Buffers:         24692 kB
Cached:          66764 kB
SwapCached:        548 kB
Active:          18056 kB
Inactive:        75852 kB
HighTotal:      131008 kB
HighFree:        85400 kB
LowTotal:       903652 kB
LowFree:        834480 kB
SwapTotal:     2097892 kB
SwapFree:      2096792 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5868 kB
Slab:            15044 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:40:38 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22380 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 840 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssss.s...s
c ---[ 846]---> BDD-cost:  139
c ---[ 845]---> BDD-cost:  104
c ---[ 844]---> BDD-cost:   29
c ---[ 843]---> BDD-cost:   74
c ---[ 842]---> BDD-cost:   26
c ---[ 841]---> BDD-cost:   49
c ---[ 840]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 5 2 5 2
c ---[ 839]---> Sorter-cost: 1050     Base: 2 2 2 2 5 2 2 2 2 2 2
c ---[ 838]---> Sorter-cost:  206     Base: 2 2 2 2 2 5 2
c ---[ 837]---> Sorter-cost:  445     Base: 2 2 2 2 3 2 2 2 2 2
c ---[ 836]---> BDD-cost:  136
c ---[ 835]---> Sorter-cost:  519     Base: 2 2 5 2 2 2 2 2
c ---[ 834]---> Adder-cost: 972   maxlim: 33760185   bits: 26/26
c ---[ 833]---> Adder-cost: 912   maxlim: 24241081   bits: 25/25
c ---[ 832]---> Adder-cost: 788   maxlim: 9018681   bits: 24/24
c ---[ 831]---> BDD-cost:    4
c ---[ 830]---> Adder-cost: 884   maxlim: 19606201   bits: 25/25
c ---[ 829]---> BDD-cost:   14
c ---[ 828]---> Adder-cost: 1044   maxlim: 65063353   bits: 27/26
c ---[ 827]---> Adder-cost: 702   maxlim: 4927097   bits: 23/23
c ---[ 826]---> Adder-cost: 884   maxlim: 19644601   bits: 25/25
c ---[ 824]---> BDD-cost:   14
c ---[ 823]---> BDD-cost:    6
c ---[ 822]---> Adder-cost: 660   maxlim: 1539178   bits: 21/21
c ---[ 821]---> Adder-cost: 956   maxlim: 8633272   bits: 24/24
c ---[ 820]---> Adder-cost: 810   maxlim: 2235565   bits: 22/22
c ---[ 819]---> BDD-cost:  967
c ---[ 818]---> Adder-cost: 322   maxlim: 12095   bits: 14/14
c ---[ 817]---> Adder-cost: 1140   maxlim: 73545145   bits: 27/27
c ---[ 816]---> Adder-cost: 762   maxlim: 6436473   bits: 23/23
c ---[ 815]---> Adder-cost: 976   maxlim: 25443769   bits: 25/25
c ---[ 814]---> Adder-cost: 866   maxlim: 12046393   bits: 24/24
c ---[ 813]---> BDD-cost:  105
c ---[ 812]---> Adder-cost: 948   maxlim: 20552889   bits: 25/25
c ---[ 811]---> BDD-cost:   58
c ---[ 810]---> Adder-cost: 1230   maxlim: 137853881   bits: 28/28
c ---[ 809]---> Adder-cost: 662   maxlim: 3194649   bits: 22/22
c ---[ 808]---> Adder-cost: 848   maxlim: 10285369   bits: 24/24
c ---[ 807]---> Adder-cost: 948   maxlim: 20488889   bits: 25/25
c ---[ 806]---> Adder-cost: 392   maxlim: 403785   bits: 20/19
c ---[ 805]---> BDD-cost:   24
c ---[ 804]---> BDD-cost:  108
c ---[ 803]---> Adder-cost: 788   maxlim: 3137514   bits: 22/22
c ---[ 801]---> Adder-cost: 1122   maxlim: 18208632   bits: 25/25
c ---[ 800]---> Adder-cost: 990   maxlim: 4612589   bits: 23/23
c ---[ 799]---> Adder-cost: 766   maxlim: 3918477   bits: 23/22
c ---[ 798]---> Adder-cost: 824   maxlim: 2475634   bits: 22/22
c ---[ 797]---> Adder-cost: 1220   maxlim: 74389945   bits: 27/27
c ---[ 796]---> Adder-cost: 1024   maxlim: 20260537   bits: 25/25
c ---[ 795]---> Adder-cost: 1022   maxlim: 26083769   bits: 25/25
c ---[ 794]---> Adder-cost: 984   maxlim: 19172537   bits: 25/25
c ---[ 793]---> BDD-cost:  418
c ---[ 792]---> Adder-cost: 1060   maxlim: 26442169   bits: 25/25
c ---[ 791]---> BDD-cost:  239
c ---[ 790]---> Adder-cost: 1378   maxlim: 227210169   bits: 28/28
c ---[ 789]---> Adder-cost: 1086   maxlim: 36442553   bits: 26/26
c ---[ 788]---> Adder-cost: 1026   maxlim: 22127289   bits: 25/25
c ---[ 787]---> Adder-cost: 1078   maxlim: 34714553   bits: 26/26
c ---[ 786]---> Adder-cost: 494   maxlim: 982745   bits: 21/20
c ---[ 785]---> BDD-cost:   49
c ---[ 784]---> BDD-cost:  384
c ---[ 783]---> Adder-cost: 1038   maxlim: 12120266   bits: 24/24
c ---[ 781]---> Adder-cost: 1306   maxlim: 35163032   bits: 26/26
c ---[ 780]---> Adder-cost: 1196   maxlim: 17394637   bits: 25/25
c ---[ 779]---> Adder-cost: 970   maxlim: 9728909   bits: 24/24
c ---[ 778]---> Adder-cost: 960   maxlim: 5565426   bits: 23/23
c ---[ 777]---> Adder-cost: 1388   maxlim: 142973881   bits: 28/28
c ---[ 776]---> Adder-cost: 1280   maxlim: 77807545   bits: 27/27
c ---[ 775]---> Adder-cost: 1094   maxlim: 26723769   bits: 25/25
c ---[ 774]---> Adder-cost: 1056   maxlim: 21423289   bits: 25/25
c ---[ 773]---> Sorter-cost: 1582     Base: 2 2 2 5 5 5 5 2 2 2 2 2 2
c ---[ 772]---> Adder-cost: 1174   maxlim: 38271673   bits: 26/26
c ---[ 771]---> Sorter-cost: 2586     Base: 2 2 2 2 2 2 13 3 2 2 2 2
c ---[ 770]---> Adder-cost: 1504   maxlim: 274228153   bits: 29/29
c ---[ 769]---> Adder-cost: 1456   maxlim: 256983993   bits: 29/28
c ---[ 768]---> Adder-cost: 1280   maxlim: 77423545   bits: 27/27
c ---[ 767]---> Adder-cost: 1148   maxlim: 37996473   bits: 26/26
c ---[ 766]---> Adder-cost: 604   maxlim: 1789017   bits: 21/21
c ---[ 765]---> BDD-cost:   78
c ---[ 764]---> Sorter-cost: 1816     Base: 2 2 5 5 5 5 2 2 2 2 2 2 2 2
c ---[ 763]---> Adder-cost: 1230   maxlim: 24386442   bits: 25/25
c ---[ 761]---> Adder-cost: 1480   maxlim: 64873176   bits: 27/26
c ---[ 760]---> Adder-cost: 1422   maxlim: 34995085   bits: 26/26
c ---[ 759]---> Adder-cost: 1226   maxlim: 32646029   bits: 26/25
c ---[ 758]---> Adder-cost: 1220   maxlim: 19191538   bits: 25/25
c ---[ 757]---> Adder-cost: 212   maxlim: 12460   bits: 14/14
c ---[ 755]---> BDD-cost:    0
c ---[ 753]---> BDD-cost:    0
c ---[ 751]---> BDD-cost:    0
c ---[ 750]---> BDD-cost:    9
c ---[ 749]---> Adder-cost: 230   maxlim: 23048   bits: 15/15
c ---[ 748]---> Adder-cost: 168   maxlim: 2056   bits: 12/12
c ---[ 747]---> Adder-cost: 206   maxlim: 7725   bits: 14/13
c ---[ 746]---> BDD-cost:    9
c ---[ 745]---> Adder-cost: 1108   maxlim: 29792379   bits: 25/25
c ---[ 744]---> Adder-cost: 778   maxlim: 2835419   bits: 22/22
c ---[ 742]---> BDD-cost:    0
c ---[ 740]---> BDD-cost:    0
c ---[ 737]---> BDD-cost:    0
c ---[ 736]---> BDD-cost:   21
c ---[ 735]---> Adder-cost: 1182   maxlim: 53746299   bits: 26/26
c ---[ 734]---> Adder-cost: 654   maxlim: 1411115   bits: 21/21
c ---[ 733]---> Adder-cost: 838   maxlim: 4686395   bits: 23/23
c ---[ 732]---> Adder-cost: 946   maxlim: 8884219   bits: 24/24
c ---[ 731]---> BDD-cost:  265
c ---[ 730]---> BDD-cost:   11
c ---[ 728]---> Adder-cost: 1182   maxlim: 30130299   bits: 25/25
c ---[ 727]---> Adder-cost: 1000   maxlim: 9130491   bits: 24/24
c ---[ 725]---> BDD-cost:    0
c ---[ 723]---> BDD-cost:    0
c ---[ 720]---> BDD-cost:    0
c ---[ 719]---> BDD-cost:   90
c ---[ 718]---> Adder-cost: 1332   maxlim: 86546043   bits: 27/27
c ---[ 717]---> Adder-cost: 1082   maxlim: 16586107   bits: 25/24
c ---[ 716]---> Adder-cost: 1022   maxlim: 9539579   bits: 24/24
c ---[ 715]---> Adder-cost: 1076   maxlim: 15894907   bits: 25/24
c ---[ 714]---> BDD-cost:  536
c ---[ 713]---> BDD-cost:   17
c ---[ 711]---> Adder-cost: 1158   maxlim: 56075643   bits: 26/26
c ---[ 710]---> Adder-cost: 1090   maxlim: 31778683   bits: 26/25
c ---[ 708]---> BDD-cost:    0
c ---[ 706]---> Adder-cost: 896   maxlim: 863850   bits: 21/20
c ---[ 705]---> BDD-cost:  165
c ---[ 703]---> BDD-cost:    0
c ---[ 702]---> Sorter-cost: 1850     Base: 2 2 2 3 3 3 3 3 2 2 2
c ---[ 701]---> Adder-cost: 1270   maxlim: 105038203   bits: 27/27
c ---[ 700]---> Adder-cost: 1262   maxlim: 98738555   bits: 27/27
c ---[ 699]---> Adder-cost: 1090   maxlim: 31625083   bits: 26/25
c ---[ 698]---> Adder-cost: 950   maxlim: 17414267   bits: 25/25
c ---[ 697]---> Sorter-cost: 7156     Base: 7 2 2 3 13 2 2 2 2
c ---[ 696]---> BDD-cost:   25
c ---[ 694]---> Adder-cost: 1094   maxlim: 6957153   bits: 23/23
c ---[ 693]---> Adder-cost: 1274   maxlim: 10901857   bits: 24/24
c ---[ 692]---> Adder-cost: 1518   maxlim: 23222049   bits: 25/25
c ---[ 691]---> Adder-cost: 1764   maxlim: 46987169   bits: 26/26
c ---[ 690]---> Adder-cost: 446   maxlim: 2421171   bits: 22/22
c ---[ 689]---> Adder-cost: 566   maxlim: 3867763   bits: 23/22
c ---[ 688]---> Adder-cost: 712   maxlim: 9058419   bits: 24/24
c ---[ 687]---> Adder-cost: 858   maxlim: 18564467   bits: 25/25
c ---[ 685]---> BDD-cost:   22
c ---[ 683]---> BDD-cost:   16
c ---[ 681]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   13
c ---[ 677]---> BDD-cost:   19
c ---[ 675]---> BDD-cost:   16
c ---[ 673]---> BDD-cost:    4
c ---[ 671]---> BDD-cost:   25
c ---[ 669]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   16
c ---[ 665]---> BDD-cost:   16
c ---[ 663]---> BDD-cost:    4
c ---[ 661]---> BDD-cost:    1
c ---[ 659]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   34
c ---[ 655]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:   19
c ---[ 649]---> BDD-cost:   16
c ---[ 647]---> BDD-cost:   10
c ---[ 645]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:   34
c ---[ 641]---> BDD-cost:   13
c ---[ 639]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   22
c ---[ 635]---> BDD-cost:   19
c ---[ 633]---> BDD-cost:   16
c ---[ 631]---> BDD-cost:   16
c ---[ 629]---> BDD-cost:   19
c ---[ 627]---> BDD-cost:   19
c ---[ 625]---> BDD-cost:    7
c ---[ 623]---> BDD-cost:   28
c ---[ 621]---> BDD-cost:   22
c ---[ 619]---> BDD-cost:   19
c ---[ 617]---> BDD-cost:   16
c ---[ 615]---> BDD-cost:    4
c ---[ 613]---> BDD-cost:    1
c ---[ 611]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   34
c ---[ 607]---> BDD-cost:   19
c ---[ 603]---> BDD-cost:   22
c ---[ 601]---> BDD-cost:   19
c ---[ 599]---> BDD-cost:   13
c ---[ 597]---> BDD-cost:   16
c ---[ 595]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:   16
c ---[ 589]---> BDD-cost:   22
c ---[ 587]---> BDD-cost:   16
c ---[ 585]---> BDD-cost:   13
c ---[ 583]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:   16
c ---[ 577]---> BDD-cost:    4
c ---[ 575]---> BDD-cost:   25
c ---[ 573]---> BDD-cost:   13
c ---[ 571]---> BDD-cost:   16
c ---[ 569]---> BDD-cost:   16
c ---[ 567]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    1
c ---[ 563]---> BDD-cost:   19
c ---[ 561]---> BDD-cost:   34
c ---[ 559]---> BDD-cost:   13
c ---[ 555]---> BDD-cost:   19
c ---[ 553]---> BDD-cost:   16
c ---[ 551]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   13
c ---[ 547]---> BDD-cost:   34
c ---[ 545]---> BDD-cost:   13
c ---[ 543]---> BDD-cost:   13
c ---[ 541]---> BDD-cost:   49
c ---[ 539]---> BDD-cost:  145
c ---[ 537]---> BDD-cost:  145
c ---[ 535]---> BDD-cost:  145
c ---[ 534]---> Sorter-cost: 2659     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 533]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Adder-cost: 3096   maxlim: 19660600   bits: 25/25
c ---[ 524]---> Adder-cost: 3666   maxlim: 19660600   bits: 26/25
c ---[ 522]---> Adder-cost: 3946   maxlim: 19660600   bits: 26/25
c ---[ 520]---> Adder-cost: 4498   maxlim: 19660600   bits: 26/25
c ---[ 518]---> BDD-cost:   46
c ---[ 516]---> BDD-cost:  136
c ---[ 514]---> BDD-cost:  136
c ---[ 512]---> BDD-cost:  136
c ---[ 511]---> Adder-cost: 396   maxlim: 1519285   bits: 22/21
c ---[ 510]---> Adder-cost: 421   maxlim: 2363061   bits: 23/22
c ---[ 509]---> Adder-cost: 419   maxlim: 2617013   bits: 23/22
c ---[ 508]---> Adder-cost: 423   maxlim: 2617013   bits: 23/22
c ---[ 507]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost: 1399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost: 3511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Adder-cost: 482   maxlim: 1365601974   bits: 31/31
c ---[ 501]---> Adder-cost: 604   maxlim: 1365601974   bits: 31/31
c ---[ 499]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1240     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost: 1488     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 1448     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Adder-cost: 941   maxlim: 31981446   bits: 26/25
c ---[ 489]---> Adder-cost: 1440   maxlim: 97943369   bits: 28/27
c ---[ 487]---> Adder-cost: 1394   maxlim: 133922572   bits: 28/27
c ---[ 485]---> Adder-cost: 1530   maxlim: 143916812   bits: 29/28
c ---[ 483]---> Sorter-cost: 5819     Base: 2 5 5 5 5 2 2 2 2 2 2 13
c ---[ 481]---> Sorter-cost: 6657     Base: 2 5 5 5 5 2 2 2 2 2 2 2 13
c ---[ 479]---> Sorter-cost: 7442     Base: 2 5 5 5 5 2 2 2 2 2 2 2 2 13
c ---[ 478]---> BDD-cost:  158
c ---[ 477]---> BDD-cost:  169
c ---[ 476]---> BDD-cost:  171
c ---[ 475]---> BDD-cost:  171
c ---[ 474]---> BDD-cost:   43
c ---[ 473]---> BDD-cost:  136
c ---[ 472]---> BDD-cost:  149
c ---[ 470]---> Adder-cost: 745   maxlim: 2621430   bits: 23/22
c ---[ 468]---> Adder-cost: 1067   maxlim: 7864300   bits: 24/23
c ---[ 466]---> Adder-cost: 1296   maxlim: 20971500   bits: 26/25
c ---[ 465]---> BDD-cost:    6
c ---[ 464]---> BDD-cost:    6
c ---[ 461]---> Sorter-cost:  883     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost: 1340     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost: 1401     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Adder-cost: 725   maxlim: 3145724   bits: 23/22
c ---[ 451]---> Adder-cost: 953   maxlim: 4718586   bits: 24/23
c ---[ 449]---> Adder-cost: 875   maxlim: 5767160   bits: 24/23
c ---[ 447]---> Adder-cost: 1050   maxlim: 8388600   bits: 24/23
c ---[ 446]---> BDD-cost:   52
c ---[ 445]---> BDD-cost:  163
c ---[ 444]---> BDD-cost:  171
c ---[ 443]---> Adder-cost: 620   maxlim: 572783825   bits: 30/30
c ---[ 442]---> Adder-cost: 592   maxlim: 385613009   bits: 30/29
c ---[ 441]---> Adder-cost: 680   maxlim: 853540049   bits: 31/30
c ---[ 439]---> BDD-cost:   43
c ---[ 437]---> BDD-cost:  137
c ---[ 435]---> BDD-cost:  145
c ---[ 433]---> BDD-cost:  145
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 430]---> Sorter-cost: 1414     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 429]---> Sorter-cost: 1519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 427]---> Adder-cost: 2178   maxlim: 1638350   bits: 22/21
c ---[ 425]---> Adder-cost: 2215   maxlim: 3276750   bits: 23/22
c ---[ 423]---> Adder-cost: 2312   maxlim: 6553550   bits: 24/23
c ---[ 421]---> Adder-cost: 2412   maxlim: 6553550   bits: 24/23
c ---[ 420]---> BDD-cost:   16
c ---[ 418]---> BDD-cost:   46
c ---[ 416]---> BDD-cost:  136
c ---[ 414]---> BDD-cost:  136
c ---[ 412]---> BDD-cost:  136
c ---[ 411]---> Adder-cost: 1104   maxlim: 3856281   bits: 23/22
c ---[ 410]---> Adder-cost: 1120   maxlim: 4780825   bits: 23/23
c ---[ 409]---> Adder-cost: 1170   maxlim: 5282137   bits: 24/23
c ---[ 408]---> Adder-cost: 1198   maxlim: 5496281   bits: 24/23
c ---[ 407]---> BDD-cost:   46
c ---[ 406]---> BDD-cost:   46
c ---[ 405]---> BDD-cost:   46
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   29
c ---[ 402]---> BDD-cost:   52
c ---[ 401]---> BDD-cost:    8
c ---[ 400]---> BDD-cost:   25
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    1
c ---[ 397]---> BDD-cost:   69
c ---[ 396]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[ 395]---> BDD-cost:   54
c ---[ 393]---> BDD-cost:   87
c ---[ 392]---> BDD-cost:   44
c ---[ 391]---> BDD-cost:   44
c ---[ 390]---> BDD-cost:  103
c ---[ 389]---> BDD-cost:  141
c ---[ 388]---> Sorter-cost:  470     Base: 2 2 2 2 2 5 2
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> Sorter-cost:  163     Base: 2 2 2 2 2 5
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    2
c ---[ 383]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 382]---> Sorter-cost:  922     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 381]---> Sorter-cost:  632     Base: 2 2 5 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  769     Base: 2 2 2 2 5 2 2 2 2
c ---[ 378]---> Sorter-cost:  193     Base: 2 2 2 2 2 2 2
c ---[ 377]---> Sorter-cost:  193     Base: 2 2 2 2 2 2 2
c ---[ 375]---> BDD-cost:   49
c ---[ 373]---> BDD-cost:  145
c ---[ 371]---> BDD-cost:  145
c ---[ 369]---> BDD-cost:  145
c ---[ 368]---> Adder-cost: 5356   maxlim: 335702839   bits: 29/29
c ---[ 367]---> Adder-cost: 5732   maxlim: 452271223   bits: 30/29
c ---[ 366]---> Adder-cost: 6268   maxlim: 555277559   bits: 30/30
c ---[ 365]---> Adder-cost: 6500   maxlim: 625490039   bits: 30/30
c ---[ 364]---> Adder-cost: 1003   maxlim: 3856281   bits: 23/22
c ---[ 363]---> Adder-cost: 1036   maxlim: 4780825   bits: 24/23
c ---[ 362]---> Adder-cost: 1074   maxlim: 5282137   bits: 24/23
c ---[ 361]---> Adder-cost: 1146   maxlim: 5496281   bits: 24/23
c ---[ 360]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 359]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 358]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 356]---> BDD-cost:   31
c ---[ 354]---> BDD-cost:  101
c ---[ 352]---> BDD-cost:  109
c ---[ 350]---> BDD-cost:  109
c ---[ 348]---> Adder-cost: 296   maxlim: 204700   bits: 19/18
c ---[ 346]---> Adder-cost: 338   maxlim: 409500   bits: 20/19
c ---[ 344]---> Adder-cost: 413   maxlim: 819100   bits: 21/20
c ---[ 342]---> Adder-cost: 458   maxlim: 819100   bits: 21/20
c ---[ 341]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 340]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 339]---> Sorter-cost:  823     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 337]---> Adder-cost: 3646   maxlim: 19865300   bits: 26/25
c ---[ 335]---> Adder-cost: 3870   maxlim: 20070100   bits: 26/25
c ---[ 333]---> Adder-cost: 4000   maxlim: 20479700   bits: 26/25
c ---[ 331]---> Adder-cost: 4148   maxlim: 20479700   bits: 26/25
c ---[ 329]---> Adder-cost: 1104   maxlim: 10485720   bits: 24/24
c ---[ 327]---> Adder-cost: 1578   maxlim: 20971480   bits: 25/25
c ---[ 325]---> Adder-cost: 2006   maxlim: 41943000   bits: 26/26
c ---[ 323]---> BDD-cost:  154
c ---[ 321]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Adder-cost: 426   maxlim: 334977   bits: 19/19
c ---[ 317]---> BDD-cost:    0
c ---[ 315]---> Adder-cost: 524   maxlim: 55509   bits: 16/16
c ---[ 313]---> Adder-cost: 572   maxlim: 135507   bits: 18/18
c ---[ 312]---> Sorter-cost:  631     Base: 2 2 2 2 2 2
c ---[ 311]---> Adder-cost: 182   maxlim: 1368   bits: 11/11
c ---[ 310]---> BDD-cost:   53
c ---[ 308]---> Adder-cost: 612   maxlim: 100601   bits: 17/17
c ---[ 306]---> Adder-cost: 812   maxlim: 892146   bits: 21/20
c ---[ 304]---> Sorter-cost:  979     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Adder-cost: 676   maxlim: 490186   bits: 20/19
c ---[ 298]---> Adder-cost: 474   maxlim: 761256   bits: 20/20
c ---[ 296]---> Adder-cost: 350   maxlim: 624898   bits: 20/20
c ---[ 294]---> Sorter-cost:  187     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> Sorter-cost:  177     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 3318     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 290]---> Sorter-cost: 3567     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 289]---> Sorter-cost: 4123     Base: 2 2 5 2 2 2 2 2 5 2 2 7
c ---[ 287]---> Adder-cost: 473   maxlim: 2715730   bits: 23/22
c ---[ 285]---> Adder-cost: 823   maxlim: 328372   bits: 20/19
c ---[ 284]---> BDD-cost:   45
c ---[ 283]---> BDD-cost:   10
c ---[ 281]---> Adder-cost: 1014   maxlim: 44627   bits: 17/16
c ---[ 280]---> Sorter-cost:  145     Base: 2 2 2 2 2
c ---[ 278]---> BDD-cost:    0
c ---[ 277]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2
c ---[ 276]---> BDD-cost:    6
c ---[ 274]---> Sorter-cost:  184     Base: 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Sorter-cost: 3352     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 272]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost: 3352     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 270]---> BDD-cost:  236
c ---[ 269]---> Sorter-cost:  152     Base: 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 2836     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 267]---> Sorter-cost:  129     Base: 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 2478     Base: 2 2 5 2 5 2 2 2 2
c ---[ 264]---> Adder-cost: 488   maxlim: 463505   bits: 20/19
c ---[ 262]---> BDD-cost:    0
c ---[ 260]---> BDD-cost:    0
c ---[ 258]---> BDD-cost:    0
c ---[ 257]---> Sorter-cost: 1492     Base: 2 2 2 2 2 2
c ---[ 256]---> Adder-cost: 222   maxlim: 2221   bits: 12/12
c ---[ 255]---> BDD-cost:   51
c ---[ 253]---> BDD-cost:    0
c ---[ 251]---> Adder-cost: 954   maxlim: 1466915   bits: 21/21
c ---[ 249]---> BDD-cost:    0
c ---[ 247]---> Sorter-cost: 1733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> BDD-cost:    0
c ---[ 243]---> Adder-cost: 496   maxlim: 875752   bits: 20/20
c ---[ 241]---> Adder-cost: 362   maxlim: 849154   bits: 20/20
c ---[ 239]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> BDD-cost:   25
c ---[ 237]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 236]---> Sorter-cost:  349     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost:  106     Base: 2 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 3461     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 233]---> Sorter-cost:  808     Base: 2 2 5 2 5 2 2
c ---[ 232]---> Sorter-cost: 4184     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[ 231]---> Sorter-cost: 4717     Base: 2 2 5 2 2 2 2 2 2 5 2 2 7
c ---[ 230]---> Sorter-cost: 2097     Base: 2 2 5 2 5 2 2 2 2
c ---[ 228]---> Adder-cost: 509   maxlim: 3793490   bits: 23/22
c ---[ 226]---> Adder-cost: 987   maxlim: 613172   bits: 21/20
c ---[ 225]---> Sorter-cost:  151     Base: 2 2 2 2
c ---[ 224]---> BDD-cost:   25
c ---[ 222]---> Adder-cost: 1314   maxlim: 75093   bits: 18/17
c ---[ 221]---> Sorter-cost:  257     Base: 2 2 2 2 2
c ---[ 219]---> BDD-cost:    0
c ---[ 218]---> Sorter-cost: 1783     Base: 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  184     Base: 2 2 2 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 3491     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 213]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 212]---> Sorter-cost: 3491     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 211]---> Sorter-cost:  826     Base: 2 2 5 5 2 2 2 7 2
c ---[ 210]---> Sorter-cost:  129     Base: 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 2630     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 208]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost: 3232     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 206]---> Sorter-cost:  152     Base: 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost: 2992     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 203]---> Adder-cost: 532   maxlim: 600465   bits: 20/20
c ---[ 201]---> BDD-cost:    0
c ---[ 199]---> BDD-cost:    0
c ---[ 197]---> BDD-cost:    0
c ---[ 196]---> Sorter-cost: 1540     Base: 2 2 2 2 2 2
c ---[ 195]---> Adder-cost: 256   maxlim: 3973   bits: 13/12
c ---[ 194]---> BDD-cost:   49
c ---[ 192]---> BDD-cost:    0
c ---[ 190]---> Adder-cost: 1004   maxlim: 1807667   bits: 21/21
c ---[ 188]---> BDD-cost:    0
c ---[ 186]---> Sorter-cost: 2003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> BDD-cost:    0
c ---[ 182]---> Adder-cost: 548   maxlim: 1168488   bits: 21/21
c ---[ 180]---> Adder-cost: 370   maxlim: 893698   bits: 20/20
c ---[ 178]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> BDD-cost:   43
c ---[ 176]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> BDD-cost:  153
c ---[ 174]---> Sorter-cost:  198     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 3461     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 172]---> Sorter-cost: 1215     Base: 2 2 5 5 2 2 2
c ---[ 171]---> Sorter-cost: 4184     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[ 170]---> Sorter-cost: 4628     Base: 2 2 5 2 2 2 2 2 2 5 2 2 2 7
c ---[ 169]---> Sorter-cost: 3573     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 167]---> Adder-cost: 524   maxlim: 3870290   bits: 23/22
c ---[ 165]---> Adder-cost: 1138   maxlim: 2143860   bits: 23/22
c ---[ 164]---> Sorter-cost:  190     Base: 2 2 2 2 2
c ---[ 163]---> BDD-cost:   43
c ---[ 161]---> Adder-cost: 1441   maxlim: 97557   bits: 18/17
c ---[ 160]---> Sorter-cost:  320     Base: 2 2 2 2 2 2
c ---[ 158]---> Adder-cost: 144   maxlim: 2166   bits: 12/12
c ---[ 157]---> Sorter-cost: 2073     Base: 2 2 2 2 2 2 2 2 2
c ---[ 156]---> BDD-cost:    8
c ---[ 154]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost: 3461     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 152]---> Sorter-cost:  198     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost: 3573     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 150]---> Sorter-cost: 1141     Base: 2 2 5 2 5 2 7 2 2 2
c ---[ 149]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 3389     Base: 2 2 5 2 2 2 2 2 5 2 2
c ---[ 147]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 3389     Base: 2 2 5 2 2 2 2 2 5 2 2
c ---[ 145]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost: 3491     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 142]---> Adder-cost: 568   maxlim: 865041   bits: 20/20
c ---[ 140]---> Sorter-cost: 2649     Base: 2 2 3 2 2 2 2 2 2 2 2
c ---[ 138]---> Adder-cost: 856   maxlim: 179996   bits: 18/18
c ---[ 136]---> Adder-cost: 942   maxlim: 1130564   bits: 21/21
c ---[ 135]---> Adder-cost: 162   maxlim: 4348   bits: 13/13
c ---[ 134]---> Adder-cost: 288   maxlim: 7045   bits: 14/13
c ---[ 133]---> BDD-cost:   53
c ---[ 131]---> BDD-cost:    0
c ---[ 129]---> Adder-cost: 1100   maxlim: 2482515   bits: 22/22
c ---[ 127]---> Sorter-cost: 1292     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> Sorter-cost: 2252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Adder-cost: 1038   maxlim: 1203126   bits: 21/21
c ---[ 121]---> Adder-cost: 576   maxlim: 1368680   bits: 21/21
c ---[ 119]---> Adder-cost: 380   maxlim: 984322   bits: 21/20
c ---[ 117]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost:  106     Base: 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost:  349     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> BDD-cost:  153
c ---[ 113]---> BDD-cost:  153
c ---[ 112]---> Sorter-cost: 3477     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 111]---> Sorter-cost: 1638     Base: 2 2 5 5 2 2 2 2
c ---[ 110]---> Sorter-cost: 4754     Base: 2 2 5 2 2 2 2 2 2 5 2 2 7
c ---[ 109]---> Sorter-cost: 5285     Base: 2 2 5 2 2 2 2 2 2 5 2 2 2 7
c ---[ 108]---> Sorter-cost: 4677     Base: 2 2 5 2 2 2 2 2 2 5 2 2 2 7
c ---[ 106]---> Adder-cost: 540   maxlim: 3972690   bits: 23/22
c ---[ 104]---> Adder-cost: 1254   maxlim: 4289524   bits: 24/23
c ---[ 103]---> Sorter-cost:  219     Base: 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost:  106     Base: 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 1591   maxlim: 173141   bits: 19/18
c ---[  99]---> Sorter-cost:  382     Base: 2 2 2 2 2 2 2
c ---[  97]---> BDD-cost:    0
c ---[  96]---> Adder-cost: 212   maxlim: 15028   bits: 15/14
c ---[  95]---> BDD-cost:    5
c ---[  93]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost: 3832     Base: 2 2 5 2 2 2 2 2 5 2 2 2
c ---[  91]---> Sorter-cost:  198     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost: 3832     Base: 2 2 5 2 2 2 2 2 5 2 2 2
c ---[  89]---> Sorter-cost: 1811     Base: 2 2 5 2 2 5 2 2 7 2 2 2
c ---[  88]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 4207     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[  86]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 3595     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[  84]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost: 4207     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:   16
c ---[  80]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  171
c ---[  78]---> BDD-c/oldhome/oroussel/solvers/minisat+_script: line 9:  8691 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.66 0.89 0.96 2/54 8687
Raw data (stat): 8687 (runsolver) R 8686 20687 20686 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842077698 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+10.0009 s]
Raw data (loadavg): 0.71 0.90 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0018 s]
Raw data (loadavg): 0.76 0.90 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0012 s]
Raw data (loadavg): 0.79 0.90 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.82 0.91 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0008 s]
Raw data (loadavg): 0.85 0.91 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0012 s]
Raw data (loadavg): 0.87 0.91 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0009 s]
Raw data (loadavg): 0.89 0.91 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0009 s]
Raw data (loadavg): 0.91 0.92 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0013 s]
Raw data (loadavg): 0.92 0.92 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 0.93 0.92 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.94 0.92 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.001 s]
Raw data (loadavg): 0.95 0.92 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.001 s]
Raw data (loadavg): 0.96 0.93 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.96 0.93 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 0.97 0.93 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.97 0.93 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.105 s]
Raw data (loadavg): 0.98 0.93 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.104 s]
Raw data (loadavg): 0.98 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.104 s]
Raw data (loadavg): 0.98 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.206 s]
Raw data (loadavg): 0.98 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.206 s]
Raw data (loadavg): 0.99 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.207 s]
Raw data (loadavg): 0.99 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.207 s]
Raw data (loadavg): 0.99 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.207 s]
Raw data (loadavg): 0.99 0.94 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.211 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.212 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.213 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.214 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.216 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.216 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.217 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.217 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.217 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.217 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.216 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.217 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.217 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.216 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.217 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.217 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.217 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.217 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.216 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.216 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.216 s]
Raw data (loadavg): 0.99 0.96 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.225 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.224 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.222 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.222 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.223 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.222 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.222 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.222 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.221 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.221 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.221 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.22 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.22 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.22 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.22 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.22 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.22 s]
Raw data (loadavg): 1.07 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.22 s]
Raw data (loadavg): 1.06 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.219 s]
Raw data (loadavg): 1.05 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.219 s]
Raw data (loadavg): 1.04 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.219 s]
Raw data (loadavg): 1.03 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.218 s]
Raw data (loadavg): 1.03 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.219 s]
Raw data (loadavg): 1.02 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.219 s]
Raw data (loadavg): 1.02 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.218 s]
Raw data (loadavg): 1.02 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.218 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.218 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.217 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.225 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.67 s]
Raw data (loadavg): 1.00 0.99 0.97 1/53 8691
Raw data (stat): 8687 (minisat+_script) S 8686 20687 20686 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842077698 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.67
CPU time (s): 1229.85
CPU user time (s): 1228.69
CPU system time (s): 1.15882
CPU usage (%): 100.015
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####