PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-20 20:21:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15267 boxname=wulflinc2 idbench=1175 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-sp98ic.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-sp98ic.opb
IDLAUNCH: 15267
/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:        557512 kB
Buffers:         35644 kB
Cached:         417304 kB
SwapCached:          0 kB
Active:         128892 kB
Inactive:       326892 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        557260 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            15772 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 20:41:21 (client local time) WITH STATUS 0 IN 1200.56 SECONDS
stats: 15267 7 1200.56 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.74 0.47 0.20 1/54 12396
Raw data (stat): 12396 (runsolver) R 12395 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481058136 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+10.0016 s]
Raw data (loadavg): 0.78 0.49 0.21 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 17171 0 0 0 951 42 0 0 25 0 1 0 481058136 61100032 13361 4294967295 134512640 134672761 3221224624 3221222608 134522444 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.0028 s]
Raw data (loadavg): 0.81 0.50 0.21 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 51156 0 0 0 1865 127 0 0 25 0 1 0 481058136 232300544 47032 4294967295 134512640 134672761 3221224624 3221223868 134564647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56714 47032 603 41 0 56673 0
vsize: 226856
[startup+30.0223 s]
Raw data (loadavg): 0.84 0.52 0.22 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 51319 0 0 0 2866 127 0 0 25 0 1 0 481058136 233119744 47195 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56914 47195 603 41 0 56873 0
vsize: 227656
[startup+40.0425 s]
Raw data (loadavg): 0.86 0.53 0.23 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 51645 0 0 0 3867 128 0 0 25 0 1 0 481058136 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.0491 s]
Raw data (loadavg): 0.88 0.55 0.24 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 52367 0 0 0 4866 130 0 0 25 0 1 0 481058136 237301760 48243 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57935 48243 603 41 0 57894 0
vsize: 231740
[startup+60.0497 s]
Raw data (loadavg): 0.90 0.56 0.24 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 52563 0 0 0 5865 130 0 0 25 0 1 0 481058136 238112768 48439 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58133 48439 603 41 0 58092 0
vsize: 232532
[startup+70.0643 s]
Raw data (loadavg): 0.92 0.58 0.25 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 53749 0 0 0 6864 133 0 0 25 0 1 0 481058136 243105792 49625 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59352 49625 603 41 0 59311 0
vsize: 237408
[startup+80.0871 s]
Raw data (loadavg): 0.93 0.59 0.26 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 54464 0 0 0 7864 135 0 0 25 0 1 0 481058136 245538816 50340 4294967295 134512640 134672761 3221224624 3221223840 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59946 50340 603 41 0 59905 0
vsize: 239784
[startup+90.1122 s]
Raw data (loadavg): 0.94 0.60 0.27 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 54584 0 0 0 8865 136 0 0 25 0 1 0 481058136 246079488 50460 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60078 50460 603 41 0 60037 0
vsize: 240312
[startup+100.127 s]
Raw data (loadavg): 0.95 0.62 0.28 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 54673 0 0 0 9866 136 0 0 25 0 1 0 481058136 246349824 50549 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60144 50549 603 41 0 60103 0
vsize: 240576
[startup+110.136 s]
Raw data (loadavg): 0.95 0.63 0.28 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 54847 0 0 0 10865 137 0 0 25 0 1 0 481058136 247160832 50723 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60342 50723 603 41 0 60301 0
vsize: 241368
[startup+120.143 s]
Raw data (loadavg): 0.96 0.64 0.29 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 54958 0 0 0 11864 137 0 0 25 0 1 0 481058136 247566336 50834 4294967295 134512640 134672761 3221224624 3221223768 134566157 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.155 s]
Raw data (loadavg): 0.97 0.65 0.30 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55028 0 0 0 12866 138 0 0 25 0 1 0 481058136 247836672 50904 4294967295 134512640 134672761 3221224624 3221223796 134556658 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.16 s]
Raw data (loadavg): 0.97 0.66 0.30 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55080 0 0 0 13866 138 0 0 25 0 1 0 481058136 247971840 50956 4294967295 134512640 134672761 3221224624 3221223888 134562158 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.274 s]
Raw data (loadavg): 0.98 0.67 0.31 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55136 0 0 0 14877 138 0 0 25 0 1 0 481058136 248242176 51012 4294967295 134512640 134672761 3221224624 3221223840 134561990 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.28 s]
Raw data (loadavg): 0.98 0.68 0.32 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55193 0 0 0 15878 138 0 0 25 0 1 0 481058136 248377344 51069 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60639 51069 603 41 0 60598 0
vsize: 242556
[startup+170.28 s]
Raw data (loadavg): 0.98 0.69 0.32 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55247 0 0 0 16878 139 0 0 25 0 1 0 481058136 248647680 51123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60705 51123 603 41 0 60664 0
vsize: 242820
[startup+180.28 s]
Raw data (loadavg): 0.98 0.70 0.33 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55302 0 0 0 17878 139 0 0 25 0 1 0 481058136 248782848 51178 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60738 51178 603 41 0 60697 0
vsize: 242952
[startup+190.294 s]
Raw data (loadavg): 0.99 0.71 0.34 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55317 0 0 0 18880 139 0 0 25 0 1 0 481058136 248918016 51193 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60771 51193 603 41 0 60730 0
vsize: 243084
[startup+200.294 s]
Raw data (loadavg): 0.99 0.72 0.34 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55349 0 0 0 19880 139 0 0 25 0 1 0 481058136 249053184 51225 4294967295 134512640 134672761 3221224624 3221223564 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60804 51225 603 41 0 60763 0
vsize: 243216
[startup+210.295 s]
Raw data (loadavg): 0.99 0.73 0.35 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55375 0 0 0 20880 139 0 0 25 0 1 0 481058136 249053184 51251 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60804 51251 603 41 0 60763 0
vsize: 243216
[startup+220.296 s]
Raw data (loadavg): 0.99 0.74 0.36 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55378 0 0 0 21880 139 0 0 25 0 1 0 481058136 249053184 51254 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60804 51254 603 41 0 60763 0
vsize: 243216
[startup+230.305 s]
Raw data (loadavg): 0.99 0.75 0.36 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55397 0 0 0 22881 139 0 0 25 0 1 0 481058136 249188352 51273 4294967295 134512640 134672761 3221224624 3221223776 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60837 51273 603 41 0 60796 0
vsize: 243348
[startup+240.305 s]
Raw data (loadavg): 0.99 0.75 0.37 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55407 0 0 0 23881 139 0 0 25 0 1 0 481058136 249188352 51283 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60837 51283 603 41 0 60796 0
vsize: 243348
[startup+250.305 s]
Raw data (loadavg): 0.99 0.76 0.38 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55419 0 0 0 24882 139 0 0 25 0 1 0 481058136 249188352 51295 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60837 51295 603 41 0 60796 0
vsize: 243348
[startup+260.311 s]
Raw data (loadavg): 0.99 0.77 0.38 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55433 0 0 0 25882 139 0 0 25 0 1 0 481058136 249323520 51309 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60870 51309 603 41 0 60829 0
vsize: 243480
[startup+270.311 s]
Raw data (loadavg): 0.99 0.78 0.39 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55440 0 0 0 26883 139 0 0 25 0 1 0 481058136 249323520 51316 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60870 51316 603 41 0 60829 0
vsize: 243480
[startup+280.311 s]
Raw data (loadavg): 0.99 0.78 0.39 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55477 0 0 0 27883 139 0 0 25 0 1 0 481058136 249323520 51353 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60870 51353 603 41 0 60829 0
vsize: 243480
[startup+290.329 s]
Raw data (loadavg): 0.99 0.79 0.40 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55488 0 0 0 28885 139 0 0 25 0 1 0 481058136 249483264 51364 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60909 51364 603 41 0 60868 0
vsize: 243636
[startup+300.328 s]
Raw data (loadavg): 0.99 0.80 0.41 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55521 0 0 0 29885 139 0 0 25 0 1 0 481058136 249483264 51397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60909 51397 603 41 0 60868 0
vsize: 243636
[startup+310.329 s]
Raw data (loadavg): 0.99 0.80 0.41 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55526 0 0 0 30885 139 0 0 25 0 1 0 481058136 249483264 51402 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60909 51402 603 41 0 60868 0
vsize: 243636
[startup+320.329 s]
Raw data (loadavg): 0.99 0.81 0.42 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55545 0 0 0 31885 139 0 0 25 0 1 0 481058136 249483264 51421 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60909 51421 603 41 0 60868 0
vsize: 243636
[startup+330.329 s]
Raw data (loadavg): 0.99 0.81 0.42 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55653 0 0 0 32885 139 0 0 25 0 1 0 481058136 249618432 51529 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60942 51529 603 41 0 60901 0
vsize: 243768
[startup+340.329 s]
Raw data (loadavg): 0.99 0.82 0.43 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55685 0 0 0 33885 139 0 0 25 0 1 0 481058136 249618432 51561 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60942 51561 603 41 0 60901 0
vsize: 243768
[startup+350.329 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55709 0 0 0 34885 139 0 0 25 0 1 0 481058136 249753600 51585 4294967295 134512640 134672761 3221224624 3221223788 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60975 51585 603 41 0 60934 0
vsize: 243900
[startup+360.329 s]
Raw data (loadavg): 0.99 0.83 0.44 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55728 0 0 0 35885 139 0 0 25 0 1 0 481058136 249888768 51604 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61008 51604 603 41 0 60967 0
vsize: 244032
[startup+370.329 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55746 0 0 0 36885 139 0 0 25 0 1 0 481058136 249888768 51622 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61008 51622 603 41 0 60967 0
vsize: 244032
[startup+380.329 s]
Raw data (loadavg): 0.99 0.84 0.45 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55760 0 0 0 37885 140 0 0 25 0 1 0 481058136 250023936 51636 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61041 51636 603 41 0 61000 0
vsize: 244164
[startup+390.328 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55784 0 0 0 38885 140 0 0 25 0 1 0 481058136 250187776 51660 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61081 51660 603 41 0 61040 0
vsize: 244324
[startup+400.328 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55785 0 0 0 39886 140 0 0 25 0 1 0 481058136 250187776 51661 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61081 51661 603 41 0 61040 0
vsize: 244324
[startup+410.329 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55808 0 0 0 40886 140 0 0 25 0 1 0 481058136 250187776 51684 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61081 51684 603 41 0 61040 0
vsize: 244324
[startup+420.329 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55847 0 0 0 41886 140 0 0 25 0 1 0 481058136 250318848 51723 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61113 51723 603 41 0 61072 0
vsize: 244452
[startup+430.329 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55861 0 0 0 42886 140 0 0 25 0 1 0 481058136 250318848 51737 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61113 51737 603 41 0 61072 0
vsize: 244452
[startup+440.329 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55868 0 0 0 43886 140 0 0 25 0 1 0 481058136 250454016 51744 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61146 51744 603 41 0 61105 0
vsize: 244584
[startup+450.329 s]
Raw data (loadavg): 0.99 0.87 0.49 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55882 0 0 0 44886 140 0 0 25 0 1 0 481058136 250454016 51758 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61146 51758 603 41 0 61105 0
vsize: 244584
[startup+460.329 s]
Raw data (loadavg): 0.99 0.87 0.49 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55896 0 0 0 45887 140 0 0 25 0 1 0 481058136 250454016 51772 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61146 51772 603 41 0 61105 0
vsize: 244584
[startup+470.33 s]
Raw data (loadavg): 0.99 0.88 0.50 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55908 0 0 0 46887 140 0 0 25 0 1 0 481058136 250589184 51784 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61179 51784 603 41 0 61138 0
vsize: 244716
[startup+480.33 s]
Raw data (loadavg): 0.99 0.88 0.50 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55927 0 0 0 47886 140 0 0 25 0 1 0 481058136 250589184 51803 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61179 51803 603 41 0 61138 0
vsize: 244716
[startup+490.33 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55934 0 0 0 48887 140 0 0 25 0 1 0 481058136 250724352 51810 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61212 51810 603 41 0 61171 0
vsize: 244848
[startup+500.33 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55941 0 0 0 49887 140 0 0 25 0 1 0 481058136 250724352 51817 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61212 51817 603 41 0 61171 0
vsize: 244848
[startup+510.331 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55954 0 0 0 50887 140 0 0 25 0 1 0 481058136 250724352 51830 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61212 51830 603 41 0 61171 0
vsize: 244848
[startup+520.33 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 55969 0 0 0 51887 140 0 0 25 0 1 0 481058136 250859520 51845 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61245 51845 603 41 0 61204 0
vsize: 244980
[startup+530.331 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56001 0 0 0 52887 140 0 0 25 0 1 0 481058136 250859520 51877 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61245 51877 603 41 0 61204 0
vsize: 244980
[startup+540.331 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56022 0 0 0 53887 141 0 0 25 0 1 0 481058136 250994688 51898 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61278 51898 603 41 0 61237 0
vsize: 245112
[startup+550.331 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56032 0 0 0 54887 141 0 0 25 0 1 0 481058136 250994688 51908 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61278 51908 603 41 0 61237 0
vsize: 245112
[startup+560.331 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56038 0 0 0 55887 141 0 0 25 0 1 0 481058136 251129856 51914 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61311 51914 603 41 0 61270 0
vsize: 245244
[startup+570.332 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56045 0 0 0 56887 141 0 0 25 0 1 0 481058136 251129856 51921 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61311 51921 603 41 0 61270 0
vsize: 245244
[startup+580.332 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56059 0 0 0 57887 141 0 0 25 0 1 0 481058136 251129856 51935 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61311 51935 603 41 0 61270 0
vsize: 245244
[startup+590.332 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56078 0 0 0 58888 141 0 0 25 0 1 0 481058136 251265024 51954 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61344 51954 603 41 0 61303 0
vsize: 245376
[startup+600.331 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56177 0 0 0 59888 141 0 0 25 0 1 0 481058136 251797504 52053 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61474 52053 603 41 0 61433 0
vsize: 245896
[startup+610.332 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56201 0 0 0 60888 141 0 0 25 0 1 0 481058136 251797504 52077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61474 52077 603 41 0 61433 0
vsize: 245896
[startup+620.332 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56233 0 0 0 61887 141 0 0 25 0 1 0 481058136 251932672 52109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61507 52109 603 41 0 61466 0
vsize: 246028
[startup+630.331 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56246 0 0 0 62888 141 0 0 25 0 1 0 481058136 252067840 52122 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61540 52122 603 41 0 61499 0
vsize: 246160
[startup+640.332 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56256 0 0 0 63888 141 0 0 25 0 1 0 481058136 252067840 52132 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61540 52132 603 41 0 61499 0
vsize: 246160
[startup+650.332 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56270 0 0 0 64888 141 0 0 25 0 1 0 481058136 252067840 52146 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61540 52146 603 41 0 61499 0
vsize: 246160
[startup+660.332 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56331 0 0 0 65888 141 0 0 25 0 1 0 481058136 252338176 52207 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61606 52207 603 41 0 61565 0
vsize: 246424
[startup+670.332 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56350 0 0 0 66888 141 0 0 25 0 1 0 481058136 252338176 52226 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61606 52226 603 41 0 61565 0
vsize: 246424
[startup+680.332 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56361 0 0 0 67888 141 0 0 25 0 1 0 481058136 252473344 52237 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61639 52237 603 41 0 61598 0
vsize: 246556
[startup+690.332 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56372 0 0 0 68889 141 0 0 25 0 1 0 481058136 252473344 52248 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61639 52248 603 41 0 61598 0
vsize: 246556
[startup+700.332 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56391 0 0 0 69889 142 0 0 25 0 1 0 481058136 252608512 52267 4294967295 134512640 134672761 3221224624 3221223796 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61672 52267 603 41 0 61631 0
vsize: 246688
[startup+710.356 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56408 0 0 0 70891 142 0 0 25 0 1 0 481058136 252608512 52284 4294967295 134512640 134672761 3221224624 3221223748 134566095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61672 52284 603 41 0 61631 0
vsize: 246688
[startup+720.355 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56423 0 0 0 71891 142 0 0 25 0 1 0 481058136 252743680 52299 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61705 52299 603 41 0 61664 0
vsize: 246820
[startup+730.355 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56440 0 0 0 72891 142 0 0 25 0 1 0 481058136 252743680 52316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61705 52316 603 41 0 61664 0
vsize: 246820
[startup+740.355 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56451 0 0 0 73891 142 0 0 25 0 1 0 481058136 252743680 52327 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61705 52327 603 41 0 61664 0
vsize: 246820
[startup+750.36 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56464 0 0 0 74892 142 0 0 25 0 1 0 481058136 252878848 52340 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61738 52340 603 41 0 61697 0
vsize: 246952
[startup+760.361 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56479 0 0 0 75892 142 0 0 25 0 1 0 481058136 252878848 52355 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61738 52355 603 41 0 61697 0
vsize: 246952
[startup+770.361 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56491 0 0 0 76893 142 0 0 25 0 1 0 481058136 252878848 52367 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61738 52367 603 41 0 61697 0
vsize: 246952
[startup+780.361 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56504 0 0 0 77893 142 0 0 25 0 1 0 481058136 253009920 52380 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61770 52380 603 41 0 61729 0
vsize: 247080
[startup+790.362 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56511 0 0 0 78893 142 0 0 25 0 1 0 481058136 253009920 52387 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61770 52387 603 41 0 61729 0
vsize: 247080
[startup+800.361 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56520 0 0 0 79893 142 0 0 25 0 1 0 481058136 253009920 52396 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61770 52396 603 41 0 61729 0
vsize: 247080
[startup+810.362 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56525 0 0 0 80893 142 0 0 25 0 1 0 481058136 253009920 52401 4294967295 134512640 134672761 3221224624 3221223748 134566142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61770 52401 603 41 0 61729 0
vsize: 247080
[startup+820.364 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56536 0 0 0 81894 142 0 0 25 0 1 0 481058136 253145088 52412 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61803 52412 603 41 0 61762 0
vsize: 247212
[startup+830.364 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56555 0 0 0 82894 142 0 0 25 0 1 0 481058136 253145088 52431 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61803 52431 603 41 0 61762 0
vsize: 247212
[startup+840.365 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56564 0 0 0 83894 142 0 0 25 0 1 0 481058136 253145088 52440 4294967295 134512640 134672761 3221224624 3221223788 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61803 52440 603 41 0 61762 0
vsize: 247212
[startup+850.369 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56573 0 0 0 84895 142 0 0 25 0 1 0 481058136 253280256 52449 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61836 52449 603 41 0 61795 0
vsize: 247344
[startup+860.37 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56582 0 0 0 85895 142 0 0 25 0 1 0 481058136 253280256 52458 4294967295 134512640 134672761 3221224624 3221223792 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61836 52458 603 41 0 61795 0
vsize: 247344
[startup+870.37 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56598 0 0 0 86894 142 0 0 25 0 1 0 481058136 253280256 52474 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61836 52474 603 41 0 61795 0
vsize: 247344
[startup+880.37 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56609 0 0 0 87893 143 0 0 25 0 1 0 481058136 253415424 52485 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61869 52485 603 41 0 61828 0
vsize: 247476
[startup+890.371 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56617 0 0 0 88893 143 0 0 25 0 1 0 481058136 253415424 52493 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61869 52493 603 41 0 61828 0
vsize: 247476
[startup+900.37 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56628 0 0 0 89893 143 0 0 25 0 1 0 481058136 253415424 52504 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61869 52504 603 41 0 61828 0
vsize: 247476
[startup+910.37 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56639 0 0 0 90893 143 0 0 25 0 1 0 481058136 253550592 52515 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61902 52515 603 41 0 61861 0
vsize: 247608
[startup+920.37 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56652 0 0 0 91893 143 0 0 25 0 1 0 481058136 253550592 52528 4294967295 134512640 134672761 3221224624 3221223776 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61902 52528 603 41 0 61861 0
vsize: 247608
[startup+930.37 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56663 0 0 0 92893 143 0 0 25 0 1 0 481058136 253550592 52539 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61902 52539 603 41 0 61861 0
vsize: 247608
[startup+940.37 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56672 0 0 0 93893 143 0 0 25 0 1 0 481058136 253550592 52548 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61902 52548 603 41 0 61861 0
vsize: 247608
[startup+950.375 s]
Raw data (loadavg): 1.07 0.98 0.69 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56679 0 0 0 94894 143 0 0 25 0 1 0 481058136 253685760 52555 4294967295 134512640 134672761 3221224624 3221223840 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61935 52555 603 41 0 61894 0
vsize: 247740
[startup+960.384 s]
Raw data (loadavg): 1.06 0.98 0.69 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56701 0 0 0 95895 143 0 0 25 0 1 0 481058136 253685760 52577 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61935 52577 603 41 0 61894 0
vsize: 247740
[startup+970.385 s]
Raw data (loadavg): 1.05 0.98 0.69 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56713 0 0 0 96895 143 0 0 25 0 1 0 481058136 253820928 52589 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61968 52589 603 41 0 61927 0
vsize: 247872
[startup+980.385 s]
Raw data (loadavg): 1.04 0.98 0.69 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56723 0 0 0 97896 143 0 0 25 0 1 0 481058136 253820928 52599 4294967295 134512640 134672761 3221224624 3221223748 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61968 52599 603 41 0 61927 0
vsize: 247872
[startup+990.392 s]
Raw data (loadavg): 1.11 1.00 0.70 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56732 0 0 0 98896 143 0 0 25 0 1 0 481058136 253820928 52608 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61968 52608 603 41 0 61927 0
vsize: 247872
[startup+1000.39 s]
Raw data (loadavg): 1.16 1.01 0.71 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56736 0 0 0 99897 143 0 0 25 0 1 0 481058136 253820928 52612 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61968 52612 603 41 0 61927 0
vsize: 247872
[startup+1010.39 s]
Raw data (loadavg): 1.14 1.01 0.71 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56739 0 0 0 100897 143 0 0 25 0 1 0 481058136 253820928 52615 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61968 52615 603 41 0 61927 0
vsize: 247872
[startup+1020.39 s]
Raw data (loadavg): 1.12 1.01 0.72 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56750 0 0 0 101897 143 0 0 25 0 1 0 481058136 254218240 52626 4294967295 134512640 134672761 3221224624 3221223792 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62065 52626 603 41 0 62024 0
vsize: 248260
[startup+1030.39 s]
Raw data (loadavg): 1.17 1.03 0.72 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56753 0 0 0 102897 143 0 0 25 0 1 0 481058136 254218240 52629 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62065 52629 603 41 0 62024 0
vsize: 248260
[startup+1040.39 s]
Raw data (loadavg): 1.14 1.02 0.73 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56765 0 0 0 103897 143 0 0 25 0 1 0 481058136 254218240 52641 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62065 52641 603 41 0 62024 0
vsize: 248260
[startup+1050.39 s]
Raw data (loadavg): 1.12 1.02 0.73 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56783 0 0 0 104897 143 0 0 25 0 1 0 481058136 254218240 52659 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62065 52659 603 41 0 62024 0
vsize: 248260
[startup+1060.39 s]
Raw data (loadavg): 1.10 1.02 0.73 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56809 0 0 0 105897 144 0 0 25 0 1 0 481058136 254353408 52685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62098 52685 603 41 0 62057 0
vsize: 248392
[startup+1070.39 s]
Raw data (loadavg): 1.09 1.02 0.73 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56819 0 0 0 106897 144 0 0 25 0 1 0 481058136 254488576 52695 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62131 52695 603 41 0 62090 0
vsize: 248524
[startup+1080.39 s]
Raw data (loadavg): 1.07 1.02 0.74 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56827 0 0 0 107897 144 0 0 25 0 1 0 481058136 254488576 52703 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62131 52703 603 41 0 62090 0
vsize: 248524
[startup+1090.39 s]
Raw data (loadavg): 1.06 1.02 0.74 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56839 0 0 0 108898 144 0 0 25 0 1 0 481058136 254488576 52715 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62131 52715 603 41 0 62090 0
vsize: 248524
[startup+1100.39 s]
Raw data (loadavg): 1.05 1.02 0.74 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56849 0 0 0 109898 144 0 0 25 0 1 0 481058136 254488576 52725 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62131 52725 603 41 0 62090 0
vsize: 248524
[startup+1110.39 s]
Raw data (loadavg): 1.04 1.02 0.74 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56935 0 0 0 110898 144 0 0 25 0 1 0 481058136 254623744 52811 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62164 52811 603 41 0 62123 0
vsize: 248656
[startup+1120.39 s]
Raw data (loadavg): 1.04 1.02 0.74 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56955 0 0 0 111898 144 0 0 25 0 1 0 481058136 254623744 52831 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62164 52831 603 41 0 62123 0
vsize: 248656
[startup+1130.4 s]
Raw data (loadavg): 1.03 1.02 0.75 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56971 0 0 0 112898 144 0 0 25 0 1 0 481058136 254758912 52847 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62197 52847 603 41 0 62156 0
vsize: 248788
[startup+1140.4 s]
Raw data (loadavg): 1.02 1.01 0.75 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56980 0 0 0 113898 144 0 0 25 0 1 0 481058136 254758912 52856 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62197 52856 603 41 0 62156 0
vsize: 248788
[startup+1150.4 s]
Raw data (loadavg): 1.02 1.01 0.75 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 56994 0 0 0 114899 144 0 0 25 0 1 0 481058136 254758912 52870 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62197 52870 603 41 0 62156 0
vsize: 248788
[startup+1160.39 s]
Raw data (loadavg): 1.02 1.01 0.75 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 57009 0 0 0 115899 144 0 0 25 0 1 0 481058136 254894080 52885 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62230 52885 603 41 0 62189 0
vsize: 248920
[startup+1170.4 s]
Raw data (loadavg): 1.01 1.01 0.75 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 57035 0 0 0 116899 144 0 0 25 0 1 0 481058136 254894080 52911 4294967295 134512640 134672761 3221224624 3221223792 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62230 52911 603 41 0 62189 0
vsize: 248920
[startup+1180.4 s]
Raw data (loadavg): 1.01 1.01 0.76 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 57062 0 0 0 117899 145 0 0 25 0 1 0 481058136 255029248 52938 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62263 52938 603 41 0 62222 0
vsize: 249052
[startup+1190.4 s]
Raw data (loadavg): 1.01 1.01 0.76 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 57137 0 0 0 118899 145 0 0 25 0 1 0 481058136 255299584 53013 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62329 53013 603 41 0 62288 0
vsize: 249316
[startup+1200.4 s]
Raw data (loadavg): 1.01 1.01 0.76 2/54 12396
Raw data (stat): 12396 (minisat+) R 12395 20937 20936 0 -1 0 57152 0 0 0 119900 145 0 0 25 0 1 0 481058136 255434752 53028 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62362 53028 603 41 0 62321 0
vsize: 249448
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.54 s]
Raw data (loadavg): 1.01 1.01 0.76 1/54 12396
Raw data (stat): 12396 (minisat+) Z 12395 20937 20936 0 -1 12 57154 0 0 0 119900 155 0 0 22 0 1 0 481058136 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.54
CPU time (s): 1200.56
CPU user time (s): 1199
CPU system time (s): 1.55476
CPU usage (%): 100.001
Max. virtual memory (Kb): 249448
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####