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/MIPLIB/miplib2003/normalized-mps-v2-13-7-p2756.opb
MD5SUM	f2badf1ad4c3213045697b74fa812a03
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4605
Optimality of the best value was proved	NO
Number of terms in the objective function	2166
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	321831
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	321831
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07284
Number of variables	2756
Total number of constraints	3511
Number of constraints which are clauses	132
Number of constraints which are cardinality constraints (but not clauses)	2976
Number of constraints which are nor clauses,nor cardinality constraints	403
Minimum length of a constraint	1
Maximum length of a constraint	546
Trace number 31159

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-05-25 22:35:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22560 boxname=wulflinc8 idbench=1376 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  f2badf1ad4c3213045697b74fa812a03  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-p2756.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-p2756.opb
IDLAUNCH: 22560
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        348624 kB
Buffers:         37620 kB
Cached:         622116 kB
SwapCached:          0 kB
Active:          30692 kB
Inactive:       635952 kB
HighTotal:      131008 kB
HighFree:         8372 kB
LowTotal:       903652 kB
LowFree:        340252 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7068 kB
Slab:            13852 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:55:44 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22560 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 738 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssss..ssssss.sss.ssss..................................................................................................................s.......s...........
c ---[ 759]---> BDD-cost:   31
c ---[ 758]---> BDD-cost:   50
c ---[ 757]---> Sorter-cost: 1402     Base: 3 3 3 2 2
c ---[ 756]---> BDD-cost:  190
c ---[ 755]---> BDD-cost:  157
c ---[ 754]---> Sorter-cost:  929     Base: 3 3 5 2
c ---[ 752]---> Sorter-cost: 1077     Base: 3 3 5 2 11
c ---[ 751]---> BDD-cost:  109
c ---[ 750]---> BDD-cost:  231
c ---[ 749]---> Sorter-cost: 1074     Base: 3 3 3 2 17
c ---[ 747]---> Sorter-cost: 1216     Base: 3 3 5 2
c ---[ 746]---> Sorter-cost:  995     Base: 3 3 3 2 2
c ---[ 745]---> BDD-cost:  216
c ---[ 744]---> Sorter-cost: 1087     Base: 3 3 5 2 11
c ---[ 742]---> BDD-cost:  105
c ---[ 741]---> Sorter-cost: 1073     Base: 3 3 3 2 17
c ---[ 740]---> BDD-cost:  100
c ---[ 739]---> Sorter-cost: 1092     Base: 3 3 3 2 2
c ---[ 738]---> BDD-cost:  131
c ---[ 737]---> BDD-cost:  193
c ---[ 736]---> Sorter-cost:  802     Base: 2 2 5 2 3
c ---[ 735]---> BDD-cost:   67
c ---[ 734]---> BDD-cost:  111
c ---[ 733]---> Sorter-cost:  931     Base: 5 2 3 3 11
c ---[ 732]---> Sorter-cost:  797     Base: 3 3 3 2 17
c ---[ 731]---> Sorter-cost: 1035     Base: 5 3 3 2
c ---[ 730]---> Sorter-cost:  779     Base: 2 2 5 2 3
c ---[ 729]---> BDD-cost:   64
c ---[ 728]---> BDD-cost:  126
c ---[ 727]---> BDD-cost:  103
c ---[ 726]---> BDD-cost:  110
c ---[ 725]---> Sorter-cost: 1070     Base: 5 3 3 3
c ---[ 724]---> Sorter-cost:  736     Base: 5 2 3 2 2
c ---[ 723]---> BDD-cost:   70
c ---[ 722]---> BDD-cost:  114
c ---[ 721]---> BDD-cost:  186
c ---[ 720]---> BDD-cost:  191
c ---[ 719]---> Sorter-cost: 1065     Base: 3 3 5 3
c ---[ 718]---> Sorter-cost:  730     Base: 5 2 3 2 2
c ---[ 717]---> BDD-cost:   44
c ---[ 716]---> BDD-cost:  144
c ---[ 715]---> BDD-cost:   90
c ---[ 714]---> BDD-cost:   63
c ---[ 713]---> Sorter-cost: 1075     Base: 5 2 3 3 5
c ---[ 712]---> Sorter-cost: 1156     Base: 5 2 3 3
c ---[ 711]---> Sorter-cost:  779     Base: 3 3 3 2 2
c ---[ 710]---> BDD-cost:    5
c ---[ 709]---> BDD-cost:   22
c ---[ 708]---> BDD-cost:   31
c ---[ 707]---> BDD-cost:  105
c ---[ 706]---> BDD-cost:   87
c ---[ 705]---> BDD-cost:  104
c ---[ 704]---> BDD-cost:   70
c ---[ 703]---> BDD-cost:  143
c ---[ 702]---> Sorter-cost:  711     Base: 3 3 3 2 3
c ---[ 701]---> BDD-cost:  147
c ---[ 700]---> BDD-cost:  151
c ---[ 699]---> BDD-cost:  144
c ---[ 698]---> BDD-cost:   14
c ---[ 697]---> BDD-cost:   31
c ---[ 696]---> BDD-cost:  103
c ---[ 695]---> BDD-cost:   89
c ---[ 694]---> BDD-cost:  101
c ---[ 693]---> BDD-cost:   62
c ---[ 692]---> BDD-cost:  142
c ---[ 691]---> Sorter-cost:  762     Base: 5 2 3 3
c ---[ 690]---> BDD-cost:  147
c ---[ 689]---> BDD-cost:  157
c ---[ 688]---> BDD-cost:  146
c ---[ 686]---> BDD-cost:   32
c ---[ 685]---> BDD-cost:  112
c ---[ 684]---> BDD-cost:   90
c ---[ 683]---> BDD-cost:  102
c ---[ 682]---> BDD-cost:   70
c ---[ 681]---> BDD-cost:  136
c ---[ 680]---> Sorter-cost:  804     Base: 5 2 3 3
c ---[ 679]---> BDD-cost:  159
c ---[ 678]---> BDD-cost:  154
c ---[ 677]---> BDD-cost:  148
c ---[ 676]---> Sorter-cost: 1050     Base: 7 3 3 2
c ---[ 675]---> BDD-cost:   18
c ---[ 674]---> Sorter-cost: 1077     Base: 5 2 3 3
c ---[ 673]---> Sorter-cost:  977     Base: 3 3 2 3 17
c ---[ 672]---> Sorter-cost: 1107     Base: 5 3 3 2
c ---[ 671]---> BDD-cost:  134
c ---[ 670]---> BDD-cost:   76
c ---[ 669]---> Sorter-cost: 1081     Base: 5 3 3 2
c ---[ 668]---> BDD-cost:   34
c ---[ 667]---> BDD-cost:   27
c ---[ 666]---> BDD-cost:   64
c ---[ 664]---> BDD-cost:   11
c ---[ 662]---> BDD-cost:   47
c ---[ 661]---> BDD-cost:   95
c ---[ 659]---> BDD-cost:   11
c ---[ 657]---> BDD-cost:   91
c ---[ 656]---> BDD-cost:   79
c ---[ 655]---> BDD-cost:   19
c ---[ 654]---> BDD-cost:   37
c ---[ 651]---> BDD-cost:    9
c ---[ 650]---> BDD-cost:   14
c ---[ 649]---> BDD-cost:   10
c ---[ 648]---> BDD-cost:  142
c ---[ 647]---> BDD-cost:   66
c ---[ 646]---> BDD-cost:   14
c ---[ 645]---> BDD-cost:   17
c ---[ 644]---> BDD-cost:   16
c ---[ 643]---> BDD-cost:   10
c ---[ 642]---> BDD-cost:  142
c ---[ 641]---> BDD-cost:   67
c ---[ 640]---> BDD-cost:    7
c ---[ 638]---> BDD-cost:   16
c ---[ 637]---> BDD-cost:   14
c ---[ 636]---> BDD-cost:   29
c ---[ 635]---> BDD-cost:   62
c ---[ 634]---> BDD-cost:  154
c ---[ 633]---> BDD-cost:  104
c ---[ 632]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:   31
c ---[ 630]---> BDD-cost:   85
c ---[ 629]---> BDD-cost:   91
c ---[ 628]---> BDD-cost:  123
c ---[ 627]---> BDD-cost:   81
c ---[ 626]---> BDD-cost:   37
c ---[ 625]---> BDD-cost:  111
c ---[ 624]---> BDD-cost:   16
c ---[ 623]---> BDD-cost:   27
c ---[ 622]---> BDD-cost:   74
c ---[ 620]---> BDD-cost:   44
c ---[ 619]---> BDD-cost:  113
c ---[ 618]---> Sorter-cost: 1080     Base: 3 3 3 2 3
c ---[ 617]---> Sorter-cost:  933     Base: 3 3 2 3 2
c ---[ 616]---> BDD-cost:   51
c ---[ 615]---> BDD-cost:  146
c ---[ 614]---> BDD-cost:   21
c ---[ 613]---> Sorter-cost:  722     Base: 5 2 3 2 2
c ---[ 610]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2
c ---[ 609]---> BDD-cost:   19
c ---[ 608]---> BDD-cost:   25
c ---[ 607]---> BDD-cost:   68
c ---[ 606]---> BDD-cost:    8
c ---[ 605]---> BDD-cost:   66
c ---[ 604]---> BDD-cost:  104
c ---[ 603]---> Sorter-cost: 1098     Base: 3 3 2 3 3
c ---[ 602]---> Sorter-cost:  818     Base: 3 3 3 2 2
c ---[ 601]---> BDD-cost:   47
c ---[ 600]---> BDD-cost:  114
c ---[ 599]---> BDD-cost:   87
c ---[ 596]---> Sorter-cost:  539     Base: 2 2 2 2 2 2 2
c ---[ 595]---> BDD-cost:   15
c ---[ 594]---> BDD-cost:   20
c ---[ 593]---> BDD-cost:   11
c ---[ 592]---> BDD-cost:   14
c ---[ 591]---> BDD-cost:   32
c ---[ 590]---> BDD-cost:   14
c ---[ 589]---> BDD-cost:  109
c ---[ 588]---> BDD-cost:   64
c ---[ 587]---> BDD-cost:   15
c ---[ 586]---> BDD-cost:   21
c ---[ 585]---> BDD-cost:   30
c ---[ 584]---> BDD-cost:   14
c ---[ 583]---> BDD-cost:   47
c ---[ 582]---> BDD-cost:   40
c ---[ 581]---> BDD-cost:   95
c ---[ 580]---> BDD-cost:   65
c ---[ 579]---> BDD-cost:   54
c ---[ 578]---> BDD-cost:   29
c ---[ 577]---> BDD-cost:   27
c ---[ 576]---> BDD-cost:   18
c ---[ 575]---> BDD-cost:  181
c ---[ 574]---> BDD-cost:  152
c ---[ 573]---> Sorter-cost: 1616     Base: 3 3 3 2 13
c ---[ 572]---> Sorter-cost:  996     Base: 3 3 3 2 2
c ---[ 571]---> BDD-cost:  138
c ---[ 570]---> BDD-cost:   95
c ---[ 569]---> BDD-cost:   45
c ---[ 568]---> BDD-cost:   60
c ---[ 567]---> Sorter-cost: 1226     Base: 3 3 5 2 7
c ---[ 566]---> Sorter-cost: 1750     Base: 3 3 3 2 3
c ---[ 565]---> Sorter-cost: 1635     Base: 3 3 5 2 5
c ---[ 563]---> Sorter-cost: 1144     Base: 3 3 5 2 5
c ---[ 562]---> BDD-cost:   70
c ---[ 561]---> BDD-cost:   20
c ---[ 560]---> BDD-cost:   41
c ---[ 559]---> Sorter-cost:  543     Base: 3 3 5 2
c ---[ 558]---> BDD-cost:   17
c ---[ 557]---> Sorter-cost: 1034     Base: 3 3 3 2 2
c ---[ 556]---> BDD-cost:   13
c ---[ 555]---> BDD-cost:   39
c ---[ 554]---> Sorter-cost:  815     Base: 3 3 3 2 2
c ---[ 553]---> BDD-cost:   17
c ---[ 552]---> BDD-cost:  162
c ---[ 551]---> BDD-cost:   15
c ---[ 550]---> BDD-cost:   53
c ---[ 549]---> Sorter-cost:  842     Base: 3 3 5 2 11
c ---[ 547]---> Sorter-cost: 1010     Base: 3 3 3 2 2
c ---[ 546]---> BDD-cost:   18
c ---[ 545]---> BDD-cost:   22
c ---[ 544]---> Sorter-cost:  814     Base: 3 3 3 2 2
c ---[ 543]---> BDD-cost:    4
c ---[ 542]---> BDD-cost:  178
c ---[ 541]---> BDD-cost:   58
c ---[ 539]---> BDD-cost:   78
c ---[ 538]---> BDD-cost:  140
c ---[ 537]---> BDD-cost:   35
c ---[ 536]---> BDD-cost:   30
c ---[ 535]---> Sorter-cost:  775     Base: 5 2 3 3
c ---[ 534]---> Sorter-cost:  688     Base: 3 3 2 3 2
c ---[ 533]---> Sorter-cost:  744     Base: 5 3 3 3
c ---[ 532]---> BDD-cost:  153
c ---[ 531]---> BDD-cost:   45
c ---[ 530]---> BDD-cost:   37
c ---[ 528]---> BDD-cost:   36
c ---[ 526]---> Sorter-cost:  599     Base: 5 3 3 3
c ---[ 525]---> BDD-cost:  146
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   30
c ---[ 522]---> BDD-cost:  162
c ---[ 521]---> BDD-cost:  136
c ---[ 520]---> Sorter-cost:  883     Base: 5 3 3 3
c ---[ 519]---> Sorter-cost:  689     Base: 5 2 3 5
c ---[ 518]---> BDD-cost:   48
c ---[ 517]---> BDD-cost:   19
c ---[ 516]---> BDD-cost:   58
c ---[ 515]---> BDD-cost:   13
c ---[ 513]---> Sorter-cost: 1042     Base: 3 3 5 2
c ---[ 512]---> Sorter-cost:  704     Base: 5 2 3 3 11
c ---[ 511]---> BDD-cost:  173
c ---[ 509]---> BDD-cost:    5
c ---[ 508]---> BDD-cost:   11
c ---[ 507]---> BDD-cost:   45
c ---[ 506]---> BDD-cost:   15
c ---[ 505]---> BDD-cost:   15
c ---[ 504]---> BDD-cost:   19
c ---[ 503]---> BDD-cost:   10
c ---[ 502]---> BDD-cost:  118
c ---[ 501]---> BDD-cost:  127
c ---[ 500]---> BDD-cost:   47
c ---[ 499]---> BDD-cost:   54
c ---[ 498]---> BDD-cost:   33
c ---[ 497]---> BDD-cost:   74
c ---[ 496]---> BDD-cost:   74
c ---[ 495]---> BDD-cost:   13
c ---[ 494]---> BDD-cost:   13
c ---[ 493]---> BDD-cost:   23
c ---[ 492]---> BDD-cost:    4
c ---[ 491]---> BDD-cost:  127
c ---[ 490]---> BDD-cost:  136
c ---[ 489]---> BDD-cost:   45
c ---[ 488]---> BDD-cost:   61
c ---[ 487]---> BDD-cost:   32
c ---[ 486]---> BDD-cost:   75
c ---[ 485]---> BDD-cost:   95
c ---[ 484]---> BDD-cost:   18
c ---[ 483]---> BDD-cost:   18
c ---[ 482]---> BDD-cost:   23
c ---[ 481]---> BDD-cost:    4
c ---[ 480]---> BDD-cost:  111
c ---[ 479]---> BDD-cost:  147
c ---[ 478]---> BDD-cost:   53
c ---[ 477]---> BDD-cost:   60
c ---[ 476]---> BDD-cost:   29
c ---[ 475]---> BDD-cost:   85
c ---[ 474]---> BDD-cost:   93
c ---[ 473]---> Sorter-cost:  795     Base: 5 2 3 3
c ---[ 472]---> Sorter-cost:  905     Base: 3 3 5 2
c ---[ 471]---> BDD-cost:   98
c ---[ 469]---> BDD-cost:   10
c ---[ 468]---> Sorter-cost:  715     Base: 5 3 3 2 11
c ---[ 467]---> BDD-cost:   17
c ---[ 466]---> BDD-cost:   14
c ---[ 464]---> Adder-cost: 1996   maxlim: 571   bits: 11/10
c ---[ 463]---> BDD-cost:   30
c ---[ 462]---> Adder-cost: 166   maxlim: 399   bits: 10/9
c ---[ 461]---> Adder-cost: 307   maxlim: 274   bits: 10/9
c ---[ 460]---> Adder-cost: 426   maxlim: 1316   bits: 11/11
c ---[ 459]---> Adder-cost: 540   maxlim: 1397   bits: 11/11
c ---[ 458]---> Adder-cost: 533   maxlim: 98   bits: 8/7
c ---[ 457]---> BDD-cost:   99
c ---[ 456]---> Adder-cost: 90   maxlim: 119   bits: 8/7
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    9
c ---[ 451]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    5
c ---[ 448]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    5
c ---[ 444]---> BDD-cost:    5
c ---[ 442]---> BDD-cost:  104
c ---[ 441]---> BDD-cost:   67
c ---[ 439]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    5
c ---[ 436]---> BDD-cost:    5
c ---[ 434]---> BDD-cost:    5
c ---[ 432]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    3
c ---[ 430]---> BDD-cost:   12
c ---[ 429]---> BDD-cost:    3
c ---[ 428]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    5
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    5
c ---[ 419]---> BDD-cost:    2
c ---[ 417]---> BDD-cost:    5
c ---[ 414]---> BDD-cost:    5
c ---[ 412]---> BDD-cost:    5
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    5
c ---[ 408]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    3
c ---[ 404]---> BDD-cost:    3
c ---[ 403]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:    5
c ---[ 399]---> BDD-cost:    3
c ---[ 397]---> BDD-cost:    3
c ---[ 394]---> BDD-cost:    3
c ---[ 393]---> BDD-cost:    5
c ---[ 391]---> BDD-cost:    5
c ---[ 388]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:   81
c ---[ 384]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    3
c ---[ 382]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    5
c ---[ 380]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    5
c ---[ 376]---> BDD-cost:   84
c ---[ 375]---> BDD-cost:    5
c ---[ 374]---> BDD-cost:    3
c ---[ 372]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    3
c ---[ 369]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:    5
c ---[ 365]---> Sorter-cost:  774     Base: 3 3 3 2 17
c ---[ 364]---> BDD-cost:    3
c ---[ 362]---> BDD-cost:    5
c ---[ 360]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    3
c ---[ 358]---> BDD-cost:    5
c ---[ 357]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    5
c ---[ 354]---> Sorter-cost:  604     Base: 3 3 2 3 17
c ---[ 351]---> BDD-cost:    5
c ---[ 350]---> BDD-cost:    3
c ---[ 348]---> BDD-cost:    5
c ---[ 346]---> BDD-cost:    3
c ---[ 345]---> BDD-cost:    5
c ---[ 343]---> BDD-cost:   73
c ---[ 341]---> BDD-cost:    5
c ---[ 340]---> BDD-cost:    3
c ---[ 338]---> BDD-cost:    5
c ---[ 336]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    5
c ---[ 332]---> BDD-cost:   52
c ---[ 331]---> BDD-cost:  106
c ---[ 330]---> BDD-cost:    5
c ---[ 327]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    3
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    5
c ---[ 320]---> Sorter-cost:  646     Base: 2 2 2 2 2 5
c ---[ 317]---> BDD-cost:    5
c ---[ 314]---> BDD-cost:    5
c ---[ 312]---> BDD-cost:    3
c ---[ 309]---> BDD-cost:  165
c ---[ 308]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:    5
c ---[ 303]---> BDD-cost:    5
c ---[ 302]---> BDD-cost:    5
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   90
c ---[ 296]---> BDD-cost:    5
c ---[ 295]---> BDD-cost:    5
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> BDD-cost:    5
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    5
c ---[ 287]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:    5
c ---[ 283]---> BDD-cost:    3
c ---[ 282]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    5
c ---[ 278]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:   15
c ---[ 274]---> BDD-cost:    5
c ---[ 273]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    5
c ---[ 270]---> BDD-cost:    5
c ---[ 269]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    5
c ---[ 266]---> BDD-cost:    5
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 262]---> BDD-cost:    5
c ---[ 260]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    5
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    5
c ---[ 256]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    3
c ---[ 254]---> BDD-cost:   21
c ---[ 253]---> BDD-cost:    5
c ---[ 252]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    5
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    5
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:    3
c ---[ 246]---> BDD-cost:    5
c ---[ 245]---> BDD-cost:    5
c ---[ 243]---> BDD-cost:   20
c ---[ 242]---> BDD-cost:    5
c ---[ 241]---> BDD-cost:    5
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    5
c ---[ 237]---> BDD-cost:    5
c ---[ 236]---> BDD-cost:    5
c ---[ 234]---> BDD-cost:    5
c ---[ 233]---> BDD-cost:    5
c ---[ 232]---> BDD-cost:  100
c ---[ 230]---> BDD-cost:    5
c ---[ 229]---> BDD-cost:    5
c ---[ 227]---> BDD-cost:    5
c ---[ 226]---> BDD-cost:    5
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:    5
c ---[ 222]---> BDD-cost:    5
c ---[ 221]---> BDD-cost:   36
c ---[ 220]---> BDD-cost:   91
c ---[ 219]---> BDD-cost:    5
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:    5
c ---[ 214]---> BDD-cost:    5
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    5
c ---[ 210]---> BDD-cost:    5
c ---[ 209]---> Sorter-cost:  775     Base: 3 3 3 2 17
c ---[ 208]---> BDD-cost:    5
c ---[ 206]---> BDD-cost:    5
c ---[ 205]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    5
c ---[ 202]---> BDD-cost:    5
c ---[ 201]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    3
c ---[ 198]---> Sorter-cost:  581     Base: 3 3 3 2 17
c ---[ 195]---> BDD-cost:    5
c ---[ 193]---> BDD-cost:    5
c ---[ 192]---> BDD-cost:    3
c ---[ 190]---> BDD-cost:    5
c ---[ 188]---> BDD-cost:    5
c ---[ 187]---> BDD-cost:   83
c ---[ 186]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 182]---> BDD-cost:    5
c ---[ 180]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    5
c ---[ 176]---> BDD-cost:  116
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    5
c ---[ 167]---> BDD-cost:    5
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:   89
c ---[ 163]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    5
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:  132
c ---[ 153]---> BDD-cost:    5
c ---[ 152]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    5
c ---[ 148]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    5
c ---[ 145]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:   76
c ---[ 142]---> BDD-cost:    5
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    5
c ---[ 136]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    5
c ---[ 133]---> BDD-cost:    5
c ---[ 132]---> BDD-cost:  107
c ---[ 131]---> BDD-cost:    5
c ---[ 129]---> BDD-cost:    5
c ---[ 127]---> BDD-cost:    5
c ---[ 126]---> BDD-cost:    5
c ---[ 124]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:    5
c ---[ 120]---> BDD-cost:    5
c ---[ 118]---> BDD-cost:    5
c ---[ 117]---> BDD-cost:    5
c ---[ 115]---> BDD-cost:    5
c ---[ 114]---> BDD-cost:    5
c ---[ 112]---> BDD-cost:    5
c ---[ 110]---> BDD-cost:   17
c ---[ 109]---> BDD-cost:   44
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    5
c ---[ 105]---> BDD-cost:    5
c ---[ 104]---> BDD-cost:    5
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:    5
c ---[  99]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    5
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:    5
c ---[  91]---> BDD-cost:    5
c ---[  90]---> BDD-cost:    5
c ---[  88]---> BDD-cost:    5
c ---[  87]---> BDD-cost:   37
c ---[  86]---> BDD-cost:    5
c ---[  84]---> BDD-cost:    5
c ---[  83]---> BDD-cost:    5
c ---[  81]---> BDD-cost:    5
c ---[  80]---> BDD-cost:    5
c ---[  79]---> BDD-cost:    5
c ---[  78]---> BDD-cost:    5
c ---[  76]---> BDD-cost:   52
c ---[  75]---> BDD-cost:    5
c ---[  74]---> BDD-cost:    5
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:    5
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    5
c ---[  65]---> BDD-cost:   66
c ---[  64]---> BDD-cost:  189
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   14
c ---[  59]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   40
c ---[  56]---> BDD-cost:   46
c ---[  55]---> BDD-cost:  122
c ---[  54]---> BDD-cost:   27
c ---[  53]---> BDD-cost:  122
c ---[  52]---> BDD-cost:  122
c ---[  51]---> BDD-cost:  122
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:   60
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:   51
c ---[  46]---> BDD-cost:   66
c ---[  45]---> BDD-cost:   43
c ---[  44]---> BDD-cost:   49
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:   29
c ---[  41]---> BDD-cost:   56
c ---[  40]---> BDD-cost:   81
c ---[  39]---> BDD-cost:   26
c ---[  38]---> BDD-cost:   66
c ---[  37]---> BDD-cost:  109
c ---[  36]---> BDD-cost:   38
c ---[  35]---> BDD-cost:   84
c ---[  34]---> BDD-cost:  219
c ---[  33]---> BDD-cost:  265
c ---[  32]---> BDD-cost:  109
c ---[  31]---> Sorter-cost: 1065     Base: 3 3 3 2 2
c ---[  30]---> Sorter-cost:  662     Base: 3 3 3 2 3
c ---[  29]---> Sorter-cost: 1360     Base: 3 3 3 2 2
c ---[  28]---> BDD-cost:  194
c ---[  27]---> BDD-cost:   44
c ---[  26]---> BDD-cost:  139
c ---[  25]---> Sorter-cost:  897     Base: 3 3 5 2
c ---[  24]---> Sorter-cost: 1184     Base: 3 3 3 2 2
c ---[  23]---> Sorter-cost: 1210     Base: 3 3 3 2 2
c ---[  22]---> BDD-cost:  113
c ---[  21]---> BDD-cost:   62
c ---[  20]---> BDD-cost:   73
c ---[  19]---> BDD-cost:   67
c ---[  18]---> BDD-cost:   24
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   19
c ---[   9]---> BDD-cost:   19
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   25
c ---[   6]---> BDD-cost:   28
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    2
c ---[   3]---> BDD-cost:   34
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   45
c ---[   0]---> BDD-cost:   25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  226650   589896 |   75550       0        0     nan |  0.000 % |
c |       100 |  226317   589156 |   83105      90      754     8.4 |  0.955 % |
c |       250 |  226064   588595 |   91415     224     1717     7.7 |  1.046 % |
c |       475 |  225724   587772 |  100557     436     3331     7.6 |  1.152 % |
c |       812 |  225316   586824 |  110612     751     6192     8.2 |  1.292 % |
c |      1318 |  225137   586396 |  121674    1229     9571     7.8 |  1.356 % |
c |      2078 |  224545   585050 |  133841    1955    15735     8.0 |  1.569 % |
c |      3219 |  223744   583235 |  147225    3042    27192     8.9 |  1.845 % |
c |      4928 |  222201   579681 |  161948    4656    43383     9.3 |  2.396 % |
c |      7490 |  220338   575372 |  178142    7109    70956    10.0 |  3.068 % |
c |     11336 |  217524   568858 |  195957   10716   103313     9.6 |  4.087 % |
c |     17102 |  215256   563574 |  215552   16240   159483     9.8 |  4.920 % |
c |     25751 |  213104   558511 |  237108   24672   251227    10.2 |  5.747 % |
c |     38725 |  211985   555776 |  260819   37504   468327    12.5 |  6.163 % |
c ==============================================================================
c [1mFound solution: 153189[0m
c ---[   0]---> Adder-cost: 11288   maxlim: 168642   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47438 |  289535   834350 |   96511   46070   610216    13.2 |  6.163 % |
c |     47539 |  289512   834294 |  106162   46167   611344    13.2 |  5.836 % |
c |     47689 |  289468   834199 |  116778   46314   612728    13.2 |  5.852 % |
c |     47914 |  289468   834199 |  128456   46539   614777    13.2 |  5.852 % |
c |     48251 |  289400   834047 |  141301   46866   618704    13.2 |  5.877 % |
c |     48757 |  289369   833965 |  155431   47365   625812    13.2 |  5.885 % |
c |     49516 |  289369   833965 |  170975   48124   641348    13.3 |  5.885 % |
c |     50657 |  289256   833712 |  188072   49246   661239    13.4 |  5.921 % |
c |     52365 |  289247   833692 |  206879   50953   703006    13.8 |  5.925 % |
c |     54927 |  289023   833147 |  227567   53497   744926    13.9 |  6.003 % |
c |     58771 |  288760   832551 |  250324   57315   794515    13.9 |  6.092 % |
c |     64537 |  288509   831960 |  275357   63055   913696    14.5 |  6.180 % |
c |     73186 |  288470   831870 |  302892   71686  1113770    15.5 |  6.194 % |
c |     86160 |  287669   830039 |  333182   84550  1307263    15.5 |  6.471 % |
c |    105621 |  286768   827950 |  366500  103896  1628791    15.7 |  6.782 % |
c |    134815 |  285674   825380 |  403150  132961  2103720    15.8 |  7.147 % |
c |    178604 |  285166   824208 |  443465  176669  2774363    15.7 |  7.326 % |
c |    244289 |  284239   822017 |  487811  242205  3899969    16.1 |  7.638 % |
c ==============================================================================
c [1mFound solution: 135087[0m
c ---[   0]---> Adder-cost: 0   maxlim: 186744   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    251099 |  284210   822067 |   94736  249000  4018432    16.1 |  7.638 % |
c |    251199 |  284204   822055 |  104209   35639   334304     9.4 |  7.668 % |
c |    251349 |  284204   822055 |  114630   35789   336052     9.4 |  7.668 % |
c |    251575 |  284164   821962 |  126093   36014   338223     9.4 |  7.685 % |
c |    251913 |  284164   821962 |  138702   36352   344340     9.5 |  7.685 % |
c |    252419 |  284164   821962 |  152573   36858   351705     9.5 |  7.685 % |
c |    253179 |  284164   821962 |  167830   37618   370671     9.9 |  7.685 % |
c |    254318 |  284164   821962 |  184613   38757   380396     9.8 |  7.685 % |
c |    256026 |  284027   821645 |  203075   40454   402270     9.9 |  7.729 % |
c |    258590 |  283931   821424 |  223382   43013   466256    10.8 |  7.767 % |
c |    262435 |  283862   821264 |  245720   46852   539404    11.5 |  7.792 % |
c |    268201 |  283782   821084 |  270292   52613   617915    11.7 |  7.821 % |
c |    276851 |  283736   820959 |  297322   61259   829437    13.5 |  7.834 % |
c |    289825 |  283655   820751 |  327054   74200  1060912    14.3 |  7.860 % |
c |    309286 |  283411   820187 |  359759   93626  1786463    19.1 |  7.945 % |
c |    338480 |  282822   818832 |  395735  122724  2259592    18.4 |  8.157 % |
c |    382269 |  282466   818024 |  435309  166467  3225280    19.4 |  8.292 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 23084 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.96 0.99 0.92 2/54 23080
Raw data (stat): 23080 (runsolver) R 23079 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 770734529 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0007 s]
Raw data (loadavg): 0.96 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.97 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0021 s]
Raw data (loadavg): 0.97 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0019 s]
Raw data (loadavg): 0.98 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0018 s]
Raw data (loadavg): 0.98 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0025 s]
Raw data (loadavg): 0.98 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0034 s]
Raw data (loadavg): 0.98 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0041 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0036 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.021 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.027 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.027 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.028 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.033 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.034 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.033 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.034 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.034 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.033 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.039 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.045 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.061 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.069 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.068 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.077 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.077 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.078 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.078 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.078 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.078 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.078 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.078 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.081 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.081 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.081 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.09 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.1 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.1 s]
Raw data (loadavg): 0.99 0.99 0.92 2/55 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.74 s]
Raw data (loadavg): 0.99 0.99 0.92 1/53 23084
Raw data (stat): 23080 (minisat+_script) S 23079 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770734529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.74
CPU time (s): 1229.87
CPU user time (s): 1229.2
CPU system time (s): 0.668898
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####