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 14215

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-20 23:18:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20280 boxname=wulflinc13 idbench=1560 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-sp98ic.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-sp98ic.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-sp98ic.opb
IDLAUNCH: 20280
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        570192 kB
Buffers:         33588 kB
Cached:         408004 kB
SwapCached:          0 kB
Active:         100740 kB
Inactive:       343676 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        569940 kB
SwapTotal:     2097136 kB
SwapFree:      2097036 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            14528 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:38:07 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 20280 7 1200.28 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 ---[  37]---> BDD-cost: 2262
c ---[  36]---> BDD-cost: 1946
c ---[  35]---> Adder-cost: 11313   maxlim: 17   bits: 6/5
c ---[  34]---> BDD-cost: 1782
c ---[  33]---> BDD-cost: 1032
c ---[  32]---> BDD-cost: 1406
c ---[  31]---> BDD-cost: 1286
c ---[  30]---> BDD-cost: 1732
c ---[  29]---> BDD-cost: 3506
c ---[  28]---> BDD-cost: 4667
c ---[  27]---> BDD-cost: 5492
c ---[  26]---> BDD-cost:15264
c ---[  25]---> BDD-cost:  692
c ---[  24]---> BDD-cost: 1291
c ---[  23]---> BDD-cost:  938
c ---[  22]---> BDD-cost: 1436
c ---[  21]---> BDD-cost: 1850
c ---[  20]---> BDD-cost: 2446
c ---[  19]---> BDD-cost: 1294
c ---[  18]---> BDD-cost: 1740
c ---[  17]---> BDD-cost: 4705
c ---[  16]---> BDD-cost:  574
c ---[  15]---> BDD-cost: 2972
c ---[  14]---> BDD-cost: 1798
c ---[  13]---> BDD-cost: 2110
c ---[  12]---> BDD-cost: 4576
c ---[  11]---> BDD-cost: 7893
c ---[  10]---> BDD-cost:  964
c ---[   9]---> BDD-cost:  888
c ---[   8]---> Adder-cost: 3085   maxlim: 18   bits: 6/5
c ---[   7]---> BDD-cost:10368
c ---[   6]---> BDD-cost:13837
c ---[   5]---> BDD-cost: 2093
c ---[   4]---> BDD-cost: 5322
c ---[   3]---> BDD-cost:15898
c ---[   2]---> BDD-cost:10691
c ---[   1]---> BDD-cost: 7120
c ---[   0]---> BDD-cost: 6716
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2838723  8628540 |  946241       0        0     nan |  0.000 % |
c |       101 | 2838723  8628540 | 1040865     101      432     4.3 |  0.153 % |
c |       251 | 2838629  8628266 | 1144951     198      746     3.8 |  0.156 % |
c |       476 | 2838402  8627591 | 1259446     369     1441     3.9 |  0.164 % |
c |       813 | 2838105  8626710 | 1385391     676     4006     5.9 |  0.174 % |
c |      1350 | 2837883  8626044 | 1523930     994     4632     4.7 |  0.180 % |
c |      2109 | 2836702  8622509 | 1676323    1313     5922     4.5 |  0.221 % |
c |      3248 | 2835466  8618721 | 1843956    1934     8688     4.5 |  0.260 % |
c |      4956 | 2833478  8612717 | 2028351    2841    13717     4.8 |  0.330 % |
c |      7518 | 2831079  8605410 | 2231186    4567    24348     5.3 |  0.408 % |
#### 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.67 0.91 0.95 2/54 25683
Raw data (stat): 25683 (runsolver) R 25682 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482121028 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99995 s]
Raw data (loadavg): 0.72 0.91 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 17171 0 0 0 958 40 0 0 25 0 1 0 482121028 61100032 13361 4294967295 134512640 134672761 3221224544 3221222080 134523443 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14917 13361 603 41 0 14876 0
vsize: 59668
[startup+20.0049 s]
Raw data (loadavg): 0.76 0.92 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 51921 0 0 0 1874 125 0 0 25 0 1 0 482121028 217600000 47795 4294967295 134512640 134672761 3221224544 3221220688 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53125 47796 603 41 0 53084 0
vsize: 212500
[startup+30.0053 s]
Raw data (loadavg): 0.80 0.92 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 62858 0 0 0 2846 153 0 0 25 0 1 0 482121028 283136000 58732 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69125 58732 603 41 0 69084 0
vsize: 276500
[startup+40.005 s]
Raw data (loadavg): 0.83 0.92 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 62951 0 0 0 3846 153 0 0 25 0 1 0 482121028 283136000 58825 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69125 58825 603 41 0 69084 0
vsize: 276500
[startup+50.0049 s]
Raw data (loadavg): 0.85 0.92 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 62975 0 0 0 4846 153 0 0 25 0 1 0 482121028 283136000 58849 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69125 58849 603 41 0 69084 0
vsize: 276500
[startup+60.0052 s]
Raw data (loadavg): 0.88 0.92 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 62976 0 0 0 5846 153 0 0 25 0 1 0 482121028 283136000 58850 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69125 58850 603 41 0 69084 0
vsize: 276500
[startup+70.0049 s]
Raw data (loadavg): 0.89 0.93 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63052 0 0 0 6845 153 0 0 25 0 1 0 482121028 283271168 58926 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69158 58926 603 41 0 69117 0
vsize: 276632
[startup+80.0062 s]
Raw data (loadavg): 0.91 0.93 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63053 0 0 0 7845 154 0 0 25 0 1 0 482121028 283271168 58927 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69158 58927 603 41 0 69117 0
vsize: 276632
[startup+90.0062 s]
Raw data (loadavg): 0.92 0.93 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63053 0 0 0 8846 154 0 0 25 0 1 0 482121028 283271168 58927 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69158 58927 603 41 0 69117 0
vsize: 276632
[startup+100.006 s]
Raw data (loadavg): 0.93 0.93 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63122 0 0 0 9846 154 0 0 25 0 1 0 482121028 283418624 58996 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69194 58996 603 41 0 69153 0
vsize: 276776
[startup+110.007 s]
Raw data (loadavg): 0.94 0.93 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63141 0 0 0 10846 154 0 0 25 0 1 0 482121028 283418624 59015 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69194 59015 603 41 0 69153 0
vsize: 276776
[startup+120.006 s]
Raw data (loadavg): 0.95 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63145 0 0 0 11846 154 0 0 25 0 1 0 482121028 283418624 59019 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69194 59019 603 41 0 69153 0
vsize: 276776
[startup+130.006 s]
Raw data (loadavg): 0.96 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63170 0 0 0 12846 154 0 0 25 0 1 0 482121028 283418624 59044 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69194 59044 603 41 0 69153 0
vsize: 276776
[startup+140.006 s]
Raw data (loadavg): 0.97 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63175 0 0 0 13846 154 0 0 25 0 1 0 482121028 283553792 59049 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69227 59049 603 41 0 69186 0
vsize: 276908
[startup+150.006 s]
Raw data (loadavg): 0.97 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63179 0 0 0 14846 154 0 0 25 0 1 0 482121028 283553792 59053 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69227 59053 603 41 0 69186 0
vsize: 276908
[startup+160.006 s]
Raw data (loadavg): 0.97 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63181 0 0 0 15846 154 0 0 25 0 1 0 482121028 283553792 59055 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69227 59055 603 41 0 69186 0
vsize: 276908
[startup+170.006 s]
Raw data (loadavg): 0.98 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63192 0 0 0 16846 154 0 0 25 0 1 0 482121028 283553792 59066 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69227 59066 603 41 0 69186 0
vsize: 276908
[startup+180.006 s]
Raw data (loadavg): 0.98 0.94 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63212 0 0 0 17847 154 0 0 25 0 1 0 482121028 283553792 59086 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69227 59086 603 41 0 69186 0
vsize: 276908
[startup+190.006 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63259 0 0 0 18847 154 0 0 25 0 1 0 482121028 283688960 59133 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69260 59133 603 41 0 69219 0
vsize: 277040
[startup+200.006 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63266 0 0 0 19847 154 0 0 25 0 1 0 482121028 283688960 59140 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69260 59140 603 41 0 69219 0
vsize: 277040
[startup+210.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63266 0 0 0 20847 154 0 0 25 0 1 0 482121028 283688960 59140 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69260 59140 603 41 0 69219 0
vsize: 277040
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63269 0 0 0 21847 154 0 0 25 0 1 0 482121028 283824128 59143 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69293 59143 603 41 0 69252 0
vsize: 277172
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63272 0 0 0 22848 154 0 0 25 0 1 0 482121028 283824128 59146 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69293 59146 603 41 0 69252 0
vsize: 277172
[startup+240.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63282 0 0 0 23848 154 0 0 25 0 1 0 482121028 283824128 59156 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69293 59156 603 41 0 69252 0
vsize: 277172
[startup+250.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63315 0 0 0 24848 154 0 0 25 0 1 0 482121028 283824128 59189 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69293 59189 603 41 0 69252 0
vsize: 277172
[startup+260.007 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63327 0 0 0 25848 154 0 0 25 0 1 0 482121028 283959296 59201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69326 59201 603 41 0 69285 0
vsize: 277304
[startup+270.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63332 0 0 0 26848 154 0 0 25 0 1 0 482121028 283959296 59206 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69326 59206 603 41 0 69285 0
vsize: 277304
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63333 0 0 0 27848 154 0 0 25 0 1 0 482121028 283959296 59207 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69326 59207 603 41 0 69285 0
vsize: 277304
[startup+290.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63333 0 0 0 28849 154 0 0 25 0 1 0 482121028 283959296 59207 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69326 59207 603 41 0 69285 0
vsize: 277304
[startup+300.006 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63336 0 0 0 29848 155 0 0 25 0 1 0 482121028 283959296 59210 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69326 59210 603 41 0 69285 0
vsize: 277304
[startup+310.006 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63336 0 0 0 30848 155 0 0 25 0 1 0 482121028 283959296 59210 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69326 59210 603 41 0 69285 0
vsize: 277304
[startup+320.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63373 0 0 0 31848 155 0 0 25 0 1 0 482121028 283959296 59247 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69326 59247 603 41 0 69285 0
vsize: 277304
[startup+330.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63373 0 0 0 32848 156 0 0 25 0 1 0 482121028 283959296 59247 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69326 59247 603 41 0 69285 0
vsize: 277304
[startup+340.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63392 0 0 0 33847 156 0 0 25 0 1 0 482121028 284094464 59266 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69359 59266 603 41 0 69318 0
vsize: 277436
[startup+350.006 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63393 0 0 0 34847 156 0 0 25 0 1 0 482121028 284094464 59267 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69359 59267 603 41 0 69318 0
vsize: 277436
[startup+360.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63397 0 0 0 35847 157 0 0 25 0 1 0 482121028 284094464 59271 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69359 59271 603 41 0 69318 0
vsize: 277436
[startup+370.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63403 0 0 0 36847 157 0 0 25 0 1 0 482121028 284094464 59277 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69359 59277 603 41 0 69318 0
vsize: 277436
[startup+380.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63405 0 0 0 37847 157 0 0 25 0 1 0 482121028 284094464 59279 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69359 59279 603 41 0 69318 0
vsize: 277436
[startup+390.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63410 0 0 0 38847 157 0 0 25 0 1 0 482121028 284229632 59284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59284 603 41 0 69351 0
vsize: 277568
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63414 0 0 0 39847 158 0 0 25 0 1 0 482121028 284229632 59288 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59288 603 41 0 69351 0
vsize: 277568
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63414 0 0 0 40846 158 0 0 25 0 1 0 482121028 284229632 59288 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59288 603 41 0 69351 0
vsize: 277568
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63423 0 0 0 41846 159 0 0 25 0 1 0 482121028 284229632 59297 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59297 603 41 0 69351 0
vsize: 277568
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63439 0 0 0 42846 159 0 0 25 0 1 0 482121028 284229632 59313 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59313 603 41 0 69351 0
vsize: 277568
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63441 0 0 0 43846 159 0 0 25 0 1 0 482121028 284229632 59315 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59315 603 41 0 69351 0
vsize: 277568
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63449 0 0 0 44845 160 0 0 25 0 1 0 482121028 284229632 59323 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69392 59323 603 41 0 69351 0
vsize: 277568
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63455 0 0 0 45845 160 0 0 25 0 1 0 482121028 284364800 59329 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59329 603 41 0 69384 0
vsize: 277700
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63457 0 0 0 46845 160 0 0 25 0 1 0 482121028 284364800 59331 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59331 603 41 0 69384 0
vsize: 277700
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63458 0 0 0 47845 160 0 0 25 0 1 0 482121028 284364800 59332 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59332 603 41 0 69384 0
vsize: 277700
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63459 0 0 0 48845 160 0 0 25 0 1 0 482121028 284364800 59333 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59333 603 41 0 69384 0
vsize: 277700
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63470 0 0 0 49845 161 0 0 25 0 1 0 482121028 284364800 59344 4294967295 134512640 134672761 3221224544 3221223716 134556609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59344 603 41 0 69384 0
vsize: 277700
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63472 0 0 0 50844 162 0 0 25 0 1 0 482121028 284364800 59346 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59346 603 41 0 69384 0
vsize: 277700
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63479 0 0 0 51844 162 0 0 25 0 1 0 482121028 284364800 59353 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69425 59353 603 41 0 69384 0
vsize: 277700
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63489 0 0 0 52844 162 0 0 25 0 1 0 482121028 284499968 59363 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59363 603 41 0 69417 0
vsize: 277832
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63489 0 0 0 53844 162 0 0 25 0 1 0 482121028 284499968 59363 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59363 603 41 0 69417 0
vsize: 277832
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63490 0 0 0 54844 162 0 0 25 0 1 0 482121028 284499968 59364 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59364 603 41 0 69417 0
vsize: 277832
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63490 0 0 0 55844 162 0 0 25 0 1 0 482121028 284499968 59364 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59364 603 41 0 69417 0
vsize: 277832
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63490 0 0 0 56843 163 0 0 25 0 1 0 482121028 284499968 59364 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59364 603 41 0 69417 0
vsize: 277832
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63491 0 0 0 57843 163 0 0 25 0 1 0 482121028 284499968 59365 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59365 603 41 0 69417 0
vsize: 277832
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63498 0 0 0 58843 163 0 0 25 0 1 0 482121028 284499968 59372 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59372 603 41 0 69417 0
vsize: 277832
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63499 0 0 0 59843 164 0 0 25 0 1 0 482121028 284499968 59373 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59373 603 41 0 69417 0
vsize: 277832
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63511 0 0 0 60843 164 0 0 25 0 1 0 482121028 284499968 59385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59385 603 41 0 69417 0
vsize: 277832
[startup+620.013 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63512 0 0 0 61843 164 0 0 25 0 1 0 482121028 284499968 59386 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59386 603 41 0 69417 0
vsize: 277832
[startup+630.013 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63513 0 0 0 62843 164 0 0 25 0 1 0 482121028 284499968 59387 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59387 603 41 0 69417 0
vsize: 277832
[startup+640.014 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63514 0 0 0 63843 165 0 0 25 0 1 0 482121028 284499968 59388 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59388 603 41 0 69417 0
vsize: 277832
[startup+650.013 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63514 0 0 0 64843 165 0 0 25 0 1 0 482121028 284499968 59388 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59388 603 41 0 69417 0
vsize: 277832
[startup+660.013 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63515 0 0 0 65843 165 0 0 25 0 1 0 482121028 284499968 59389 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59389 603 41 0 69417 0
vsize: 277832
[startup+670.014 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63520 0 0 0 66843 165 0 0 25 0 1 0 482121028 284499968 59394 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69458 59394 603 41 0 69417 0
vsize: 277832
[startup+680.015 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63523 0 0 0 67843 165 0 0 25 0 1 0 482121028 284499968 59397 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69458 59397 603 41 0 69417 0
vsize: 277832
[startup+690.015 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63524 0 0 0 68843 165 0 0 25 0 1 0 482121028 284499968 59398 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69458 59398 603 41 0 69417 0
vsize: 277832
[startup+700.015 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63533 0 0 0 69843 165 0 0 25 0 1 0 482121028 284499968 59407 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69458 59407 603 41 0 69417 0
vsize: 277832
[startup+710.015 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63535 0 0 0 70843 165 0 0 25 0 1 0 482121028 284499968 59409 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69458 59409 603 41 0 69417 0
vsize: 277832
[startup+720.015 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63535 0 0 0 71843 165 0 0 25 0 1 0 482121028 284499968 59409 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69458 59409 603 41 0 69417 0
vsize: 277832
[startup+730.015 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63536 0 0 0 72844 165 0 0 25 0 1 0 482121028 284635136 59410 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59410 603 41 0 69450 0
vsize: 277964
[startup+740.015 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63538 0 0 0 73844 165 0 0 25 0 1 0 482121028 284635136 59412 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59412 603 41 0 69450 0
vsize: 277964
[startup+750.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63542 0 0 0 74844 165 0 0 25 0 1 0 482121028 284635136 59416 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59416 603 41 0 69450 0
vsize: 277964
[startup+760.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63542 0 0 0 75844 165 0 0 25 0 1 0 482121028 284635136 59416 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59416 603 41 0 69450 0
vsize: 277964
[startup+770.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63543 0 0 0 76844 165 0 0 25 0 1 0 482121028 284635136 59417 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59417 603 41 0 69450 0
vsize: 277964
[startup+780.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63543 0 0 0 77844 166 0 0 25 0 1 0 482121028 284635136 59417 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59417 603 41 0 69450 0
vsize: 277964
[startup+790.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63543 0 0 0 78844 166 0 0 25 0 1 0 482121028 284635136 59417 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59417 603 41 0 69450 0
vsize: 277964
[startup+800.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63545 0 0 0 79844 166 0 0 25 0 1 0 482121028 284635136 59419 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59419 603 41 0 69450 0
vsize: 277964
[startup+810.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63548 0 0 0 80844 166 0 0 25 0 1 0 482121028 284635136 59422 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59422 603 41 0 69450 0
vsize: 277964
[startup+820.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63548 0 0 0 81844 166 0 0 25 0 1 0 482121028 284635136 59422 4294967295 134512640 134672761 3221224544 3221223760 134561950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59422 603 41 0 69450 0
vsize: 277964
[startup+830.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63555 0 0 0 82845 166 0 0 25 0 1 0 482121028 284635136 59429 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59429 603 41 0 69450 0
vsize: 277964
[startup+840.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63556 0 0 0 83845 166 0 0 25 0 1 0 482121028 284635136 59430 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59430 603 41 0 69450 0
vsize: 277964
[startup+850.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63558 0 0 0 84845 166 0 0 25 0 1 0 482121028 284635136 59432 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59432 603 41 0 69450 0
vsize: 277964
[startup+860.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63562 0 0 0 85845 166 0 0 25 0 1 0 482121028 284635136 59436 4294967295 134512640 134672761 3221224544 3221223760 134561982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59436 603 41 0 69450 0
vsize: 277964
[startup+870.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63562 0 0 0 86845 166 0 0 25 0 1 0 482121028 284635136 59436 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59436 603 41 0 69450 0
vsize: 277964
[startup+880.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63564 0 0 0 87845 166 0 0 25 0 1 0 482121028 284635136 59438 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59438 603 41 0 69450 0
vsize: 277964
[startup+890.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63564 0 0 0 88846 166 0 0 25 0 1 0 482121028 284635136 59438 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59438 603 41 0 69450 0
vsize: 277964
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63565 0 0 0 89846 166 0 0 25 0 1 0 482121028 284635136 59439 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59439 603 41 0 69450 0
vsize: 277964
[startup+910.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63566 0 0 0 90846 166 0 0 25 0 1 0 482121028 284635136 59440 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59440 603 41 0 69450 0
vsize: 277964
[startup+920.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63566 0 0 0 91846 166 0 0 25 0 1 0 482121028 284635136 59440 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59440 603 41 0 69450 0
vsize: 277964
[startup+930.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63568 0 0 0 92846 166 0 0 25 0 1 0 482121028 284635136 59442 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59442 603 41 0 69450 0
vsize: 277964
[startup+940.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63569 0 0 0 93846 166 0 0 25 0 1 0 482121028 284635136 59443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59443 603 41 0 69450 0
vsize: 277964
[startup+950.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63569 0 0 0 94846 166 0 0 25 0 1 0 482121028 284635136 59443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69491 59443 603 41 0 69450 0
vsize: 277964
[startup+960.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63574 0 0 0 95846 166 0 0 25 0 1 0 482121028 284770304 59448 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59448 603 41 0 69483 0
vsize: 278096
[startup+970.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63574 0 0 0 96847 166 0 0 25 0 1 0 482121028 284770304 59448 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59448 603 41 0 69483 0
vsize: 278096
[startup+980.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63574 0 0 0 97847 166 0 0 25 0 1 0 482121028 284770304 59448 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59448 603 41 0 69483 0
vsize: 278096
[startup+990.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63575 0 0 0 98847 166 0 0 25 0 1 0 482121028 284770304 59449 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59449 603 41 0 69483 0
vsize: 278096
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63576 0 0 0 99847 166 0 0 25 0 1 0 482121028 284770304 59450 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59450 603 41 0 69483 0
vsize: 278096
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63578 0 0 0 100847 166 0 0 25 0 1 0 482121028 284770304 59452 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59452 603 41 0 69483 0
vsize: 278096
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63578 0 0 0 101847 166 0 0 25 0 1 0 482121028 284770304 59452 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59452 603 41 0 69483 0
vsize: 278096
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63580 0 0 0 102848 166 0 0 25 0 1 0 482121028 284770304 59454 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59454 603 41 0 69483 0
vsize: 278096
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63582 0 0 0 103847 166 0 0 25 0 1 0 482121028 284770304 59456 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69524 59456 603 41 0 69483 0
vsize: 278096
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63596 0 0 0 104847 166 0 0 25 0 1 0 482121028 284770304 59470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59470 603 41 0 69483 0
vsize: 278096
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63597 0 0 0 105847 166 0 0 25 0 1 0 482121028 284770304 59471 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59471 603 41 0 69483 0
vsize: 278096
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63598 0 0 0 106847 166 0 0 25 0 1 0 482121028 284770304 59472 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59472 603 41 0 69483 0
vsize: 278096
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63599 0 0 0 107847 166 0 0 25 0 1 0 482121028 284770304 59473 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59473 603 41 0 69483 0
vsize: 278096
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63601 0 0 0 108848 166 0 0 25 0 1 0 482121028 284770304 59475 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59475 603 41 0 69483 0
vsize: 278096
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63601 0 0 0 109848 166 0 0 25 0 1 0 482121028 284770304 59475 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59475 603 41 0 69483 0
vsize: 278096
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63603 0 0 0 110848 167 0 0 25 0 1 0 482121028 284770304 59477 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59477 603 41 0 69483 0
vsize: 278096
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63605 0 0 0 111848 167 0 0 25 0 1 0 482121028 284770304 59479 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69524 59479 603 41 0 69483 0
vsize: 278096
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63610 0 0 0 112848 167 0 0 25 0 1 0 482121028 284905472 59484 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59484 603 41 0 69516 0
vsize: 278228
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63612 0 0 0 113848 167 0 0 25 0 1 0 482121028 284905472 59486 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59486 603 41 0 69516 0
vsize: 278228
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63614 0 0 0 114848 167 0 0 25 0 1 0 482121028 284905472 59488 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59488 603 41 0 69516 0
vsize: 278228
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63616 0 0 0 115848 167 0 0 25 0 1 0 482121028 284905472 59490 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59490 603 41 0 69516 0
vsize: 278228
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63617 0 0 0 116848 167 0 0 25 0 1 0 482121028 284905472 59491 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59491 603 41 0 69516 0
vsize: 278228
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63623 0 0 0 117848 167 0 0 25 0 1 0 482121028 284905472 59497 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59497 603 41 0 69516 0
vsize: 278228
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63625 0 0 0 118848 167 0 0 25 0 1 0 482121028 284905472 59499 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59499 603 41 0 69516 0
vsize: 278228
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 25683
Raw data (stat): 25683 (minisat+) R 25682 30701 30700 0 -1 0 63625 0 0 0 119849 167 0 0 25 0 1 0 482121028 284905472 59499 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69557 59499 603 41 0 69516 0
vsize: 278228
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 25683
Raw data (stat): 25683 (minisat+) Z 25682 30701 30700 0 -1 12 63627 0 0 0 119849 179 0 0 25 0 1 0 482121028 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.13
CPU time (s): 1200.28
CPU user time (s): 1198.49
CPU system time (s): 1.79073
CPU usage (%): 100.013
Max. virtual memory (Kb): 278228
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####