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 13858

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-20 22:04:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20272 boxname=wulflinc2 idbench=1560 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-sp98ic.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-sp98ic.opb
IDLAUNCH: 20272
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        489544 kB
Buffers:         35804 kB
Cached:         484600 kB
SwapCached:          0 kB
Active:         141548 kB
Inactive:       381688 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        489292 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            16020 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:24:35 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 20272 7 1200.36 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 | 1612556  5358940 |  537518       0        0     nan |  0.000 % |
c |       100 | 1612556  5358940 |  591269     100      358     3.6 |  0.153 % |
c |       251 | 1612545  5358913 |  650396     249     1184     4.8 |  0.154 % |
c |       477 | 1612483  5358733 |  715436     425     1871     4.4 |  0.157 % |
c |       816 | 1612407  5358505 |  786980     673     3074     4.6 |  0.161 % |
c |      1330 | 1612401  5358493 |  865678    1186     5196     4.4 |  0.162 % |
c |      2089 | 1612261  5358079 |  952245    1814     8334     4.6 |  0.170 % |
c |      3228 | 1611909  5357029 | 1047470    2658    12229     4.6 |  0.185 % |
c |      4939 | 1611387  5355431 | 1152217    4193    21511     5.1 |  0.212 % |
c |      7501 | 1610810  5353702 | 1267439    6129    30616     5.0 |  0.243 % |
c |     11346 | 1610060  5351408 | 1394183    9611    49637     5.2 |  0.281 % |
c |     17113 | 1609854  5350770 | 1533601   15286   102328     6.7 |  0.290 % |
c |     25762 | 1609239  5348845 | 1686961   23709   187289     7.9 |  0.317 % |
c |     38736 | 1608577  5346827 | 1855657   36413   365690    10.0 |  0.351 % |
c |     58199 | 1607386  5342910 | 2041223   55516   546629     9.8 |  0.390 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.95 2/54 13700
Raw data (stat): 13700 (runsolver) R 13699 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481677603 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 17171 0 0 0 952 46 0 0 25 0 1 0 481677603 61100032 13361 4294967295 134512640 134672761 3221224624 3221222972 1075349905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14917 13361 603 41 0 14876 0
vsize: 59668
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 51191 0 0 0 1867 130 0 0 25 0 1 0 481677603 232435712 47067 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56747 47067 603 41 0 56706 0
vsize: 226988
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 51319 0 0 0 2867 131 0 0 25 0 1 0 481677603 233119744 47195 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56914 47195 603 41 0 56873 0
vsize: 227656
[startup+40.0025 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 51645 0 0 0 3866 132 0 0 25 0 1 0 481677603 234463232 47521 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57242 47521 603 41 0 57201 0
vsize: 228968
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 52367 0 0 0 4864 133 0 0 25 0 1 0 481677603 237301760 48243 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57935 48243 603 41 0 57894 0
vsize: 231740
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 52563 0 0 0 5864 134 0 0 25 0 1 0 481677603 238112768 48439 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58133 48439 603 41 0 58092 0
vsize: 232532
[startup+70.002 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 13700
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 53749 0 0 0 6861 137 0 0 25 0 1 0 481677603 243105792 49625 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59352 49625 603 41 0 59311 0
vsize: 237408
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 54463 0 0 0 7857 140 0 0 25 0 1 0 481677603 245538816 50339 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59946 50339 603 41 0 59905 0
vsize: 239784
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 54577 0 0 0 8857 140 0 0 25 0 1 0 481677603 245944320 50453 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60045 50453 603 41 0 60004 0
vsize: 240180
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 54673 0 0 0 9856 141 0 0 25 0 1 0 481677603 246349824 50549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60144 50549 603 41 0 60103 0
vsize: 240576
[startup+110.021 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 54847 0 0 0 10857 142 0 0 25 0 1 0 481677603 247160832 50723 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60342 50723 603 41 0 60301 0
vsize: 241368
[startup+120.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 54958 0 0 0 11857 142 0 0 25 0 1 0 481677603 247566336 50834 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60441 50834 603 41 0 60400 0
vsize: 241764
[startup+130.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55028 0 0 0 12856 143 0 0 25 0 1 0 481677603 247836672 50904 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60507 50904 603 41 0 60466 0
vsize: 242028
[startup+140.052 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55080 0 0 0 13858 144 0 0 25 0 1 0 481677603 247971840 50956 4294967295 134512640 134672761 3221224624 3221223792 134560748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60540 50956 603 41 0 60499 0
vsize: 242160
[startup+150.079 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55136 0 0 0 14860 144 0 0 25 0 1 0 481677603 248242176 51012 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60606 51012 603 41 0 60565 0
vsize: 242424
[startup+160.079 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55192 0 0 0 15860 145 0 0 25 0 1 0 481677603 248377344 51068 4294967295 134512640 134672761 3221224624 3221223792 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60639 51068 603 41 0 60598 0
vsize: 242556
[startup+170.079 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55247 0 0 0 16860 145 0 0 25 0 1 0 481677603 248647680 51123 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60705 51123 603 41 0 60664 0
vsize: 242820
[startup+180.079 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55302 0 0 0 17860 145 0 0 25 0 1 0 481677603 248782848 51178 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60738 51178 603 41 0 60697 0
vsize: 242952
[startup+190.081 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55317 0 0 0 18860 145 0 0 25 0 1 0 481677603 248918016 51193 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60771 51193 603 41 0 60730 0
vsize: 243084
[startup+200.081 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55348 0 0 0 19860 145 0 0 25 0 1 0 481677603 249053184 51224 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60804 51224 603 41 0 60763 0
vsize: 243216
[startup+210.082 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55374 0 0 0 20861 145 0 0 25 0 1 0 481677603 249053184 51250 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60804 51250 603 41 0 60763 0
vsize: 243216
[startup+220.084 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55377 0 0 0 21861 145 0 0 25 0 1 0 481677603 249053184 51253 4294967295 134512640 134672761 3221224624 3221223796 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60804 51253 603 41 0 60763 0
vsize: 243216
[startup+230.084 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55395 0 0 0 22861 145 0 0 25 0 1 0 481677603 249188352 51271 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60837 51271 603 41 0 60796 0
vsize: 243348
[startup+240.084 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55406 0 0 0 23861 145 0 0 25 0 1 0 481677603 249188352 51282 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60837 51282 603 41 0 60796 0
vsize: 243348
[startup+250.087 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55419 0 0 0 24862 145 0 0 25 0 1 0 481677603 249188352 51295 4294967295 134512640 134672761 3221224624 3221223796 134556658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60837 51295 603 41 0 60796 0
vsize: 243348
[startup+260.091 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55432 0 0 0 25862 145 0 0 25 0 1 0 481677603 249323520 51308 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60870 51308 603 41 0 60829 0
vsize: 243480
[startup+270.091 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55439 0 0 0 26862 145 0 0 25 0 1 0 481677603 249323520 51315 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60870 51315 603 41 0 60829 0
vsize: 243480
[startup+280.091 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55476 0 0 0 27862 145 0 0 25 0 1 0 481677603 249323520 51352 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60870 51352 603 41 0 60829 0
vsize: 243480
[startup+290.092 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55488 0 0 0 28863 145 0 0 25 0 1 0 481677603 249483264 51364 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60909 51364 603 41 0 60868 0
vsize: 243636
[startup+300.092 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55518 0 0 0 29863 146 0 0 25 0 1 0 481677603 249483264 51394 4294967295 134512640 134672761 3221224624 3221223748 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60909 51394 603 41 0 60868 0
vsize: 243636
[startup+310.092 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55524 0 0 0 30863 146 0 0 25 0 1 0 481677603 249483264 51400 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60909 51400 603 41 0 60868 0
vsize: 243636
[startup+320.092 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55542 0 0 0 31863 146 0 0 25 0 1 0 481677603 249483264 51418 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60909 51418 603 41 0 60868 0
vsize: 243636
[startup+330.098 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55650 0 0 0 32863 146 0 0 25 0 1 0 481677603 249618432 51526 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60942 51526 603 41 0 60901 0
vsize: 243768
[startup+340.097 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55681 0 0 0 33863 146 0 0 25 0 1 0 481677603 249618432 51557 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60942 51557 603 41 0 60901 0
vsize: 243768
[startup+350.097 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55705 0 0 0 34863 146 0 0 25 0 1 0 481677603 249753600 51581 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60975 51581 603 41 0 60934 0
vsize: 243900
[startup+360.098 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55724 0 0 0 35864 146 0 0 25 0 1 0 481677603 249888768 51600 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61008 51600 603 41 0 60967 0
vsize: 244032
[startup+370.098 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55740 0 0 0 36864 146 0 0 25 0 1 0 481677603 249888768 51616 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61008 51616 603 41 0 60967 0
vsize: 244032
[startup+380.099 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55753 0 0 0 37864 146 0 0 25 0 1 0 481677603 249888768 51629 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61008 51629 603 41 0 60967 0
vsize: 244032
[startup+390.098 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55784 0 0 0 38864 146 0 0 25 0 1 0 481677603 250187776 51660 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61081 51660 603 41 0 61040 0
vsize: 244324
[startup+400.098 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55784 0 0 0 39864 146 0 0 25 0 1 0 481677603 250187776 51660 4294967295 134512640 134672761 3221224624 3221223748 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61081 51660 603 41 0 61040 0
vsize: 244324
[startup+410.097 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55807 0 0 0 40864 146 0 0 25 0 1 0 481677603 250187776 51683 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61081 51683 603 41 0 61040 0
vsize: 244324
[startup+420.097 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55818 0 0 0 41864 146 0 0 25 0 1 0 481677603 250187776 51694 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61081 51694 603 41 0 61040 0
vsize: 244324
[startup+430.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55856 0 0 0 42865 147 0 0 25 0 1 0 481677603 250318848 51732 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61113 51732 603 41 0 61072 0
vsize: 244452
[startup+440.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55864 0 0 0 43865 147 0 0 25 0 1 0 481677603 250454016 51740 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61146 51740 603 41 0 61105 0
vsize: 244584
[startup+450.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55881 0 0 0 44865 147 0 0 25 0 1 0 481677603 250454016 51757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61146 51757 603 41 0 61105 0
vsize: 244584
[startup+460.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55890 0 0 0 45866 147 0 0 25 0 1 0 481677603 250454016 51766 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61146 51766 603 41 0 61105 0
vsize: 244584
[startup+470.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55904 0 0 0 46866 147 0 0 25 0 1 0 481677603 250589184 51780 4294967295 134512640 134672761 3221224624 3221223804 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61179 51780 603 41 0 61138 0
vsize: 244716
[startup+480.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55919 0 0 0 47866 147 0 0 25 0 1 0 481677603 250589184 51795 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61179 51795 603 41 0 61138 0
vsize: 244716
[startup+490.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55931 0 0 0 48866 147 0 0 25 0 1 0 481677603 250589184 51807 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61179 51807 603 41 0 61138 0
vsize: 244716
[startup+500.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55939 0 0 0 49866 147 0 0 25 0 1 0 481677603 250724352 51815 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61212 51815 603 41 0 61171 0
vsize: 244848
[startup+510.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55948 0 0 0 50866 147 0 0 25 0 1 0 481677603 250724352 51824 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61212 51824 603 41 0 61171 0
vsize: 244848
[startup+520.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55966 0 0 0 51866 147 0 0 25 0 1 0 481677603 250724352 51842 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61212 51842 603 41 0 61171 0
vsize: 244848
[startup+530.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 55995 0 0 0 52866 147 0 0 25 0 1 0 481677603 250859520 51871 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61245 51871 603 41 0 61204 0
vsize: 244980
[startup+540.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56009 0 0 0 53866 147 0 0 25 0 1 0 481677603 250994688 51885 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61278 51885 603 41 0 61237 0
vsize: 245112
[startup+550.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56025 0 0 0 54866 147 0 0 25 0 1 0 481677603 250994688 51901 4294967295 134512640 134672761 3221224624 3221223816 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61278 51901 603 41 0 61237 0
vsize: 245112
[startup+560.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56037 0 0 0 55867 147 0 0 25 0 1 0 481677603 251129856 51913 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61311 51913 603 41 0 61270 0
vsize: 245244
[startup+570.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56043 0 0 0 56867 147 0 0 25 0 1 0 481677603 251129856 51919 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61311 51919 603 41 0 61270 0
vsize: 245244
[startup+580.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56055 0 0 0 57867 147 0 0 25 0 1 0 481677603 251129856 51931 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61311 51931 603 41 0 61270 0
vsize: 245244
[startup+590.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56072 0 0 0 58867 147 0 0 25 0 1 0 481677603 251265024 51948 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61344 51948 603 41 0 61303 0
vsize: 245376
[startup+600.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56117 0 0 0 59867 147 0 0 25 0 1 0 481677603 251527168 51993 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61408 51993 603 41 0 61367 0
vsize: 245632
[startup+610.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56191 0 0 0 60867 147 0 0 25 0 1 0 481677603 251797504 52067 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61474 52067 603 41 0 61433 0
vsize: 245896
[startup+620.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56216 0 0 0 61867 147 0 0 25 0 1 0 481677603 251932672 52092 4294967295 134512640 134672761 3221224624 3221223808 134557980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61507 52092 603 41 0 61466 0
vsize: 246028
[startup+630.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56240 0 0 0 62867 147 0 0 25 0 1 0 481677603 251932672 52116 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61507 52116 603 41 0 61466 0
vsize: 246028
[startup+640.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56250 0 0 0 63867 147 0 0 25 0 1 0 481677603 252067840 52126 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61540 52126 603 41 0 61499 0
vsize: 246160
[startup+650.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56263 0 0 0 64867 147 0 0 25 0 1 0 481677603 252067840 52139 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61540 52139 603 41 0 61499 0
vsize: 246160
[startup+660.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56281 0 0 0 65867 147 0 0 25 0 1 0 481677603 252067840 52157 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61540 52157 603 41 0 61499 0
vsize: 246160
[startup+670.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56346 0 0 0 66867 148 0 0 25 0 1 0 481677603 252338176 52222 4294967295 134512640 134672761 3221224624 3221223820 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61606 52222 603 41 0 61565 0
vsize: 246424
[startup+680.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56353 0 0 0 67867 148 0 0 25 0 1 0 481677603 252473344 52229 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61639 52229 603 41 0 61598 0
vsize: 246556
[startup+690.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56364 0 0 0 68867 148 0 0 25 0 1 0 481677603 252473344 52240 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61639 52240 603 41 0 61598 0
vsize: 246556
[startup+700.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56379 0 0 0 69867 148 0 0 25 0 1 0 481677603 252473344 52255 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61639 52255 603 41 0 61598 0
vsize: 246556
[startup+710.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56400 0 0 0 70867 148 0 0 25 0 1 0 481677603 252608512 52276 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 52276 603 41 0 61631 0
vsize: 246688
[startup+720.108 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56413 0 0 0 71868 148 0 0 25 0 1 0 481677603 252608512 52289 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 52289 603 41 0 61631 0
vsize: 246688
[startup+730.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56431 0 0 0 72868 148 0 0 25 0 1 0 481677603 252743680 52307 4294967295 134512640 134672761 3221224624 3221223792 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61705 52307 603 41 0 61664 0
vsize: 246820
[startup+740.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56445 0 0 0 73868 148 0 0 25 0 1 0 481677603 252743680 52321 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61705 52321 603 41 0 61664 0
vsize: 246820
[startup+750.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56458 0 0 0 74868 148 0 0 25 0 1 0 481677603 252878848 52334 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61738 52334 603 41 0 61697 0
vsize: 246952
[startup+760.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56468 0 0 0 75868 149 0 0 25 0 1 0 481677603 252878848 52344 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61738 52344 603 41 0 61697 0
vsize: 246952
[startup+770.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56483 0 0 0 76869 149 0 0 25 0 1 0 481677603 252878848 52359 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61738 52359 603 41 0 61697 0
vsize: 246952
[startup+780.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56492 0 0 0 77869 149 0 0 25 0 1 0 481677603 252878848 52368 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61738 52368 603 41 0 61697 0
vsize: 246952
[startup+790.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56506 0 0 0 78869 149 0 0 25 0 1 0 481677603 253009920 52382 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61770 52382 603 41 0 61729 0
vsize: 247080
[startup+800.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56514 0 0 0 79869 149 0 0 25 0 1 0 481677603 253009920 52390 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61770 52390 603 41 0 61729 0
vsize: 247080
[startup+810.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56522 0 0 0 80869 149 0 0 25 0 1 0 481677603 253009920 52398 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61770 52398 603 41 0 61729 0
vsize: 247080
[startup+820.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56528 0 0 0 81868 149 0 0 25 0 1 0 481677603 253009920 52404 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61770 52404 603 41 0 61729 0
vsize: 247080
[startup+830.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56541 0 0 0 82869 149 0 0 25 0 1 0 481677603 253145088 52417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61803 52417 603 41 0 61762 0
vsize: 247212
[startup+840.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56557 0 0 0 83869 149 0 0 25 0 1 0 481677603 253145088 52433 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61803 52433 603 41 0 61762 0
vsize: 247212
[startup+850.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56568 0 0 0 84869 149 0 0 25 0 1 0 481677603 253145088 52444 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61803 52444 603 41 0 61762 0
vsize: 247212
[startup+860.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56574 0 0 0 85869 149 0 0 25 0 1 0 481677603 253280256 52450 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61836 52450 603 41 0 61795 0
vsize: 247344
[startup+870.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56584 0 0 0 86869 149 0 0 25 0 1 0 481677603 253280256 52460 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61836 52460 603 41 0 61795 0
vsize: 247344
[startup+880.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56600 0 0 0 87869 150 0 0 25 0 1 0 481677603 253280256 52476 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61836 52476 603 41 0 61795 0
vsize: 247344
[startup+890.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56612 0 0 0 88869 150 0 0 25 0 1 0 481677603 253415424 52488 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61869 52488 603 41 0 61828 0
vsize: 247476
[startup+900.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56620 0 0 0 89869 150 0 0 25 0 1 0 481677603 253415424 52496 4294967295 134512640 134672761 3221224624 3221223808 134559559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61869 52496 603 41 0 61828 0
vsize: 247476
[startup+910.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56630 0 0 0 90869 150 0 0 25 0 1 0 481677603 253415424 52506 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61869 52506 603 41 0 61828 0
vsize: 247476
[startup+920.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56641 0 0 0 91869 150 0 0 25 0 1 0 481677603 253550592 52517 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61902 52517 603 41 0 61861 0
vsize: 247608
[startup+930.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56654 0 0 0 92869 150 0 0 25 0 1 0 481677603 253550592 52530 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61902 52530 603 41 0 61861 0
vsize: 247608
[startup+940.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56665 0 0 0 93869 150 0 0 25 0 1 0 481677603 253550592 52541 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61902 52541 603 41 0 61861 0
vsize: 247608
[startup+950.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56674 0 0 0 94869 150 0 0 25 0 1 0 481677603 253685760 52550 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61935 52550 603 41 0 61894 0
vsize: 247740
[startup+960.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56680 0 0 0 95870 150 0 0 25 0 1 0 481677603 253685760 52556 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61935 52556 603 41 0 61894 0
vsize: 247740
[startup+970.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56703 0 0 0 96870 150 0 0 25 0 1 0 481677603 253685760 52579 4294967295 134512640 134672761 3221224624 3221223840 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61935 52579 603 41 0 61894 0
vsize: 247740
[startup+980.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56715 0 0 0 97870 150 0 0 25 0 1 0 481677603 253820928 52591 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61968 52591 603 41 0 61927 0
vsize: 247872
[startup+990.116 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56724 0 0 0 98870 150 0 0 25 0 1 0 481677603 253820928 52600 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61968 52600 603 41 0 61927 0
vsize: 247872
[startup+1000.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56732 0 0 0 99870 150 0 0 25 0 1 0 481677603 253820928 52608 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61968 52608 603 41 0 61927 0
vsize: 247872
[startup+1010.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56737 0 0 0 100870 150 0 0 25 0 1 0 481677603 253820928 52613 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61968 52613 603 41 0 61927 0
vsize: 247872
[startup+1020.12 s]
Raw data (loadavg): 1.00 1.00 0.95 3/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56739 0 0 0 101870 150 0 0 25 0 1 0 481677603 253820928 52615 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61968 52615 603 41 0 61927 0
vsize: 247872
[startup+1030.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56750 0 0 0 102870 151 0 0 25 0 1 0 481677603 254218240 52626 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62065 52626 603 41 0 62024 0
vsize: 248260
[startup+1040.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56753 0 0 0 103871 151 0 0 25 0 1 0 481677603 254218240 52629 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62065 52629 603 41 0 62024 0
vsize: 248260
[startup+1050.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56765 0 0 0 104871 151 0 0 25 0 1 0 481677603 254218240 52641 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62065 52641 603 41 0 62024 0
vsize: 248260
[startup+1060.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56783 0 0 0 105871 151 0 0 25 0 1 0 481677603 254218240 52659 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62065 52659 603 41 0 62024 0
vsize: 248260
[startup+1070.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56809 0 0 0 106871 151 0 0 25 0 1 0 481677603 254353408 52685 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62098 52685 603 41 0 62057 0
vsize: 248392
[startup+1080.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56818 0 0 0 107871 151 0 0 25 0 1 0 481677603 254353408 52694 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62098 52694 603 41 0 62057 0
vsize: 248392
[startup+1090.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56827 0 0 0 108872 151 0 0 25 0 1 0 481677603 254488576 52703 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62131 52703 603 41 0 62090 0
vsize: 248524
[startup+1100.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56838 0 0 0 109872 151 0 0 25 0 1 0 481677603 254488576 52714 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62131 52714 603 41 0 62090 0
vsize: 248524
[startup+1110.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56849 0 0 0 110872 151 0 0 25 0 1 0 481677603 254488576 52725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62131 52725 603 41 0 62090 0
vsize: 248524
[startup+1120.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56911 0 0 0 111872 151 0 0 25 0 1 0 481677603 254623744 52787 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62164 52787 603 41 0 62123 0
vsize: 248656
[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56952 0 0 0 112872 151 0 0 25 0 1 0 481677603 254623744 52828 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62164 52828 603 41 0 62123 0
vsize: 248656
[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56969 0 0 0 113872 151 0 0 25 0 1 0 481677603 254758912 52845 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62197 52845 603 41 0 62156 0
vsize: 248788
[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56979 0 0 0 114872 151 0 0 25 0 1 0 481677603 254758912 52855 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62197 52855 603 41 0 62156 0
vsize: 248788
[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 56993 0 0 0 115872 151 0 0 25 0 1 0 481677603 254758912 52869 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62197 52869 603 41 0 62156 0
vsize: 248788
[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 57007 0 0 0 116872 151 0 0 25 0 1 0 481677603 254894080 52883 4294967295 134512640 134672761 3221224624 3221223824 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62230 52883 603 41 0 62189 0
vsize: 248920
[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 57027 0 0 0 117872 152 0 0 25 0 1 0 481677603 254894080 52903 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62230 52903 603 41 0 62189 0
vsize: 248920
[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 57061 0 0 0 118872 152 0 0 25 0 1 0 481677603 255029248 52937 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62263 52937 603 41 0 62222 0
vsize: 249052
[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 13702
Raw data (stat): 13700 (minisat+) R 13699 20937 20936 0 -1 0 57136 0 0 0 119872 152 0 0 25 0 1 0 481677603 255299584 53012 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62329 53012 603 41 0 62288 0
vsize: 249316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 13702
Raw data (stat): 13700 (minisat+) Z 13699 20937 20936 0 -1 12 57138 0 0 0 119873 162 0 0 25 0 1 0 481677603 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.22
CPU time (s): 1200.36
CPU user time (s): 1198.73
CPU system time (s): 1.62675
CPU usage (%): 100.011
Max. virtual memory (Kb): 249316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####