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-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-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.81166
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 20228

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 20:26:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15273 boxname=wulflinc5 idbench=1175 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp98ic.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp98ic.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp98ic.opb
IDLAUNCH: 15273
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        559548 kB
Buffers:         23060 kB
Cached:         430332 kB
SwapCached:        304 kB
Active:          83264 kB
Inactive:       372600 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        559296 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            13540 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:47:00 (client local time) WITH STATUS 0 IN 1200.58 SECONDS
stats: 15273 7 1200.58 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.70 0.94 0.91 2/54 992
Raw data (stat): 992 (runsolver) R 991 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489731432 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+9.99979 s]
Raw data (loadavg): 0.74 0.94 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 17572 0 0 0 955 43 0 0 25 0 1 0 489731432 62672896 13769 4294967295 134512640 134672761 3221224544 3221222464 134544780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15301 13769 603 41 0 15260 0
vsize: 61204
[startup+20.0009 s]
Raw data (loadavg): 0.78 0.94 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 60246 0 0 0 1850 147 0 0 25 0 1 0 489731432 266862592 56147 4294967295 134512640 134672761 3221224544 3220911376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65152 56147 603 41 0 65111 0
vsize: 260608
[startup+30.0013 s]
Raw data (loadavg): 0.82 0.94 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 86429 0 0 0 2784 213 0 0 25 0 1 0 489731432 399683584 82328 4294967295 134512640 134672761 3221224544 3221223088 134621062 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.0007 s]
Raw data (loadavg): 0.84 0.94 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 86429 0 0 0 3785 213 0 0 25 0 1 0 489731432 399683584 82328 4294967295 134512640 134672761 3221224544 3221223088 134621141 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.0018 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 86429 0 0 0 4785 213 0 0 25 0 1 0 489731432 399683584 82328 4294967295 134512640 134672761 3221224544 3221223088 134621024 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.0016 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 91302 0 0 0 5769 229 0 0 25 0 1 0 489731432 411242496 84652 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100401 84652 603 41 0 100360 0
vsize: 401604
[startup+70.0019 s]
Raw data (loadavg): 0.90 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 93877 0 0 0 6753 245 0 0 25 0 1 0 489731432 421879808 87227 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102998 87227 603 41 0 102957 0
vsize: 411992
[startup+80.003 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 96114 0 0 0 7737 261 0 0 25 0 1 0 489731432 431144960 89464 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 105260 89464 603 41 0 105219 0
vsize: 421040
[startup+90.0028 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 98046 0 0 0 8727 269 0 0 25 0 1 0 489731432 439545856 91396 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107311 91396 603 41 0 107270 0
vsize: 429244
[startup+100.003 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 99480 0 0 0 9719 277 0 0 25 0 1 0 489731432 445657088 92830 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 108803 92830 603 41 0 108762 0
vsize: 435212
[startup+110.003 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 101410 0 0 0 10710 286 0 0 25 0 1 0 489731432 453791744 94760 4294967295 134512640 134672761 3221224544 3221222896 134604072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110789 94760 603 41 0 110748 0
vsize: 443156
[startup+120.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 102362 0 0 0 11704 292 0 0 25 0 1 0 489731432 457703424 95712 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111744 95712 603 41 0 111703 0
vsize: 446976
[startup+130.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 103524 0 0 0 12696 299 0 0 25 0 1 0 489731432 462442496 96874 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112901 96874 603 41 0 112860 0
vsize: 451604
[startup+140.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 105142 0 0 0 13688 307 0 0 25 0 1 0 489731432 468877312 98492 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114472 98492 603 41 0 114431 0
vsize: 457888
[startup+150.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 106357 0 0 0 14681 314 0 0 25 0 1 0 489731432 474353664 99707 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115809 99707 603 41 0 115768 0
vsize: 463236
[startup+160.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 107420 0 0 0 15677 319 0 0 25 0 1 0 489731432 479657984 100770 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117104 100770 603 41 0 117063 0
vsize: 468416
[startup+170.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 108401 0 0 0 16672 323 0 0 25 0 1 0 489731432 484233216 101751 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118221 101751 603 41 0 118180 0
vsize: 472884
[startup+180.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 109381 0 0 0 17668 328 0 0 25 0 1 0 489731432 488402944 102731 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119239 102731 603 41 0 119198 0
vsize: 476956
[startup+190.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 110303 0 0 0 18664 332 0 0 25 0 1 0 489731432 492257280 103653 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120180 103653 603 41 0 120139 0
vsize: 480720
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 111142 0 0 0 19660 335 0 0 25 0 1 0 489731432 495779840 104492 4294967295 134512640 134672761 3221224544 3221222992 134607016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121040 104492 603 41 0 120999 0
vsize: 484160
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 112058 0 0 0 20656 339 0 0 25 0 1 0 489731432 499605504 105408 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121974 105408 603 41 0 121933 0
vsize: 487896
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 112789 0 0 0 21653 342 0 0 25 0 1 0 489731432 502661120 106139 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122720 106139 603 41 0 122679 0
vsize: 490880
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 113571 0 0 0 22650 346 0 0 25 0 1 0 489731432 505921536 106921 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123516 106921 603 41 0 123475 0
vsize: 494064
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 114364 0 0 0 23646 349 0 0 25 0 1 0 489731432 509472768 107714 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124383 107714 603 41 0 124342 0
vsize: 497532
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 115010 0 0 0 24643 352 0 0 25 0 1 0 489731432 512540672 108360 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125132 108360 603 41 0 125091 0
vsize: 500528
[startup+260.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 115735 0 0 0 25640 356 0 0 25 0 1 0 489731432 516227072 109085 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126032 109085 603 41 0 125991 0
vsize: 504128
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 116497 0 0 0 26637 359 0 0 25 0 1 0 489731432 519761920 109847 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126895 109847 603 41 0 126854 0
vsize: 507580
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 117179 0 0 0 27632 363 0 0 25 0 1 0 489731432 523108352 110529 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127712 110529 603 41 0 127671 0
vsize: 510848
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 117799 0 0 0 28629 365 0 0 25 0 1 0 489731432 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 118390 0 0 0 29626 368 0 0 25 0 1 0 489731432 528773120 111740 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129095 111740 603 41 0 129054 0
vsize: 516380
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 118980 0 0 0 30623 371 0 0 25 0 1 0 489731432 531509248 112330 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129763 112330 603 41 0 129722 0
vsize: 519052
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 119587 0 0 0 31621 373 0 0 25 0 1 0 489731432 534532096 112937 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130501 112937 603 41 0 130460 0
vsize: 522004
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 120193 0 0 0 32618 376 0 0 25 0 1 0 489731432 537276416 113543 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131171 113543 603 41 0 131130 0
vsize: 524684
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 120825 0 0 0 33615 379 0 0 25 0 1 0 489731432 539987968 114175 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131833 114175 603 41 0 131792 0
vsize: 527332
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 121451 0 0 0 34612 382 0 0 25 0 1 0 489731432 542867456 114801 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132536 114801 603 41 0 132495 0
vsize: 530144
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 122031 0 0 0 35609 385 0 0 25 0 1 0 489731432 545193984 115381 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133104 115381 603 41 0 133063 0
vsize: 532416
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 122715 0 0 0 36607 387 0 0 25 0 1 0 489731432 548081664 116065 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133809 116065 603 41 0 133768 0
vsize: 535236
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 123327 0 0 0 37604 390 0 0 25 0 1 0 489731432 550895616 116677 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134496 116677 603 41 0 134455 0
vsize: 537984
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 123936 0 0 0 38601 393 0 0 25 0 1 0 489731432 553377792 117286 4294967295 134512640 134672761 3221224544 3221222832 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135102 117286 603 41 0 135061 0
vsize: 540408
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 124532 0 0 0 39599 395 0 0 25 0 1 0 489731432 555929600 117882 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135725 117882 603 41 0 135684 0
vsize: 542900
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 125037 0 0 0 40596 398 0 0 25 0 1 0 489731432 558055424 118387 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136244 118387 603 41 0 136203 0
vsize: 544976
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 125566 0 0 0 41592 401 0 0 25 0 1 0 489731432 560246784 118916 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136779 118916 603 41 0 136738 0
vsize: 547116
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 126175 0 0 0 42590 404 0 0 25 0 1 0 489731432 563130368 119525 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137483 119525 603 41 0 137442 0
vsize: 549932
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 126847 0 0 0 43587 407 0 0 25 0 1 0 489731432 566349824 120197 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138269 120197 603 41 0 138228 0
vsize: 553076
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 127444 0 0 0 44585 409 0 0 25 0 1 0 489731432 569008128 120794 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138918 120794 603 41 0 138877 0
vsize: 555672
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 127985 0 0 0 45582 412 0 0 25 0 1 0 489731432 571514880 121335 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139530 121335 603 41 0 139489 0
vsize: 558120
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 128583 0 0 0 46579 415 0 0 25 0 1 0 489731432 574357504 121933 4294967295 134512640 134672761 3221224544 3221222928 134632066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140224 121933 603 41 0 140183 0
vsize: 560896
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 129144 0 0 0 47576 418 0 0 25 0 1 0 489731432 576552960 122494 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140760 122494 603 41 0 140719 0
vsize: 563040
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 129792 0 0 0 48574 421 0 0 25 0 1 0 489731432 579514368 123142 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141483 123142 603 41 0 141442 0
vsize: 565932
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 130387 0 0 0 49572 422 0 0 25 0 1 0 489731432 582148096 123737 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142126 123737 603 41 0 142085 0
vsize: 568504
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 130955 0 0 0 50570 425 0 0 25 0 1 0 489731432 584667136 124305 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142741 124305 603 41 0 142700 0
vsize: 570964
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 131464 0 0 0 51568 427 0 0 25 0 1 0 489731432 587083776 124814 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143331 124814 603 41 0 143290 0
vsize: 573324
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 132105 0 0 0 52566 429 0 0 25 0 1 0 489731432 589934592 125455 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144027 125455 603 41 0 143986 0
vsize: 576108
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 132674 0 0 0 53563 432 0 0 25 0 1 0 489731432 592293888 126024 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144603 126024 603 41 0 144562 0
vsize: 578412
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 133194 0 0 0 54561 435 0 0 25 0 1 0 489731432 594698240 126544 4294967295 134512640 134672761 3221224544 3221221856 134566712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145190 126544 603 41 0 145149 0
vsize: 580760
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 133791 0 0 0 55559 437 0 0 25 0 1 0 489731432 597479424 127141 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145869 127141 603 41 0 145828 0
vsize: 583476
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 134310 0 0 0 56557 438 0 0 25 0 1 0 489731432 599777280 127660 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146430 127660 603 41 0 146389 0
vsize: 585720
[startup+580.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 134839 0 0 0 57555 441 0 0 25 0 1 0 489731432 602148864 128189 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147009 128189 603 41 0 146968 0
vsize: 588036
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 135434 0 0 0 58552 443 0 0 25 0 1 0 489731432 604958720 128784 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147695 128784 603 41 0 147654 0
vsize: 590780
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 136003 0 0 0 59550 446 0 0 25 0 1 0 489731432 607506432 129353 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148317 129353 603 41 0 148276 0
vsize: 593268
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 136473 0 0 0 60548 448 0 0 25 0 1 0 489731432 609484800 129823 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148800 129823 603 41 0 148759 0
vsize: 595200
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 136965 0 0 0 61546 450 0 0 25 0 1 0 489731432 611700736 130315 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149341 130315 603 41 0 149300 0
vsize: 597364
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 137437 0 0 0 62544 452 0 0 25 0 1 0 489731432 613564416 130787 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149796 130787 603 41 0 149755 0
vsize: 599184
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 137974 0 0 0 63541 455 0 0 25 0 1 0 489731432 616042496 131324 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150401 131324 603 41 0 150360 0
vsize: 601604
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 138435 0 0 0 64539 458 0 0 25 0 1 0 489731432 618074112 131785 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150897 131785 603 41 0 150856 0
vsize: 603588
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 138886 0 0 0 65536 460 0 0 25 0 1 0 489731432 619991040 132236 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151365 132236 603 41 0 151324 0
vsize: 605460
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 139299 0 0 0 66534 462 0 0 25 0 1 0 489731432 621645824 132649 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151769 132649 603 41 0 151728 0
vsize: 607076
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 139819 0 0 0 67532 465 0 0 25 0 1 0 489731432 624177152 133169 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152387 133169 603 41 0 152346 0
vsize: 609548
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 140307 0 0 0 68530 467 0 0 25 0 1 0 489731432 626262016 133657 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152896 133657 603 41 0 152855 0
vsize: 611584
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 140725 0 0 0 69528 469 0 0 25 0 1 0 489731432 628035584 134075 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153329 134075 603 41 0 153288 0
vsize: 613316
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 141180 0 0 0 70526 471 0 0 25 0 1 0 489731432 630145024 134530 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153844 134530 603 41 0 153803 0
vsize: 615376
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 141599 0 0 0 71524 473 0 0 25 0 1 0 489731432 631918592 134949 4294967295 134512640 134672761 3221224544 3221222864 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154277 134949 603 41 0 154236 0
vsize: 617108
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 142053 0 0 0 72523 475 0 0 25 0 1 0 489731432 633896960 135403 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154760 135403 603 41 0 154719 0
vsize: 619040
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 142490 0 0 0 73521 477 0 0 25 0 1 0 489731432 635830272 135840 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155232 135840 603 41 0 155191 0
vsize: 620928
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 142888 0 0 0 74519 478 0 0 25 0 1 0 489731432 637521920 136238 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155645 136238 603 41 0 155604 0
vsize: 622580
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 143322 0 0 0 75517 481 0 0 25 0 1 0 489731432 639459328 136672 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156118 136672 603 41 0 156077 0
vsize: 624472
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 143764 0 0 0 76514 483 0 0 25 0 1 0 489731432 641568768 137114 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156633 137114 603 41 0 156592 0
vsize: 626532
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 144196 0 0 0 77513 486 0 0 25 0 1 0 489731432 643670016 137546 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157146 137546 603 41 0 157105 0
vsize: 628584
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 144609 0 0 0 78510 488 0 0 25 0 1 0 489731432 645160960 137959 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157510 137959 603 41 0 157469 0
vsize: 630040
[startup+800.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 145048 0 0 0 79508 490 0 0 25 0 1 0 489731432 647233536 138398 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158016 138398 603 41 0 157975 0
vsize: 632064
[startup+810.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 145486 0 0 0 80507 492 0 0 25 0 1 0 489731432 649289728 138836 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158518 138836 603 41 0 158477 0
vsize: 634072
[startup+820.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 145945 0 0 0 81505 494 0 0 25 0 1 0 489731432 651763712 139295 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159122 139295 603 41 0 159081 0
vsize: 636488
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 146379 0 0 0 82503 497 0 0 25 0 1 0 489731432 653746176 139729 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159606 139729 603 41 0 159565 0
vsize: 638424
[startup+840.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 146776 0 0 0 83502 499 0 0 25 0 1 0 489731432 655777792 140126 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160102 140126 603 41 0 160061 0
vsize: 640408
[startup+850.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 147152 0 0 0 84500 500 0 0 25 0 1 0 489731432 657620992 140502 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160552 140502 603 41 0 160511 0
vsize: 642208
[startup+860.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 147606 0 0 0 85498 502 0 0 25 0 1 0 489731432 659918848 140956 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161113 140956 603 41 0 161072 0
vsize: 644452
[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 148057 0 0 0 86497 504 0 0 25 0 1 0 489731432 662622208 141407 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161773 141407 603 41 0 161732 0
vsize: 647092
[startup+880.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 148482 0 0 0 87497 506 0 0 25 0 1 0 489731432 664813568 141832 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162308 141832 603 41 0 162267 0
vsize: 649232
[startup+890.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 148917 0 0 0 88495 508 0 0 25 0 1 0 489731432 667070464 142267 4294967295 134512640 134672761 3221224544 3221222636 134566528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162859 142267 603 41 0 162818 0
vsize: 651436
[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 149410 0 0 0 89492 511 0 0 25 0 1 0 489731432 669585408 142760 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163473 142760 603 41 0 163432 0
vsize: 653892
[startup+910.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 149791 0 0 0 90490 513 0 0 25 0 1 0 489731432 671481856 143141 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163936 143141 603 41 0 163895 0
vsize: 655744
[startup+920.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150213 0 0 0 91489 515 0 0 25 0 1 0 489731432 673529856 143563 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 164436 143563 603 41 0 164395 0
vsize: 657744
[startup+930.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150642 0 0 0 92488 516 0 0 25 0 1 0 489731432 675856384 143992 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165004 143992 603 41 0 164963 0
vsize: 660016
[startup+940.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150663 0 0 0 93482 521 0 0 25 0 1 0 489731432 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.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150668 0 0 0 94478 525 0 0 25 0 1 0 489731432 676020224 144018 4294967295 134512640 134672761 3221224544 3221222960 134644246 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.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150668 0 0 0 95475 529 0 0 25 0 1 0 489731432 676020224 144018 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165044 144018 603 41 0 165003 0
vsize: 660176
[startup+970.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150674 0 0 0 96471 533 0 0 25 0 1 0 489731432 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.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150675 0 0 0 97467 537 0 0 25 0 1 0 489731432 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.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150688 0 0 0 98462 542 0 0 25 0 1 0 489731432 676020224 144038 4294967295 134512640 134672761 3221224544 3221222960 134644240 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150700 0 0 0 99459 545 0 0 25 0 1 0 489731432 676184064 144050 4294967295 134512640 134672761 3221224544 3221222960 134644291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165084 144050 603 41 0 165043 0
vsize: 660336
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 150827 0 0 0 100456 549 0 0 25 0 1 0 489731432 676675584 144177 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165204 144177 603 41 0 165163 0
vsize: 660816
[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 151160 0 0 0 101453 552 0 0 25 0 1 0 489731432 678375424 144510 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 165619 144510 603 41 0 165578 0
vsize: 662476
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 151500 0 0 0 102450 556 0 0 25 0 1 0 489731432 680075264 144850 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166034 144850 603 41 0 165993 0
vsize: 664136
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 151775 0 0 0 103446 559 0 0 25 0 1 0 489731432 681517056 145125 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166386 145125 603 41 0 166345 0
vsize: 665544
[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 151922 0 0 0 104444 561 0 0 25 0 1 0 489731432 682270720 145272 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166570 145272 603 41 0 166529 0
vsize: 666280
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 152118 0 0 0 105443 563 0 0 25 0 1 0 489731432 683249664 145468 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166809 145468 603 41 0 166768 0
vsize: 667236
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 152479 0 0 0 106441 565 0 0 25 0 1 0 489731432 685412352 145829 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167337 145829 603 41 0 167296 0
vsize: 669348
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 152790 0 0 0 107439 567 0 0 25 0 1 0 489731432 687378432 146140 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167817 146140 603 41 0 167776 0
vsize: 671268
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 153156 0 0 0 108438 569 0 0 25 0 1 0 489731432 689537024 146506 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168344 146506 603 41 0 168303 0
vsize: 673376
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 153346 0 0 0 109436 571 0 0 25 0 1 0 489731432 690323456 146696 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168536 146696 603 41 0 168495 0
vsize: 674144
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 153517 0 0 0 110435 572 0 0 25 0 1 0 489731432 690913280 146867 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168680 146867 603 41 0 168639 0
vsize: 674720
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 153706 0 0 0 111434 573 0 0 25 0 1 0 489731432 691896320 147056 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168920 147056 603 41 0 168879 0
vsize: 675680
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 153849 0 0 0 112433 574 0 0 25 0 1 0 489731432 692486144 147199 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169064 147199 603 41 0 169023 0
vsize: 676256
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 154015 0 0 0 113431 577 0 0 25 0 1 0 489731432 693202944 147365 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169239 147365 603 41 0 169198 0
vsize: 676956
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 154218 0 0 0 114429 578 0 0 25 0 1 0 489731432 694284288 147568 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169503 147568 603 41 0 169462 0
vsize: 678012
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 154387 0 0 0 115427 580 0 0 25 0 1 0 489731432 694939648 147737 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169663 147737 603 41 0 169622 0
vsize: 678652
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 154585 0 0 0 116426 582 0 0 25 0 1 0 489731432 696049664 147935 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169934 147935 603 41 0 169893 0
vsize: 679736
[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 154774 0 0 0 117425 583 0 0 25 0 1 0 489731432 696901632 148124 4294967295 134512640 134672761 3221224544 3221222960 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170142 148124 603 41 0 170101 0
vsize: 680568
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 154992 0 0 0 118423 585 0 0 25 0 1 0 489731432 698146816 148342 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170446 148342 603 41 0 170405 0
vsize: 681784
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 992
Raw data (stat): 992 (minisat+) R 991 24215 24214 0 -1 0 155213 0 0 0 119432 586 0 0 25 0 1 0 489731432 699228160 148563 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170710 148563 603 41 0 170669 0
vsize: 682840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.6 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 992
Raw data (stat): 992 (minisat+) Z 991 24215 24214 0 -1 12 155213 0 0 0 119432 625 0 0 24 0 1 0 489731432 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.6
CPU time (s): 1200.58
CPU user time (s): 1194.33
CPU system time (s): 6.25305
CPU usage (%): 99.9981
Max. virtual memory (Kb): 682840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####