PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp98ic.opb
MD5SUM	b6b40b25db69f63dc02649b5c9a3693a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	10894
Biggest coefficient in the objective function	1079902210
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	3040671454286
Number of bits of the sum of numbers in the objective function	42
Biggest number in a constraint	1079902210
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	3040671454286
Number of bits of the biggest sum of numbers	42
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	8.81066
Number of variables	10894
Total number of constraints	11719
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	11518
Number of constraints which are nor clauses,nor cardinality constraints	181
Minimum length of a constraint	1
Maximum length of a constraint	5038
Trace number 13855

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        479004 kB
Buffers:         34700 kB
Cached:         497936 kB
SwapCached:          8 kB
Active:         179644 kB
Inactive:       355784 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        478752 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14584 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:22:55 (client local time) WITH STATUS 0 IN 1200.89 SECONDS
stats: 20278 7 1200.89 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 825 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssss.ssssssss.ss.s..sssss..sssssssssssssssssssssssssssssssssss.sssss.s..sssssssssssssssssssssssssssss.ssssssss.sssss..s.s.s.sssssssssssssssssss.ssss.sssssssssssssssssssss
c ---[ 976]---> BDD-cost: 3578
c ---[ 970]---> Adder-cost: 2336   maxlim: 26   bits: 6/5
c ---[ 953]---> BDD-cost: 4629
c ---[ 942]---> Adder-cost: 5853   maxlim: 28   bits: 6/5
c ---[ 931]---> BDD-cost: 1386
c ---[ 912]---> BDD-cost: 1551
c ---[ 910]---> Adder-cost: 1275   maxlim: 21   bits: 6/5
c ---[ 872]---> BDD-cost:10452
c ---[ 866]---> BDD-cost:   21
c ---[ 865]---> BDD-cost: 1846
c ---[ 863]---> BDD-cost:   45
c ---[ 862]---> BDD-cost:   35
c ---[ 861]---> BDD-cost:   39
c ---[ 860]---> BDD-cost:   35
c ---[ 859]---> BDD-cost:   39
c ---[ 858]---> BDD-cost:   35
c ---[ 857]---> BDD-cost:   39
c ---[ 856]---> BDD-cost:   39
c ---[ 855]---> BDD-cost:   35
c ---[ 854]---> BDD-cost:   35
c ---[ 852]---> BDD-cost:   39
c ---[ 851]---> BDD-cost:   45
c ---[ 850]---> BDD-cost:   45
c ---[ 849]---> BDD-cost:   35
c ---[ 848]---> BDD-cost:   35
c ---[ 847]---> BDD-cost:   35
c ---[ 846]---> BDD-cost:   39
c ---[ 845]---> BDD-cost:   35
c ---[ 844]---> BDD-cost:   39
c ---[ 843]---> BDD-cost:   45
c ---[ 841]---> BDD-cost:   21
c ---[ 840]---> BDD-cost:   35
c ---[ 839]---> BDD-cost:   35
c ---[ 838]---> BDD-cost:   35
c ---[ 837]---> BDD-cost:   39
c ---[ 836]---> BDD-cost:   23
c ---[ 835]---> BDD-cost:   11
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   35
c ---[ 832]---> BDD-cost:   39
c ---[ 831]---> Adder-cost: 7378   maxlim: 4   bits: 4/3
c ---[ 830]---> BDD-cost:   35
c ---[ 829]---> BDD-cost:   39
c ---[ 828]---> BDD-cost:   35
c ---[ 827]---> BDD-cost:   39
c ---[ 826]---> BDD-cost:   29
c ---[ 825]---> BDD-cost:   19
c ---[ 824]---> BDD-cost:   29
c ---[ 823]---> BDD-cost:   23
c ---[ 822]---> BDD-cost:   13
c ---[ 821]---> BDD-cost:   39
c ---[ 819]---> BDD-cost:   29
c ---[ 818]---> BDD-cost:   29
c ---[ 817]---> BDD-cost:   39
c ---[ 816]---> BDD-cost:   15
c ---[ 815]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   19
c ---[ 813]---> BDD-cost:   29
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   29
c ---[ 810]---> BDD-cost:   29
c ---[ 808]---> BDD-cost:   39
c ---[ 807]---> BDD-cost:   39
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   29
c ---[ 804]---> BDD-cost:   29
c ---[ 803]---> BDD-cost:   35
c ---[ 802]---> BDD-cost:   39
c ---[ 801]---> BDD-cost:   29
c ---[ 800]---> BDD-cost:   15
c ---[ 799]---> BDD-cost:   13
c ---[ 797]---> BDD-cost:   25
c ---[ 796]---> BDD-cost:   29
c ---[ 795]---> BDD-cost:   29
c ---[ 794]---> BDD-cost:   35
c ---[ 793]---> BDD-cost:   39
c ---[ 792]---> BDD-cost:   29
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   23
c ---[ 789]---> BDD-cost:   35
c ---[ 788]---> BDD-cost:   39
c ---[ 786]---> BDD-cost:   29
c ---[ 785]---> BDD-cost:   25
c ---[ 784]---> BDD-cost:   29
c ---[ 783]---> BDD-cost:   39
c ---[ 782]---> BDD-cost:   23
c ---[ 781]---> BDD-cost:   23
c ---[ 780]---> BDD-cost:   29
c ---[ 779]---> BDD-cost:   29
c ---[ 778]---> BDD-cost:   25
c ---[ 777]---> BDD-cost:   29
c ---[ 776]---> BDD-cost:    0
c ---[ 775]---> BDD-cost:   35
c ---[ 774]---> BDD-cost:   39
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   39
c ---[ 771]---> BDD-cost:   29
c ---[ 770]---> BDD-cost:   29
c ---[ 769]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   39
c ---[ 767]---> BDD-cost:   25
c ---[ 766]---> BDD-cost:   45
c ---[ 765]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ---[ 764]---> BDD-cost:   23
c ---[ 763]---> BDD-cost:   13
c ---[ 762]---> BDD-cost:   23
c ---[ 761]---> BDD-cost:   45
c ---[ 760]---> BDD-cost:   45
c ---[ 759]---> BDD-cost:   13
c ---[ 758]---> BDD-cost:   45
c ---[ 757]---> BDD-cost:   21
c ---[ 756]---> BDD-cost:   45
c ---[ 755]---> BDD-cost:   45
c ---[ 753]---> BDD-cost: 3225
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   23
c ---[ 750]---> BDD-cost:   35
c ---[ 749]---> BDD-cost:   39
c ---[ 748]---> BDD-cost:   29
c ---[ 747]---> BDD-cost:   13
c ---[ 746]---> BDD-cost:   25
c ---[ 745]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:   39
c ---[ 743]---> BDD-cost:   23
c ---[ 742]---> BDD-cost: 1279
c ---[ 741]---> BDD-cost:   13
c ---[ 740]---> BDD-cost:   23
c ---[ 739]---> BDD-cost:   29
c ---[ 738]---> BDD-cost:   29
c ---[ 737]---> BDD-cost:   25
c ---[ 736]---> BDD-cost:   29
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   39
c ---[ 733]---> BDD-cost:   29
c ---[ 732]---> BDD-cost:   39
c ---[ 730]---> BDD-cost:   29
c ---[ 729]---> BDD-cost:   29
c ---[ 728]---> BDD-cost:   35
c ---[ 727]---> BDD-cost:   39
c ---[ 726]---> BDD-cost:   25
c ---[ 725]---> BDD-cost:   13
c ---[ 724]---> BDD-cost:   37
c ---[ 723]---> BDD-cost:   43
c ---[ 722]---> BDD-cost:   43
c ---[ 721]---> BDD-cost:   45
c ---[ 719]---> BDD-cost:   23
c ---[ 718]---> BDD-cost:   45
c ---[ 717]---> BDD-cost:   45
c ---[ 716]---> BDD-cost:   23
c ---[ 715]---> BDD-cost:   13
c ---[ 714]---> BDD-cost:   43
c ---[ 713]---> BDD-cost:   15
c ---[ 712]---> BDD-cost:   23
c ---[ 711]---> BDD-cost:   45
c ---[ 710]---> BDD-cost:   13
c ---[ 708]---> BDD-cost:   45
c ---[ 707]---> BDD-cost:   45
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   45
c ---[ 704]---> BDD-cost:   45
c ---[ 703]---> BDD-cost:   45
c ---[ 702]---> BDD-cost:   43
c ---[ 701]---> BDD-cost:   43
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   45
c ---[ 697]---> BDD-cost:   45
c ---[ 696]---> BDD-cost:   43
c ---[ 695]---> BDD-cost:   45
c ---[ 694]---> BDD-cost:   13
c ---[ 693]---> BDD-cost:   35
c ---[ 692]---> BDD-cost:   39
c ---[ 691]---> BDD-cost:   29
c ---[ 690]---> BDD-cost:   25
c ---[ 689]---> BDD-cost:   29
c ---[ 688]---> BDD-cost:   39
c ---[ 686]---> BDD-cost:   17
c ---[ 685]---> BDD-cost:   25
c ---[ 684]---> BDD-cost:   21
c ---[ 683]---> BDD-cost:   29
c ---[ 682]---> BDD-cost:   29
c ---[ 681]---> BDD-cost:    3
c ---[ 680]---> BDD-cost:   29
c ---[ 679]---> BDD-cost:   35
c ---[ 678]---> BDD-cost:   39
c ---[ 677]---> BDD-cost:   29
c ---[ 675]---> BDD-cost:   39
c ---[ 674]---> BDD-cost:   29
c ---[ 673]---> BDD-cost:   29
c ---[ 672]---> BDD-cost:   35
c ---[ 671]---> BDD-cost:   39
c ---[ 670]---> BDD-cost:    3
c ---[ 669]---> BDD-cost:   11
c ---[ 668]---> BDD-cost:   35
c ---[ 667]---> BDD-cost:   39
c ---[ 666]---> BDD-cost:   35
c ---[ 665]---> BDD-cost: 1030
c ---[ 664]---> BDD-cost:   39
c ---[ 663]---> BDD-cost:   39
c ---[ 662]---> BDD-cost:   35
c ---[ 661]---> BDD-cost:   39
c ---[ 660]---> BDD-cost:   19
c ---[ 659]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   39
c ---[ 657]---> BDD-cost:   19
c ---[ 656]---> BDD-cost:   35
c ---[ 655]---> BDD-cost:   39
c ---[ 654]---> Adder-cost: 1065   maxlim: 26   bits: 6/5
c ---[ 653]---> BDD-cost:   35
c ---[ 652]---> BDD-cost:   39
c ---[ 651]---> BDD-cost:   17
c ---[ 650]---> BDD-cost:   35
c ---[ 649]---> BDD-cost:   39
c ---[ 648]---> BDD-cost:    5
c ---[ 647]---> BDD-cost:   35
c ---[ 646]---> BDD-cost:   39
c ---[ 645]---> BDD-cost:   35
c ---[ 644]---> BDD-cost:   39
c ---[ 642]---> Adder-cost: 4843   maxlim: 4   bits: 4/3
c ---[ 641]---> BDD-cost:   39
c ---[ 640]---> BDD-cost:   35
c ---[ 639]---> BDD-cost:   39
c ---[ 638]---> BDD-cost:   35
c ---[ 637]---> BDD-cost:   35
c ---[ 636]---> BDD-cost:   35
c ---[ 635]---> BDD-cost:   39
c ---[ 634]---> BDD-cost:   35
c ---[ 633]---> BDD-cost:   35
c ---[ 632]---> BDD-cost:   39
c ---[ 630]---> BDD-cost:   35
c ---[ 629]---> BDD-cost:   35
c ---[ 628]---> BDD-cost:   39
c ---[ 627]---> BDD-cost:   35
c ---[ 625]---> BDD-cost:   35
c ---[ 624]---> BDD-cost:   39
c ---[ 623]---> BDD-cost:   17
c ---[ 622]---> BDD-cost:   35
c ---[ 621]---> BDD-cost:   39
c ---[ 619]---> BDD-cost:   35
c ---[ 618]---> BDD-cost:   39
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   35
c ---[ 615]---> BDD-cost:   39
c ---[ 614]---> BDD-cost:   35
c ---[ 613]---> BDD-cost:   39
c ---[ 612]---> BDD-cost:   35
c ---[ 611]---> BDD-cost:   39
c ---[ 610]---> BDD-cost:   13
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   39
c ---[ 606]---> BDD-cost:   19
c ---[ 605]---> BDD-cost:   35
c ---[ 604]---> BDD-cost:   35
c ---[ 603]---> BDD-cost:   43
c ---[ 602]---> BDD-cost:   35
c ---[ 601]---> BDD-cost:   39
c ---[ 600]---> BDD-cost:   19
c ---[ 599]---> BDD-cost:   35
c ---[ 597]---> BDD-cost:   35
c ---[ 596]---> BDD-cost:   39
c ---[ 595]---> BDD-cost:   19
c ---[ 594]---> BDD-cost:   43
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   35
c ---[ 591]---> BDD-cost:   17
c ---[ 590]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:   19
c ---[ 588]---> BDD-cost:   35
c ---[ 586]---> BDD-cost:   39
c ---[ 585]---> BDD-cost:   29
c ---[ 584]---> BDD-cost:   29
c ---[ 583]---> BDD-cost:   39
c ---[ 582]---> BDD-cost:   27
c ---[ 581]---> BDD-cost:   45
c ---[ 580]---> BDD-cost:   29
c ---[ 579]---> BDD-cost:   45
c ---[ 578]---> BDD-cost:   25
c ---[ 577]---> BDD-cost:   19
c ---[ 575]---> BDD-cost:   29
c ---[ 574]---> BDD-cost:   25
c ---[ 573]---> BDD-cost:   35
c ---[ 572]---> BDD-cost:   27
c ---[ 571]---> BDD-cost:   27
c ---[ 570]---> BDD-cost:   35
c ---[ 569]---> BDD-cost:   29
c ---[ 568]---> BDD-cost:   29
c ---[ 567]---> BDD-cost:    3
c ---[ 566]---> BDD-cost:   25
c ---[ 564]---> BDD-cost:   29
c ---[ 563]---> BDD-cost:   39
c ---[ 562]---> BDD-cost:   23
c ---[ 561]---> BDD-cost:    3
c ---[ 560]---> BDD-cost:   23
c ---[ 559]---> BDD-cost:   29
c ---[ 558]---> BDD-cost:   29
c ---[ 557]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:   29
c ---[ 555]---> BDD-cost:   35
c ---[ 553]---> BDD-cost:   39
c ---[ 552]---> BDD-cost:   29
c ---[ 551]---> BDD-cost:   39
c ---[ 550]---> BDD-cost:   29
c ---[ 549]---> BDD-cost:   29
c ---[ 548]---> BDD-cost:   35
c ---[ 547]---> BDD-cost:   39
c ---[ 546]---> BDD-cost:   25
c ---[ 545]---> BDD-cost:   35
c ---[ 544]---> BDD-cost:   39
c ---[ 542]---> BDD-cost:   45
c ---[ 541]---> BDD-cost:   45
c ---[ 540]---> BDD-cost:   35
c ---[ 539]---> BDD-cost:   35
c ---[ 538]---> BDD-cost:   35
c ---[ 537]---> BDD-cost:   39
c ---[ 536]---> BDD-cost:   35
c ---[ 535]---> BDD-cost:   39
c ---[ 534]---> BDD-cost:   35
c ---[ 533]---> BDD-cost:   39
c ---[ 532]---> BDD-cost:11348
c ---[ 531]---> BDD-cost: 6571
c ---[ 530]---> BDD-cost:   29
c ---[ 529]---> BDD-cost:   29
c ---[ 528]---> BDD-cost:   35
c ---[ 527]---> BDD-cost:   39
c ---[ 526]---> BDD-cost:   39
c ---[ 525]---> BDD-cost:   27
c ---[ 524]---> BDD-cost:   45
c ---[ 523]---> BDD-cost:   29
c ---[ 522]---> BDD-cost:   45
c ---[ 521]---> BDD-cost:   29
c ---[ 520]---> BDD-cost: 2592
c ---[ 519]---> BDD-cost:   19
c ---[ 518]---> BDD-cost:   43
c ---[ 517]---> BDD-cost:   29
c ---[ 516]---> BDD-cost:   19
c ---[ 515]---> BDD-cost:   35
c ---[ 514]---> BDD-cost:   27
c ---[ 513]---> BDD-cost:   45
c ---[ 512]---> BDD-cost:   45
c ---[ 511]---> BDD-cost:   19
c ---[ 510]---> BDD-cost:   21
c ---[ 508]---> BDD-cost:    9
c ---[ 507]---> BDD-cost:   35
c ---[ 506]---> BDD-cost:   29
c ---[ 505]---> BDD-cost:   25
c ---[ 504]---> BDD-cost:   39
c ---[ 503]---> BDD-cost:   29
c ---[ 502]---> BDD-cost:   29
c ---[ 501]---> BDD-cost:   39
c ---[ 500]---> BDD-cost:   23
c ---[ 499]---> BDD-cost:   23
c ---[ 497]---> BDD-cost:   29
c ---[ 496]---> BDD-cost:   25
c ---[ 495]---> BDD-cost:   29
c ---[ 494]---> BDD-cost:   29
c ---[ 493]---> BDD-cost:   39
c ---[ 492]---> BDD-cost:   39
c ---[ 491]---> BDD-cost:   25
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   29
c ---[ 488]---> BDD-cost:   35
c ---[ 486]---> BDD-cost:   39
c ---[ 485]---> BDD-cost:   29
c ---[ 484]---> BDD-cost:   39
c ---[ 483]---> BDD-cost:   23
c ---[ 482]---> BDD-cost:   25
c ---[ 481]---> BDD-cost:   25
c ---[ 480]---> BDD-cost:   29
c ---[ 479]---> BDD-cost:   29
c ---[ 478]---> BDD-cost:   29
c ---[ 477]---> BDD-cost:   35
c ---[ 475]---> BDD-cost:   39
c ---[ 474]---> BDD-cost:   29
c ---[ 473]---> BDD-cost:   25
c ---[ 472]---> BDD-cost:   39
c ---[ 471]---> BDD-cost:   29
c ---[ 470]---> BDD-cost:   29
c ---[ 469]---> BDD-cost:   39
c ---[ 468]---> BDD-cost:   17
c ---[ 467]---> BDD-cost:   25
c ---[ 466]---> BDD-cost:   21
c ---[ 465]---> BDD-cost:10772
c ---[ 464]---> BDD-cost:   29
c ---[ 463]---> BDD-cost:    5
c ---[ 462]---> BDD-cost:   29
c ---[ 461]---> BDD-cost:   29
c ---[ 460]---> BDD-cost:   39
c ---[ 459]---> BDD-cost:   39
c ---[ 458]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:   29
c ---[ 456]---> BDD-cost:   29
c ---[ 455]---> BDD-cost:   35
c ---[ 453]---> BDD-cost:   39
c ---[ 452]---> BDD-cost:   29
c ---[ 451]---> BDD-cost:   39
c ---[ 450]---> BDD-cost:   17
c ---[ 449]---> BDD-cost:   13
c ---[ 448]---> BDD-cost:   25
c ---[ 447]---> BDD-cost:   29
c ---[ 446]---> BDD-cost:   29
c ---[ 445]---> BDD-cost:   29
c ---[ 444]---> BDD-cost:   35
c ---[ 442]---> BDD-cost:   39
c ---[ 441]---> BDD-cost:   29
c ---[ 440]---> BDD-cost:    5
c ---[ 439]---> BDD-cost:   39
c ---[ 438]---> BDD-cost:   29
c ---[ 437]---> BDD-cost:   35
c ---[ 436]---> BDD-cost:   39
c ---[ 435]---> BDD-cost:   39
c ---[ 434]---> BDD-cost:   27
c ---[ 433]---> BDD-cost:   39
c ---[ 431]---> BDD-cost:   29
c ---[ 430]---> BDD-cost:   35
c ---[ 429]---> BDD-cost:   39
c ---[ 428]---> BDD-cost:   39
c ---[ 427]---> BDD-cost:   35
c ---[ 426]---> BDD-cost:   35
c ---[ 425]---> BDD-cost:   39
c ---[ 424]---> BDD-cost:   19
c ---[ 423]---> BDD-cost:   35
c ---[ 422]---> BDD-cost:   39
c ---[ 419]---> BDD-cost:   35
c ---[ 418]---> BDD-cost:   39
c ---[ 417]---> BDD-cost:   29
c ---[ 416]---> BDD-cost:   29
c ---[ 415]---> BDD-cost:   39
c ---[ 414]---> BDD-cost:   39
c ---[ 413]---> BDD-cost:   27
c ---[ 412]---> BDD-cost:   29
c ---[ 411]---> BDD-cost:   39
c ---[ 410]---> BDD-cost:   39
c ---[ 408]---> BDD-cost:   29
c ---[ 407]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   39
c ---[ 405]---> BDD-cost:   29
c ---[ 404]---> BDD-cost:   39
c ---[ 403]---> BDD-cost:   39
c ---[ 402]---> BDD-cost:   29
c ---[ 401]---> BDD-cost:   35
c ---[ 400]---> BDD-cost:   39
c ---[ 399]---> BDD-cost:   39
c ---[ 397]---> BDD-cost:   29
c ---[ 396]---> BDD-cost:   39
c ---[ 395]---> BDD-cost:   39
c ---[ 394]---> BDD-cost:   29
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:   39
c ---[ 391]---> BDD-cost:   27
c ---[ 390]---> BDD-cost:   39
c ---[ 389]---> BDD-cost:   39
c ---[ 388]---> BDD-cost:   29
c ---[ 386]---> BDD-cost:   29
c ---[ 385]---> BDD-cost:   39
c ---[ 384]---> BDD-cost:   23
c ---[ 383]---> BDD-cost:   45
c ---[ 382]---> BDD-cost:   17
c ---[ 381]---> BDD-cost:   45
c ---[ 380]---> BDD-cost:   45
c ---[ 379]---> BDD-cost:   17
c ---[ 378]---> BDD-cost:   45
c ---[ 377]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   45
c ---[ 374]---> BDD-cost:   45
c ---[ 373]---> BDD-cost:   45
c ---[ 372]---> BDD-cost:   45
c ---[ 371]---> BDD-cost:   45
c ---[ 370]---> BDD-cost:   17
c ---[ 369]---> BDD-cost:   23
c ---[ 368]---> BDD-cost:   29
c ---[ 367]---> BDD-cost:   25
c ---[ 366]---> BDD-cost:   29
c ---[ 365]---> BDD-cost:11754
c ---[ 364]---> BDD-cost:   29
c ---[ 363]---> BDD-cost:   39
c ---[ 362]---> BDD-cost:   39
c ---[ 361]---> BDD-cost:   25
c ---[ 360]---> BDD-cost:   29
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   39
c ---[ 356]---> BDD-cost:   29
c ---[ 355]---> BDD-cost:   39
c ---[ 353]---> BDD-cost:   23
c ---[ 352]---> BDD-cost:   25
c ---[ 351]---> BDD-cost:   25
c ---[ 350]---> BDD-cost:   29
c ---[ 349]---> BDD-cost:   29
c ---[ 348]---> BDD-cost:   29
c ---[ 347]---> BDD-cost:   35
c ---[ 346]---> BDD-cost:   39
c ---[ 345]---> BDD-cost:   29
c ---[ 344]---> BDD-cost:   25
c ---[ 342]---> BDD-cost:   45
c ---[ 341]---> BDD-cost:   21
c ---[ 340]---> BDD-cost:   45
c ---[ 339]---> BDD-cost:   45
c ---[ 338]---> BDD-cost:   21
c ---[ 337]---> BDD-cost:   45
c ---[ 336]---> BDD-cost:   45
c ---[ 335]---> BDD-cost:   45
c ---[ 334]---> BDD-cost:   45
c ---[ 333]---> BDD-cost:   45
c ---[ 331]---> BDD-cost:   45
c ---[ 330]---> BDD-cost:   45
c ---[ 329]---> BDD-cost:   21
c ---[ 328]---> BDD-cost:   21
c ---[ 327]---> BDD-cost:   29
c ---[ 326]---> BDD-cost:   21
c ---[ 325]---> BDD-cost:   35
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   23
c ---[ 322]---> BDD-cost:   35
c ---[ 320]---> BDD-cost:   29
c ---[ 319]---> BDD-cost:   29
c ---[ 318]---> BDD-cost:   29
c ---[ 317]---> BDD-cost:   29
c ---[ 316]---> BDD-cost:   35
c ---[ 315]---> BDD-cost:   39
c ---[ 314]---> BDD-cost:   29
c ---[ 313]---> BDD-cost:   39
c ---[ 312]---> BDD-cost:   29
c ---[ 311]---> BDD-cost:   29
c ---[ 310]---> BDD-cost: 7190
c ---[ 308]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   39
c ---[ 305]---> BDD-cost:   19
c ---[ 304]---> BDD-cost:   43
c ---[ 303]---> BDD-cost:   29
c ---[ 302]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   45
c ---[ 295]---> BDD-cost:   45
c ---[ 294]---> BDD-cost:   23
c ---[ 293]---> BDD-cost:   25
c ---[ 292]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   29
c ---[ 289]---> BDD-cost:   29
c ---[ 288]---> BDD-cost:   19
c ---[ 287]---> BDD-cost: 2951
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:   35
c ---[ 284]---> BDD-cost:   27
c ---[ 283]---> BDD-cost:   39
c ---[ 282]---> BDD-cost:   45
c ---[ 281]---> BDD-cost:   45
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:   19
c ---[ 278]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   29
c ---[ 274]---> BDD-cost:   39
c ---[ 273]---> BDD-cost:   39
c ---[ 272]---> BDD-cost:   43
c ---[ 271]---> BDD-cost:   43
c ---[ 270]---> BDD-cost:   43
c ---[ 269]---> BDD-cost:   43
c ---[ 268]---> BDD-cost:   39
c ---[ 267]---> BDD-cost:   39
c ---[ 266]---> BDD-cost:   29
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   35
c ---[ 262]---> BDD-cost:   39
c ---[ 261]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:   39
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   13
c ---[ 257]---> BDD-cost:   25
c ---[ 256]---> BDD-cost:   29
c ---[ 255]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   29
c ---[ 252]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   39
c ---[ 250]---> BDD-cost:   29
c ---[ 248]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 246]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   29
c ---[ 244]---> BDD-cost:   45
c ---[ 242]---> BDD-cost:   45
c ---[ 241]---> BDD-cost:   23
c ---[ 240]---> BDD-cost:   25
c ---[ 239]---> BDD-cost:   35
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   29
c ---[ 236]---> BDD-cost:   35
c ---[ 235]---> BDD-cost:   35
c ---[ 234]---> BDD-cost:   39
c ---[ 233]---> BDD-cost:   35
c ---[ 231]---> BDD-cost:   39
c ---[ 230]---> BDD-cost:   45
c ---[ 229]---> BDD-cost:   45
c ---[ 228]---> BDD-cost:   35
c ---[ 227]---> BDD-cost:   35
c ---[ 226]---> BDD-cost:   35
c ---[ 225]---> BDD-cost:   35
c ---[ 224]---> BDD-cost:   39
c ---[ 223]---> BDD-cost:   35
c ---[ 222]---> BDD-cost:   29
c ---[ 220]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   25
c ---[ 218]---> BDD-cost:   35
c ---[ 217]---> BDD-cost:   29
c ---[ 216]---> BDD-cost:   35
c ---[ 215]---> BDD-cost:   43
c ---[ 214]---> BDD-cost:   35
c ---[ 213]---> BDD-cost:   35
c ---[ 212]---> BDD-cost:   39
c ---[ 211]---> BDD-cost:    5
c ---[ 209]---> BDD-cost:   35
c ---[ 208]---> BDD-cost:   39
c ---[ 207]---> BDD-cost:   43
c ---[ 206]---> BDD-cost:   35
c ---[ 205]---> BDD-cost:   29
c ---[ 204]---> BDD-cost:   11
c ---[ 203]---> BDD-cost:   35
c ---[ 202]---> BDD-cost:   27
c ---[ 201]---> BDD-cost:   35
c ---[ 200]---> BDD-cost:   35
c ---[ 199]---> BDD-cost: 7370
c ---[ 197]---> BDD-cost:   29
c ---[ 196]---> BDD-cost:   29
c ---[ 195]---> BDD-cost:   39
c ---[ 194]---> BDD-cost:   45
c ---[ 193]---> BDD-cost:   45
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   45
c ---[ 190]---> BDD-cost:   43
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   25
c ---[ 186]---> BDD-cost:   23
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   35
c ---[ 183]---> BDD-cost:   29
c ---[ 182]---> BDD-cost:   27
c ---[ 181]---> BDD-cost:   35
c ---[ 180]---> BDD-cost:   39
c ---[ 179]---> BDD-cost:   23
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   35
c ---[ 176]---> Adder-cost: 14905   maxlim: 25   bits: 6/5
c ---[ 175]---> BDD-cost:   25
c ---[ 174]---> BDD-cost:   29
c ---[ 173]---> BDD-cost:   35
c ---[ 172]---> BDD-cost:   35
c ---[ 171]---> BDD-cost:   39
c ---[ 170]---> BDD-cost:   29
c ---[ 169]---> Adder-cost: 4078   maxlim: 22   bits: 6/5
c ---[ 162]---> BDD-cost: 8628
c ---[ 155]---> Adder-cost: 6350   maxlim: 28   bits: 6/5
c ---[ 151]---> BDD-cost:  512
c ---[ 150]---> BDD-cost: 2589
c ---[ 149]---> Adder-cost: 3452   maxlim: 22   bits: 6/5
c ---[ 148]---> BDD-cost: 2014
c ---[ 147]---> Adder-cost: 7393   maxlim: 13   bits: 5/4
c ---[ 146]---> BDD-cost: 4198
c ---[ 145]---> BDD-cost: 7632
c ---[ 144]---> BDD-cost: 2670
c ---[ 143]---> BDD-cost:  218
c ---[ 142]---> BDD-cost:  267
c ---[ 141]---> BDD-cost:  172
c ---[ 140]---> BDD-cost:  156
c ---[ 139]---> BDD-cost:  906
c ---[ 138]---> BDD-cost: 2278
c ---[ 137]---> BDD-cost: 1528
c ---[ 136]---> BDD-cost: 5832
c ---[ 135]---> BDD-cost:   62
c ---[ 134]---> BDD-cost:  252
c ---[ 133]---> BDD-cost:  188
c ---[ 132]---> BDD-cost: 1184
c ---[ 131]---> BDD-cost:  718
c ---[ 130]---> BDD-cost: 1100
c ---[ 129]---> BDD-cost: 2508
c ---[ 128]---> BDD-cost: 1150
c ---[ 127]---> BDD-cost: 3936
c ---[ 126]---> BDD-cost:   42
c ---[ 125]---> BDD-cost:   84
c ---[ 124]---> BDD-cost:  260
c ---[ 123]---> BDD-cost: 3116
c ---[ 122]---> BDD-cost: 4948
c ---[ 121]---> BDD-cost:  677
c ---[ 120]---> BDD-cost: 6103
c ---[ 119]---> BDD-cost: 1076
c ---[ 118]---> BDD-cost:  877
c ---[ 117]---> BDD-cost:  925
c ---[ 116]---> BDD-cost: 5587
c ---[ 115]---> BDD-cost: 3737
c ---[ 114]---> BDD-cost: 6970
c ---[ 113]---> BDD-cost:  750
c ---[ 112]---> BDD-cost: 3897
c ---[ 111]---> BDD-cost:  516
c ---[ 110]---> BDD-cost: 1813
c ---[ 109]---> BDD-cost: 1320
c ---[ 108]---> BDD-cost: 2942
c ---[ 107]---> BDD-cost: 2610
c ---[ 106]---> BDD-cost:  795
c ---[ 105]---> BDD-cost: 4397
c ---[ 104]---> BDD-cost: 1303
c ---[ 103]---> BDD-cost: 4943
c ---[ 102]---> BDD-cost: 1194
c ---[ 101]---> BDD-cost: 4333
c ---[ 100]---> BDD-cost:  437
c ---[  99]---> BDD-cost:  250
c ---[  98]---> BDD-cost: 7832
c ---[  97]---> Adder-cost: 12966   maxlim: 17   bits: 6/5
c ---[  96]---> BDD-cost: 5415
c ---[  95]---> Adder-cost: 2316   maxlim: 21   bits: 6/5
c ---[  94]---> BDD-cost:  234
c ---[  93]---> BDD-cost:  212
c ---[  92]---> BDD-cost: 4374
c ---[  91]---> BDD-cost:  732
c ---[  90]---> BDD-cost: 2076
c ---[  89]---> BDD-cost:  286
c ---[  88]---> BDD-cost: 2622
c ---[  87]---> BDD-cost:  382
c ---[  86]---> BDD-cost: 2248
c ---[  85]---> BDD-cost: 5404
c ---[  84]---> BDD-cost:  854
c ---[  83]---> BDD-cost: 7887
c ---[  82]---> BDD-cost:  991
c ---[  81]---> BDD-cost: 4578
c ---[  80]---> BDD-cost:  607
c ---[  79]---> BDD-cost:  217
c ---[  78]---> BDD-cost: 1449
c ---[  77]---> BDD-cost: 1048
c ---[  76]---> BDD-cost:  862
c ---[  75]---> BDD-cost: 1956
c ---[  74]---> BDD-cost: 5181
c ---[  73]---> BDD-cost:  458
c ---[  72]---> BDD-cost:   98
c ---[  71]---> BDD-cost: 3438
c ---[  70]---> BDD-cost:  878
c ---[  69]---> BDD-cost:  728
c ---[  68]---> BDD-cost: 1368
c ---[  67]---> BDD-cost: 4240
c ---[  66]---> BDD-cost: 4764
c ---[  65]---> BDD-cost: 2522
c ---[  64]---> BDD-cost: 2730
c ---[  63]---> BDD-cost: 1097
c ---[  62]---> BDD-cost:  875
c ---[  61]---> BDD-cost:  776
c ---[  60]---> BDD-cost: 2126
c ---[  59]---> BDD-cost: 1226
c ---[  58]---> BDD-cost: 1144
c ---[  57]---> BDD-cost:  334
c ---[  56]---> BDD-cost:  750
c ---[  55]---> BDD-cost:  146
c ---[  54]---> BDD-cost:  206
c ---[  53]---> BDD-cost: 2832
c ---[  52]---> BDD-cost: 8880
c ---[  51]---> BDD-cost:  192
c ---[  50]---> BDD-cost: 2964
c ---[  49]---> Adder-cost: 8882   maxlim: 20   bits: 6/5
c ---[  48]---> BDD-cost:    1
c ---[  47]---> Adder-cost: 7973   maxlim: 20   bits: 6/5
c ---[  46]---> BDD-cost:   80
c ---[  45]---> BDD-cost:  238
c ---[  44]---> BDD-cost:   88
c ---[  43]---> BDD-cost:  136
c ---[  42]---> BDD-cost: 4262
c ---[  41]---> BDD-cost:10085
c ---[  40]---> BDD-cost:  968
c ---[  39]---> BDD-cost:  921
c ---[  38]---> BDD-cost: 2472
c ---[ #### 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.83 0.94 0.90 2/54 29073
Raw data (stat): 29073 (runsolver) R 29072 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481665646 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0004 s]
Raw data (loadavg): 0.86 0.94 0.90 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 17572 0 0 0 953 45 0 0 25 0 1 0 481665646 62672896 13769 4294967295 134512640 134672761 3221224544 3221222480 134522981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15301 13769 603 41 0 15260 0
vsize: 61204
[startup+20.0008 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 59629 0 0 0 1847 152 0 0 25 0 1 0 481665646 252387328 55530 4294967295 134512640 134672761 3221224544 3220666016 134604223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61618 55530 603 41 0 61577 0
vsize: 246472
[startup+30.0004 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 86429 0 0 0 2777 221 0 0 25 0 1 0 481665646 399683584 82328 4294967295 134512640 134672761 3221224544 3221223088 134621173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 97579 82328 603 41 0 97538 0
vsize: 390316
[startup+40.0006 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 86429 0 0 0 3777 221 0 0 25 0 1 0 481665646 399683584 82328 4294967295 134512640 134672761 3221224544 3221223152 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 97579 82328 603 41 0 97538 0
vsize: 390316
[startup+50.0009 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 86429 0 0 0 4777 221 0 0 25 0 1 0 481665646 399683584 82328 4294967295 134512640 134672761 3221224544 3221223088 134621247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 97579 82328 603 41 0 97538 0
vsize: 390316
[startup+60.0006 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 91222 0 0 0 5761 238 0 0 25 0 1 0 481665646 410972160 84572 4294967295 134512640 134672761 3221224544 3221222960 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100335 84573 603 41 0 100294 0
vsize: 401340
[startup+70.0009 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 93865 0 0 0 6746 252 0 0 25 0 1 0 481665646 421879808 87215 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 102998 87215 603 41 0 102957 0
vsize: 411992
[startup+80.0012 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 96125 0 0 0 7731 268 0 0 25 0 1 0 481665646 431280128 89475 4294967295 134512640 134672761 3221224544 3221222668 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 105293 89475 603 41 0 105252 0
vsize: 421172
[startup+90.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 98074 0 0 0 8722 276 0 0 25 0 1 0 481665646 439689216 91424 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 107346 91424 603 41 0 107305 0
vsize: 429384
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 99510 0 0 0 9715 284 0 0 25 0 1 0 481665646 445796352 92860 4294967295 134512640 134672761 3221224544 3221222896 134604055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 108837 92860 603 41 0 108796 0
vsize: 435348
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 101447 0 0 0 10705 294 0 0 25 0 1 0 481665646 453931008 94797 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110823 94797 603 41 0 110782 0
vsize: 443292
[startup+120.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 102391 0 0 0 11699 300 0 0 25 0 1 0 481665646 457846784 95741 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111779 95741 603 41 0 111738 0
vsize: 447116
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 103592 0 0 0 12692 307 0 0 25 0 1 0 481665646 462716928 96942 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112968 96942 603 41 0 112927 0
vsize: 451872
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 105181 0 0 0 13684 315 0 0 25 0 1 0 481665646 469012480 98531 4294967295 134512640 134672761 3221224544 3221221936 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114505 98531 603 41 0 114464 0
vsize: 458020
[startup+150.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 106392 0 0 0 14677 322 0 0 25 0 1 0 481665646 474497024 99742 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115844 99742 603 41 0 115803 0
vsize: 463376
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 107456 0 0 0 15672 327 0 0 25 0 1 0 481665646 479805440 100806 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117140 100806 603 41 0 117099 0
vsize: 468560
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 108427 0 0 0 16667 331 0 0 25 0 1 0 481665646 484376576 101777 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118256 101777 603 41 0 118215 0
vsize: 473024
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 109402 0 0 0 17663 336 0 0 25 0 1 0 481665646 488402944 102752 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119239 102752 603 41 0 119198 0
vsize: 476956
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 110322 0 0 0 18658 341 0 0 25 0 1 0 481665646 492257280 103672 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120180 103672 603 41 0 120139 0
vsize: 480720
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 111171 0 0 0 19654 345 0 0 25 0 1 0 481665646 495927296 104521 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121076 104521 603 41 0 121035 0
vsize: 484304
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 112078 0 0 0 20648 351 0 0 25 0 1 0 481665646 499740672 105428 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122007 105428 603 41 0 121966 0
vsize: 488028
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 112809 0 0 0 21645 355 0 0 25 0 1 0 481665646 502796288 106159 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122753 106159 603 41 0 122712 0
vsize: 491012
[startup+230.029 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 113601 0 0 0 22643 359 0 0 25 0 1 0 481665646 506056704 106951 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123549 106951 603 41 0 123508 0
vsize: 494196
[startup+240.028 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 114367 0 0 0 23640 362 0 0 25 0 1 0 481665646 509472768 107717 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124383 107717 603 41 0 124342 0
vsize: 497532
[startup+250.029 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 115036 0 0 0 24636 366 0 0 25 0 1 0 481665646 512684032 108386 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125167 108386 603 41 0 125126 0
vsize: 500668
[startup+260.054 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 115743 0 0 0 25636 369 0 0 25 0 1 0 481665646 516227072 109093 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126032 109093 603 41 0 125991 0
vsize: 504128
[startup+270.054 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 116505 0 0 0 26633 372 0 0 25 0 1 0 481665646 519761920 109855 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126895 109855 603 41 0 126854 0
vsize: 507580
[startup+280.059 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 117191 0 0 0 27630 376 0 0 25 0 1 0 481665646 523108352 110541 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 127712 110541 603 41 0 127671 0
vsize: 510848
[startup+290.065 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 117799 0 0 0 28628 379 0 0 25 0 1 0 481665646 525991936 111149 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128416 111149 603 41 0 128375 0
vsize: 513664
[startup+300.065 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 118405 0 0 0 29624 382 0 0 25 0 1 0 481665646 528916480 111755 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129130 111755 603 41 0 129089 0
vsize: 516520
[startup+310.065 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 118999 0 0 0 30621 384 0 0 25 0 1 0 481665646 531656704 112349 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129799 112349 603 41 0 129758 0
vsize: 519196
[startup+320.064 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 119613 0 0 0 31618 388 0 0 25 0 1 0 481665646 534667264 112963 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130534 112963 603 41 0 130493 0
vsize: 522136
[startup+330.065 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 120214 0 0 0 32615 391 0 0 25 0 1 0 481665646 537276416 113564 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131171 113564 603 41 0 131130 0
vsize: 524684
[startup+340.065 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 120843 0 0 0 33612 394 0 0 25 0 1 0 481665646 540123136 114193 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131866 114193 603 41 0 131825 0
vsize: 527464
[startup+350.07 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 121479 0 0 0 34609 397 0 0 25 0 1 0 481665646 542867456 114829 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132536 114829 603 41 0 132495 0
vsize: 530144
[startup+360.073 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 122075 0 0 0 35607 400 0 0 25 0 1 0 481665646 545357824 115425 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133144 115425 603 41 0 133103 0
vsize: 532576
[startup+370.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 122750 0 0 0 36604 402 0 0 25 0 1 0 481665646 548220928 116100 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133843 116100 603 41 0 133802 0
vsize: 535372
[startup+380.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 123396 0 0 0 37602 405 0 0 25 0 1 0 481665646 551202816 116746 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134571 116746 603 41 0 134530 0
vsize: 538284
[startup+390.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 123978 0 0 0 38600 407 0 0 25 0 1 0 481665646 553517056 117328 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135136 117328 603 41 0 135095 0
vsize: 540544
[startup+400.087 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 124584 0 0 0 39599 410 0 0 25 0 1 0 481665646 556064768 117934 4294967295 134512640 134672761 3221224544 3221222960 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135758 117934 603 41 0 135717 0
vsize: 543032
[startup+410.089 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 125112 0 0 0 40597 412 0 0 25 0 1 0 481665646 558358528 118462 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136318 118462 603 41 0 136277 0
vsize: 545272
[startup+420.088 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 125631 0 0 0 41595 414 0 0 25 0 1 0 481665646 560656384 118981 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136879 118981 603 41 0 136838 0
vsize: 547516
[startup+430.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 126238 0 0 0 42593 416 0 0 25 0 1 0 481665646 563449856 119588 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137561 119588 603 41 0 137520 0
vsize: 550244
[startup+440.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 126900 0 0 0 43591 418 0 0 25 0 1 0 481665646 566644736 120250 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138341 120250 603 41 0 138300 0
vsize: 553364
[startup+450.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 127497 0 0 0 44588 421 0 0 25 0 1 0 481665646 569278464 120847 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138984 120847 603 41 0 138943 0
vsize: 555936
[startup+460.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 128061 0 0 0 45586 424 0 0 25 0 1 0 481665646 571789312 121411 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139597 121411 603 41 0 139556 0
vsize: 558388
[startup+470.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 128628 0 0 0 46584 426 0 0 25 0 1 0 481665646 574521344 121978 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140264 121978 603 41 0 140223 0
vsize: 561056
[startup+480.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 129213 0 0 0 47581 428 0 0 25 0 1 0 481665646 576827392 122563 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140827 122563 603 41 0 140786 0
vsize: 563308
[startup+490.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 129852 0 0 0 48579 431 0 0 25 0 1 0 481665646 579833856 123202 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141561 123202 603 41 0 141520 0
vsize: 566244
[startup+500.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 130446 0 0 0 49576 434 0 0 25 0 1 0 481665646 582455296 123796 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142201 123796 603 41 0 142160 0
vsize: 568804
[startup+510.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 131029 0 0 0 50573 436 0 0 25 0 1 0 481665646 584986624 124379 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142819 124379 603 41 0 142778 0
vsize: 571276
[startup+520.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 131558 0 0 0 51571 438 0 0 25 0 1 0 481665646 587517952 124908 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143437 124908 603 41 0 143396 0
vsize: 573748
[startup+530.095 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 132165 0 0 0 52570 441 0 0 25 0 1 0 481665646 590213120 125515 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144095 125515 603 41 0 144054 0
vsize: 576380
[startup+540.099 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 132745 0 0 0 53569 442 0 0 25 0 1 0 481665646 592564224 126095 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144669 126095 603 41 0 144628 0
vsize: 578676
[startup+550.099 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 133277 0 0 0 54566 444 0 0 25 0 1 0 481665646 595030016 126627 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145271 126627 603 41 0 145230 0
vsize: 581084
[startup+560.098 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 133857 0 0 0 55564 446 0 0 25 0 1 0 481665646 597770240 127207 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145940 127207 603 41 0 145899 0
vsize: 583760
[startup+570.098 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 134368 0 0 0 56563 448 0 0 25 0 1 0 481665646 600055808 127718 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146498 127718 603 41 0 146457 0
vsize: 585992
[startup+580.099 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 134896 0 0 0 57561 450 0 0 25 0 1 0 481665646 602431488 128246 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147078 128246 603 41 0 147037 0
vsize: 588312
[startup+590.099 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 135488 0 0 0 58559 453 0 0 25 0 1 0 481665646 605102080 128838 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147730 128838 603 41 0 147689 0
vsize: 590920
[startup+600.099 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 136033 0 0 0 59556 455 0 0 25 0 1 0 481665646 607653888 129383 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148353 129383 603 41 0 148312 0
vsize: 593412
[startup+610.101 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 136530 0 0 0 60555 457 0 0 25 0 1 0 481665646 609759232 129880 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148867 129880 603 41 0 148826 0
vsize: 595468
[startup+620.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 137040 0 0 0 61553 459 0 0 25 0 1 0 481665646 611983360 130390 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149410 130390 603 41 0 149369 0
vsize: 597640
[startup+630.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 137516 0 0 0 62551 461 0 0 25 0 1 0 481665646 613867520 130866 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149870 130866 603 41 0 149829 0
vsize: 599480
[startup+640.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 138021 0 0 0 63549 463 0 0 25 0 1 0 481665646 616185856 131371 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150436 131371 603 41 0 150395 0
vsize: 601744
[startup+650.101 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 138487 0 0 0 64546 466 0 0 25 0 1 0 481665646 618352640 131837 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150965 131837 603 41 0 150924 0
vsize: 603860
[startup+660.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 138931 0 0 0 65544 467 0 0 25 0 1 0 481665646 620126208 132281 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151398 132281 603 41 0 151357 0
vsize: 605592
[startup+670.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 139406 0 0 0 66543 469 0 0 25 0 1 0 481665646 622231552 132756 4294967295 134512640 134672761 3221224544 3221222896 134604682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151912 132756 603 41 0 151871 0
vsize: 607648
[startup+680.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 139884 0 0 0 67541 471 0 0 25 0 1 0 481665646 624484352 133234 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152462 133234 603 41 0 152421 0
vsize: 609848
[startup+690.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 140365 0 0 0 68538 474 0 0 25 0 1 0 481665646 626552832 133715 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152967 133715 603 41 0 152926 0
vsize: 611868
[startup+700.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 140783 0 0 0 69536 476 0 0 25 0 1 0 481665646 628314112 134133 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153397 134133 603 41 0 153356 0
vsize: 613588
[startup+710.101 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 141240 0 0 0 70535 478 0 0 25 0 1 0 481665646 630288384 134590 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153879 134590 603 41 0 153838 0
vsize: 615516
[startup+720.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 141659 0 0 0 71532 480 0 0 25 0 1 0 481665646 632061952 135009 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154312 135009 603 41 0 154271 0
vsize: 617248
[startup+730.102 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 142127 0 0 0 72530 482 0 0 25 0 1 0 481665646 634187776 135477 4294967295 134512640 134672761 3221224544 3221222896 134604645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154831 135477 603 41 0 154790 0
vsize: 619324
[startup+740.101 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 142531 0 0 0 73529 484 0 0 25 0 1 0 481665646 635973632 135881 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155267 135881 603 41 0 155226 0
vsize: 621068
[startup+750.416 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 142941 0 0 0 74559 486 0 0 25 0 1 0 481665646 637808640 136291 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155715 136291 603 41 0 155674 0
vsize: 622860
[startup+760.416 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 143387 0 0 0 75557 488 0 0 25 0 1 0 481665646 639782912 136737 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156197 136737 603 41 0 156156 0
vsize: 624788
[startup+770.415 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 143806 0 0 0 76555 490 0 0 25 0 1 0 481665646 641716224 137156 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156669 137156 603 41 0 156628 0
vsize: 626676
[startup+780.416 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 144268 0 0 0 77553 492 0 0 25 0 1 0 481665646 643817472 137618 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157182 137618 603 41 0 157141 0
vsize: 628728
[startup+790.416 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 144686 0 0 0 78551 494 0 0 25 0 1 0 481665646 645500928 138036 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157593 138036 603 41 0 157552 0
vsize: 630372
[startup+800.416 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 145149 0 0 0 79549 496 0 0 25 0 1 0 481665646 647720960 138499 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158135 138499 603 41 0 158094 0
vsize: 632540
[startup+810.416 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 145563 0 0 0 80547 498 0 0 25 0 1 0 481665646 649666560 138913 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158610 138913 603 41 0 158569 0
vsize: 634440
[startup+820.418 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 146017 0 0 0 81545 500 0 0 25 0 1 0 481665646 652058624 139367 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159194 139367 603 41 0 159153 0
vsize: 636776
[startup+830.418 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 146415 0 0 0 82543 502 0 0 25 0 1 0 481665646 653893632 139765 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159642 139765 603 41 0 159601 0
vsize: 638568
[startup+840.418 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 146864 0 0 0 83541 504 0 0 25 0 1 0 481665646 656220160 140214 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160210 140214 603 41 0 160169 0
vsize: 640840
[startup+850.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 147229 0 0 0 84540 506 0 0 25 0 1 0 481665646 657915904 140579 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160624 140579 603 41 0 160583 0
vsize: 642496
[startup+860.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 147693 0 0 0 85538 508 0 0 25 0 1 0 481665646 660443136 141043 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161241 141043 603 41 0 161200 0
vsize: 644964
[startup+870.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 148148 0 0 0 86536 510 0 0 25 0 1 0 481665646 663134208 141498 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161898 141498 603 41 0 161857 0
vsize: 647592
[startup+880.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 148553 0 0 0 87534 512 0 0 25 0 1 0 481665646 665124864 141903 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162384 141903 603 41 0 162343 0
vsize: 649536
[startup+890.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 149010 0 0 0 88532 514 0 0 25 0 1 0 481665646 667447296 142360 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162951 142360 603 41 0 162910 0
vsize: 651804
[startup+900.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 149450 0 0 0 89530 516 0 0 25 0 1 0 481665646 669917184 142800 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163554 142800 603 41 0 163513 0
vsize: 654216
[startup+910.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 149865 0 0 0 90529 518 0 0 25 0 1 0 481665646 671944704 143215 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 164049 143215 603 41 0 164008 0
vsize: 656196
[startup+920.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150284 0 0 0 91527 520 0 0 25 0 1 0 481665646 673976320 143634 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 164545 143634 603 41 0 164504 0
vsize: 658180
[startup+930.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150654 0 0 0 92525 522 0 0 25 0 1 0 481665646 675856384 144004 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165004 144004 603 41 0 164963 0
vsize: 660016
[startup+940.419 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150663 0 0 0 93520 526 0 0 25 0 1 0 481665646 676020224 144013 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144013 603 41 0 165003 0
vsize: 660176
[startup+950.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150668 0 0 0 94518 529 0 0 25 0 1 0 481665646 676020224 144018 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144018 603 41 0 165003 0
vsize: 660176
[startup+960.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150674 0 0 0 95515 533 0 0 25 0 1 0 481665646 676020224 144024 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144024 603 41 0 165003 0
vsize: 660176
[startup+970.421 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150674 0 0 0 96511 536 0 0 25 0 1 0 481665646 676020224 144024 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144024 603 41 0 165003 0
vsize: 660176
[startup+980.421 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150675 0 0 0 97508 539 0 0 25 0 1 0 481665646 676020224 144025 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144025 603 41 0 165003 0
vsize: 660176
[startup+990.421 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150688 0 0 0 98504 544 0 0 25 0 1 0 481665646 676020224 144038 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144038 603 41 0 165003 0
vsize: 660176
[startup+1000.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150700 0 0 0 99499 548 0 0 25 0 1 0 481665646 676184064 144050 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165084 144050 603 41 0 165043 0
vsize: 660336
[startup+1010.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 150867 0 0 0 100495 551 0 0 25 0 1 0 481665646 676839424 144217 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165244 144217 603 41 0 165203 0
vsize: 660976
[startup+1020.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 151242 0 0 0 101491 555 0 0 25 0 1 0 481665646 678866944 144592 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165739 144592 603 41 0 165698 0
vsize: 662956
[startup+1030.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 151562 0 0 0 102488 558 0 0 25 0 1 0 481665646 680402944 144912 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166114 144912 603 41 0 166073 0
vsize: 664456
[startup+1040.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 151803 0 0 0 103484 561 0 0 25 0 1 0 481665646 681713664 145153 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166434 145153 603 41 0 166393 0
vsize: 665736
[startup+1050.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 151991 0 0 0 104483 563 0 0 25 0 1 0 481665646 682663936 145341 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166666 145341 603 41 0 166625 0
vsize: 666664
[startup+1060.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 152183 0 0 0 105481 565 0 0 25 0 1 0 481665646 683642880 145533 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166905 145533 603 41 0 166864 0
vsize: 667620
[startup+1070.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 152519 0 0 0 106479 566 0 0 25 0 1 0 481665646 685608960 145869 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167385 145869 603 41 0 167344 0
vsize: 669540
[startup+1080.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 152853 0 0 0 107477 569 0 0 25 0 1 0 481665646 687771648 146203 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167913 146203 603 41 0 167872 0
vsize: 671652
[startup+1090.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 153225 0 0 0 108476 570 0 0 25 0 1 0 481665646 689930240 146575 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168440 146575 603 41 0 168399 0
vsize: 673760
[startup+1100.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 153400 0 0 0 109474 572 0 0 25 0 1 0 481665646 690716672 146750 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168632 146750 603 41 0 168591 0
vsize: 674528
[startup+1110.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 153580 0 0 0 110472 574 0 0 25 0 1 0 481665646 691306496 146930 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168776 146930 603 41 0 168735 0
vsize: 675104
[startup+1120.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 153721 0 0 0 111471 576 0 0 25 0 1 0 481665646 691896320 147071 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168920 147071 603 41 0 168879 0
vsize: 675680
[startup+1130.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 153863 0 0 0 112470 577 0 0 25 0 1 0 481665646 692486144 147213 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169064 147213 603 41 0 169023 0
vsize: 676256
[startup+1140.42 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 154047 0 0 0 113468 578 0 0 25 0 1 0 481665646 693399552 147397 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169287 147397 603 41 0 169246 0
vsize: 677148
[startup+1150.43 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 154282 0 0 0 114467 580 0 0 25 0 1 0 481665646 694611968 147632 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169583 147632 603 41 0 169542 0
vsize: 678332
[startup+1160.43 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 154422 0 0 0 115466 581 0 0 25 0 1 0 481665646 695103488 147772 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169703 147772 603 41 0 169662 0
vsize: 678812
[startup+1170.43 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 154611 0 0 0 116465 582 0 0 25 0 1 0 481665646 696049664 147961 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169934 147961 603 41 0 169893 0
vsize: 679736
[startup+1180.43 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 154837 0 0 0 117464 583 0 0 25 0 1 0 481665646 697262080 148187 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170230 148187 603 41 0 170189 0
vsize: 680920
[startup+1190.43 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 155033 0 0 0 118464 584 0 0 25 0 1 0 481665646 698343424 148383 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170494 148383 603 41 0 170453 0
vsize: 681976
[startup+1200.44 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29075
Raw data (stat): 29073 (minisat+) R 29072 30854 30853 0 -1 0 155245 0 0 0 119463 586 0 0 25 0 1 0 481665646 699420672 148595 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170757 148595 603 41 0 170716 0
vsize: 683028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.83 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 29075
Raw data (stat): 29073 (minisat+) Z 29072 30854 30853 0 -1 12 155245 0 0 0 119463 624 0 0 25 0 1 0 481665646 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.83
CPU time (s): 1200.89
CPU user time (s): 1194.64
CPU system time (s): 6.24905
CPU usage (%): 100.005
Max. virtual memory (Kb): 683028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####