PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst1.opb
MD5SUM	3be753912a1804561d804d0545fc341d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	13633395
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	9232
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	32
Number of constraints which are nor clauses,nor cardinality constraints	600
Minimum length of a constraint	1
Maximum length of a constraint	260
Trace number 32470

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-27 10:08:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23850 boxname=wulflinc4 idbench=1494 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3be753912a1804561d804d0545fc341d  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-bienst1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-bienst1.opb
IDLAUNCH: 23850
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        914116 kB
Buffers:          7448 kB
Cached:          92688 kB
SwapCached:        504 kB
Active:          17716 kB
Inactive:        84856 kB
HighTotal:      131008 kB
HighFree:        35168 kB
LowTotal:       903652 kB
LowFree:        878948 kB
SwapTotal:     2097136 kB
SwapFree:      2096000 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            12376 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:28:32 (client local time) WITH STATUS 152 IN 1229.98 SECONDS
stats: 23850 7 1229.98 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 732 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 731]---> BDD-cost:    7
c ---[ 730]---> BDD-cost:    7
c ---[ 729]---> BDD-cost:    7
c ---[ 728]---> BDD-cost:    7
c ---[ 727]---> BDD-cost:    7
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    7
c ---[ 724]---> BDD-cost:    7
c ---[ 723]---> BDD-cost:    7
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:    7
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    7
c ---[ 718]---> BDD-cost:    7
c ---[ 717]---> BDD-cost:    7
c ---[ 716]---> BDD-cost:    7
c ---[ 715]---> BDD-cost:    7
c ---[ 714]---> BDD-cost:    7
c ---[ 713]---> BDD-cost:    7
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    7
c ---[ 710]---> BDD-cost:    7
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:    7
c ---[ 706]---> BDD-cost:    7
c ---[ 705]---> BDD-cost:    7
c ---[ 704]---> BDD-cost:    7
c ---[ 702]---> BDD-cost: 2971
c ---[ 700]---> BDD-cost: 2984
c ---[ 698]---> BDD-cost: 2838
c ---[ 696]---> BDD-cost: 2958
c ---[ 694]---> BDD-cost: 2984
c ---[ 692]---> BDD-cost: 3041
c ---[ 690]---> BDD-cost: 2984
c ---[ 688]---> BDD-cost: 3035
c ---[ 686]---> BDD-cost: 3048
c ---[ 684]---> BDD-cost: 3048
c ---[ 682]---> BDD-cost: 3131
c ---[ 680]---> BDD-cost: 3157
c ---[ 678]---> BDD-cost: 3157
c ---[ 676]---> BDD-cost: 3157
c ---[ 674]---> BDD-cost: 2801
c ---[ 672]---> BDD-cost: 2801
c ---[ 670]---> BDD-cost: 2801
c ---[ 668]---> BDD-cost: 2897
c ---[ 666]---> BDD-cost: 2910
c ---[ 664]---> BDD-cost: 2910
c ---[ 662]---> BDD-cost: 2871
c ---[ 660]---> BDD-cost: 2801
c ---[ 658]---> BDD-cost: 2762
c ---[ 656]---> BDD-cost: 2801
c ---[ 654]---> BDD-cost: 2910
c ---[ 652]---> BDD-cost: 2897
c ---[ 650]---> BDD-cost: 2910
c ---[ 648]---> BDD-cost: 2910
c ---[ 646]---> BDD-cost: 2952
c ---[ 644]---> BDD-cost: 2813
c ---[ 642]---> BDD-cost: 2813
c ---[ 640]---> BDD-cost: 2991
c ---[ 638]---> BDD-cost: 3058
c ---[ 636]---> BDD-cost: 2978
c ---[ 634]---> BDD-cost: 2991
c ---[ 632]---> BDD-cost: 2958
c ---[ 630]---> BDD-cost: 2824
c ---[ 628]---> BDD-cost: 2824
c ---[ 626]---> BDD-cost: 2824
c ---[ 624]---> BDD-cost: 2958
c ---[ 622]---> BDD-cost: 2958
c ---[ 620]---> BDD-cost: 2932
c ---[ 618]---> BDD-cost: 2804
c ---[ 616]---> BDD-cost: 2817
c ---[ 614]---> BDD-cost: 2817
c ---[ 612]---> BDD-cost: 2804
c ---[ 610]---> BDD-cost: 2931
c ---[ 608]---> BDD-cost: 2918
c ---[ 606]---> BDD-cost: 2944
c ---[ 604]---> BDD-cost: 2801
c ---[ 602]---> BDD-cost: 2801
c ---[ 600]---> BDD-cost: 2762
c ---[ 598]---> BDD-cost: 2788
c ---[ 596]---> BDD-cost: 2897
c ---[ 594]---> BDD-cost: 2910
c ---[ 592]---> BDD-cost: 2897
c ---[ 591]---> BDD-cost:   52
c ---[ 590]---> BDD-cost:   52
c ---[ 589]---> BDD-cost:   52
c ---[ 588]---> BDD-cost:   52
c ---[ 587]---> BDD-cost:   52
c ---[ 586]---> BDD-cost:   52
c ---[ 585]---> BDD-cost:   52
c ---[ 584]---> BDD-cost:   50
c ---[ 583]---> BDD-cost:   52
c ---[ 582]---> BDD-cost:   52
c ---[ 581]---> BDD-cost:   52
c ---[ 580]---> BDD-cost:   52
c ---[ 579]---> BDD-cost:   52
c ---[ 578]---> BDD-cost:   52
c ---[ 577]---> BDD-cost:   50
c ---[ 576]---> BDD-cost:   50
c ---[ 575]---> BDD-cost:   52
c ---[ 574]---> BDD-cost:   52
c ---[ 573]---> BDD-cost:   52
c ---[ 572]---> BDD-cost:   52
c ---[ 571]---> BDD-cost:   52
c ---[ 570]---> BDD-cost:   52
c ---[ 569]---> BDD-cost:   50
c ---[ 568]---> BDD-cost:   52
c ---[ 567]---> BDD-cost:   50
c ---[ 566]---> BDD-cost:   52
c ---[ 565]---> BDD-cost:   52
c ---[ 564]---> BDD-cost:   52
c ---[ 563]---> BDD-cost:   54
c ---[ 562]---> BDD-cost:   52
c ---[ 561]---> BDD-cost:   54
c ---[ 560]---> BDD-cost:   54
c ---[ 559]---> BDD-cost:   54
c ---[ 558]---> BDD-cost:   54
c ---[ 557]---> BDD-cost:   54
c ---[ 556]---> BDD-cost:   54
c ---[ 555]---> BDD-cost:   54
c ---[ 554]---> BDD-cost:   54
c ---[ 553]---> BDD-cost:   54
c ---[ 552]---> BDD-cost:   54
c ---[ 551]---> BDD-cost:   54
c ---[ 550]---> BDD-cost:   54
c ---[ 549]---> BDD-cost:   54
c ---[ 548]---> BDD-cost:   54
c ---[ 547]---> BDD-cost:   54
c ---[ 546]---> BDD-cost:   54
c ---[ 545]---> BDD-cost:   54
c ---[ 544]---> BDD-cost:   54
c ---[ 543]---> BDD-cost:   54
c ---[ 542]---> BDD-cost:   52
c ---[ 541]---> BDD-cost:   52
c ---[ 540]---> BDD-cost:   52
c ---[ 539]---> BDD-cost:   52
c ---[ 538]---> BDD-cost:   52
c ---[ 537]---> BDD-cost:   52
c ---[ 536]---> BDD-cost:   52
c ---[ 534]---> BDD-cost: 1054
c ---[ 532]---> BDD-cost: 1066
c ---[ 530]---> BDD-cost: 1066
c ---[ 528]---> BDD-cost: 1054
c ---[ 526]---> BDD-cost: 1054
c ---[ 524]---> BDD-cost: 1066
c ---[ 522]---> BDD-cost: 1066
c ---[ 520]---> BDD-cost: 1031
c ---[ 518]---> BDD-cost: 1044
c ---[ 516]---> BDD-cost: 1044
c ---[ 514]---> BDD-cost: 1044
c ---[ 512]---> BDD-cost: 1044
c ---[ 510]---> BDD-cost: 1044
c ---[ 508]---> BDD-cost: 1044
c ---[ 506]---> BDD-cost: 1031
c ---[ 504]---> BDD-cost: 1031
c ---[ 502]---> BDD-cost: 1044
c ---[ 500]---> BDD-cost: 1044
c ---[ 498]---> BDD-cost: 1044
c ---[ 496]---> BDD-cost: 1044
c ---[ 494]---> BDD-cost: 1044
c ---[ 492]---> BDD-cost: 1044
c ---[ 490]---> BDD-cost: 1031
c ---[ 488]---> BDD-cost: 1044
c ---[ 486]---> BDD-cost: 1031
c ---[ 484]---> BDD-cost: 1044
c ---[ 482]---> BDD-cost: 1044
c ---[ 480]---> BDD-cost: 1044
c ---[ 478]---> BDD-cost: 1128
c ---[ 476]---> BDD-cost: 1115
c ---[ 474]---> BDD-cost: 1128
c ---[ 472]---> BDD-cost: 1128
c ---[ 470]---> BDD-cost: 1128
c ---[ 468]---> BDD-cost: 1128
c ---[ 466]---> BDD-cost: 1128
c ---[ 464]---> BDD-cost: 1138
c ---[ 462]---> BDD-cost: 1128
c ---[ 460]---> BDD-cost: 1138
c ---[ 458]---> BDD-cost: 1138
c ---[ 456]---> BDD-cost: 1128
c ---[ 454]---> BDD-cost: 1138
c ---[ 452]---> BDD-cost: 1138
c ---[ 450]---> BDD-cost: 1128
c ---[ 448]---> BDD-cost: 1128
c ---[ 446]---> BDD-cost: 1138
c ---[ 444]---> BDD-cost: 1138
c ---[ 442]---> BDD-cost: 1138
c ---[ 440]---> BDD-cost: 1138
c ---[ 438]---> BDD-cost: 1138
c ---[ 436]---> BDD-cost: 1115
c ---[ 434]---> BDD-cost: 1107
c ---[ 432]---> BDD-cost: 1115
c ---[ 430]---> BDD-cost: 1115
c ---[ 428]---> BDD-cost: 1115
c ---[ 426]---> BDD-cost: 1115
c ---[ 424]---> BDD-cost: 1115
c ---[ 422]---> BDD-cost:  153
c ---[ 420]---> BDD-cost:  153
c ---[ 418]---> BDD-cost:  153
c ---[ 416]---> BDD-cost:  153
c ---[ 414]---> BDD-cost:   93
c ---[ 412]---> BDD-cost:   93
c ---[ 410]---> BDD-cost:   93
c ---[ 408]---> BDD-cost:   93
c ---[ 406]---> BDD-cost:   15
c ---[ 404]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 398]---> BDD-cost:  393
c ---[ 396]---> BDD-cost:  393
c ---[ 394]---> BDD-cost:  393
c ---[ 392]---> BDD-cost:  393
c ---[ 391]---> BDD-cost:   20
c ---[ 390]---> BDD-cost:   20
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:   20
c ---[ 386]---> BDD-cost:   20
c ---[ 385]---> BDD-cost:   20
c ---[ 384]---> BDD-cost:   15
c ---[ 383]---> BDD-cost:   15
c ---[ 382]---> BDD-cost:   15
c ---[ 381]---> BDD-cost:   15
c ---[ 380]---> BDD-cost:   15
c ---[ 379]---> BDD-cost:   15
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   21
c ---[ 376]---> BDD-cost:   21
c ---[ 375]---> BDD-cost:   21
c ---[ 374]---> BDD-cost:   21
c ---[ 373]---> BDD-cost:   21
c ---[ 372]---> BDD-cost:   19
c ---[ 371]---> BDD-cost:   19
c ---[ 370]---> BDD-cost:   19
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   19
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> BDD-cost:  479
c ---[ 365]---> BDD-cost:  479
c ---[ 364]---> BDD-cost:  479
c ---[ 363]---> BDD-cost:  479
c ---[ 362]---> BDD-cost:  479
c ---[ 361]---> BDD-cost:  479
c ---[ 360]---> BDD-cost:  743
c ---[ 359]---> BDD-cost:  743
c ---[ 358]---> BDD-cost:  743
c ---[ 357]---> BDD-cost:  743
c ---[ 356]---> BDD-cost:  743
c ---[ 355]---> BDD-cost:  743
c ---[ 354]---> BDD-cost:  382
c ---[ 353]---> BDD-cost:  382
c ---[ 352]---> BDD-cost:  382
c ---[ 351]---> BDD-cost:  382
c ---[ 350]---> BDD-cost:  382
c ---[ 349]---> BDD-cost:  382
c ---[ 348]---> BDD-cost:  743
c ---[ 347]---> BDD-cost:  743
c ---[ 346]---> BDD-cost:  743
c ---[ 345]---> BDD-cost:  743
c ---[ 344]---> BDD-cost:  743
c ---[ 343]---> BDD-cost:  743
c ---[ 342]---> BDD-cost:   21
c ---[ 341]---> BDD-cost:   21
c ---[ 340]---> BDD-cost:   21
c ---[ 339]---> BDD-cost:   21
c ---[ 338]---> BDD-cost:   21
c ---[ 337]---> BDD-cost:   21
c ---[ 336]---> BDD-cost:   21
c ---[ 335]---> BDD-cost:   21
c ---[ 334]---> BDD-cost:   21
c ---[ 333]---> BDD-cost:   21
c ---[ 332]---> BDD-cost:   21
c ---[ 331]---> BDD-cost:   21
c ---[ 330]---> BDD-cost:   21
c ---[ 329]---> BDD-cost:   20
c ---[ 328]---> BDD-cost:   20
c ---[ 327]---> BDD-cost:   20
c ---[ 326]---> BDD-cost:   20
c ---[ 325]---> BDD-cost:   20
c ---[ 324]---> BDD-cost:   20
c ---[ 323]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   19
c ---[ 321]---> BDD-cost:   19
c ---[ 320]---> BDD-cost:   19
c ---[ 319]---> BDD-cost:   19
c ---[ 318]---> BDD-cost:   19
c ---[ 317]---> BDD-cost:  919
c ---[ 316]---> BDD-cost:  919
c ---[ 315]---> BDD-cost:  919
c ---[ 314]---> BDD-cost:  919
c ---[ 313]---> BDD-cost:  919
c ---[ 312]---> BDD-cost:  919
c ---[ 311]---> BDD-cost:  230
c ---[ 310]---> BDD-cost:  230
c ---[ 309]---> BDD-cost:  230
c ---[ 308]---> BDD-cost:  230
c ---[ 307]---> BDD-cost:  230
c ---[ 306]---> BDD-cost:  230
c ---[ 305]---> BDD-cost:  230
c ---[ 304]---> BDD-cost:  230
c ---[ 303]---> BDD-cost:  230
c ---[ 302]---> BDD-cost:  230
c ---[ 301]---> BDD-cost:  230
c ---[ 300]---> BDD-cost:  230
c ---[ 299]---> BDD-cost:  230
c ---[ 298]---> BDD-cost:  230
c ---[ 297]---> BDD-cost:  230
c ---[ 296]---> BDD-cost:  230
c ---[ 295]---> BDD-cost:  230
c ---[ 294]---> BDD-cost:  230
c ---[ 293]---> BDD-cost:   18
c ---[ 292]---> BDD-cost:   18
c ---[ 291]---> BDD-cost:   18
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   18
c ---[ 286]---> BDD-cost:   18
c ---[ 285]---> BDD-cost:   18
c ---[ 284]---> BDD-cost:   18
c ---[ 283]---> BDD-cost:   18
c ---[ 282]---> BDD-cost:   18
c ---[ 281]---> BDD-cost:   19
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:   19
c ---[ 278]---> BDD-cost:   19
c ---[ 277]---> BDD-cost:   19
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   19
c ---[ 274]---> BDD-cost:   17
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   17
c ---[ 271]---> BDD-cost:   17
c ---[ 270]---> BDD-cost:   17
c ---[ 269]---> BDD-cost:   17
c ---[ 268]---> BDD-cost:  722
c ---[ 267]---> BDD-cost:  722
c ---[ 266]---> BDD-cost:  722
c ---[ 265]---> BDD-cost:  722
c ---[ 264]---> BDD-cost:  722
c ---[ 263]---> BDD-cost:  722
c ---[ 262]---> BDD-cost:  465
c ---[ 261]---> BDD-cost:  465
c ---[ 260]---> BDD-cost:  465
c ---[ 259]---> BDD-cost:  465
c ---[ 258]---> BDD-cost:  465
c ---[ 257]---> BDD-cost:  465
c ---[ 256]---> BDD-cost:  265
c ---[ 255]---> BDD-cost:  265
c ---[ 254]---> BDD-cost:  265
c ---[ 253]---> BDD-cost:  265
c ---[ 252]---> BDD-cost:  265
c ---[ 251]---> BDD-cost:  265
c ---[ 250]---> BDD-cost:  706
c ---[ 249]---> BDD-cost:  706
c ---[ 248]---> BDD-cost:  706
c ---[ 247]---> BDD-cost:  706
c ---[ 246]---> BDD-cost:  706
c ---[ 245]---> BDD-cost:  706
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   16
c ---[ 241]---> BDD-cost:   16
c ---[ 240]---> BDD-cost:   16
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   19
c ---[ 235]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   19
c ---[ 233]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   15
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   15
c ---[ 228]---> BDD-cost:   15
c ---[ 227]---> BDD-cost:   15
c ---[ 226]---> BDD-cost:   19
c ---[ 225]---> BDD-cost:   19
c ---[ 224]---> BDD-cost:   19
c ---[ 223]---> BDD-cost:   19
c ---[ 222]---> BDD-cost:   19
c ---[ 221]---> BDD-cost:   19
c ---[ 220]---> BDD-cost:   19
c ---[ 219]---> BDD-cost:  156
c ---[ 218]---> BDD-cost:  156
c ---[ 217]---> BDD-cost:  156
c ---[ 216]---> BDD-cost:  156
c ---[ 215]---> BDD-cost:  156
c ---[ 214]---> BDD-cost:  156
c ---[ 213]---> BDD-cost:  722
c ---[ 212]---> BDD-cost:  722
c ---[ 211]---> BDD-cost:  722
c ---[ 210]---> BDD-cost:  722
c ---[ 209]---> BDD-cost:  722
c ---[ 208]---> BDD-cost:  722
c ---[ 207]---> BDD-cost:  265
c ---[ 206]---> BDD-cost:  265
c ---[ 205]---> BDD-cost:  265
c ---[ 204]---> BDD-cost:  265
c ---[ 203]---> BDD-cost:  265
c ---[ 202]---> BDD-cost:  265
c ---[ 201]---> BDD-cost:  451
c ---[ 200]---> BDD-cost:  451
c ---[ 199]---> BDD-cost:  451
c ---[ 198]---> BDD-cost:  451
c ---[ 197]---> BDD-cost:  451
c ---[ 196]---> BDD-cost:  451
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   21
c ---[ 190]---> BDD-cost:   21
c ---[ 189]---> BDD-cost:   19
c ---[ 188]---> BDD-cost:   19
c ---[ 187]---> BDD-cost:   19
c ---[ 186]---> BDD-cost:   19
c ---[ 185]---> BDD-cost:   19
c ---[ 184]---> BDD-cost:   19
c ---[ 183]---> BDD-cost:   19
c ---[ 182]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   19
c ---[ 180]---> BDD-cost:   19
c ---[ 179]---> BDD-cost:   19
c ---[ 178]---> BDD-cost:   19
c ---[ 177]---> BDD-cost:   20
c ---[ 176]---> BDD-cost:   20
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   20
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> BDD-cost:  940
c ---[ 170]---> BDD-cost:  940
c ---[ 169]---> BDD-cost:  940
c ---[ 168]---> BDD-cost:  940
c ---[ 167]---> BDD-cost:  940
c ---[ 166]---> BDD-cost:  940
c ---[ 165]---> BDD-cost:  940
c ---[ 164]---> BDD-cost:  608
c ---[ 163]---> BDD-cost:  608
c ---[ 162]---> BDD-cost:  608
c ---[ 161]---> BDD-cost:  608
c ---[ 160]---> BDD-cost:  608
c ---[ 159]---> BDD-cost:  608
c ---[ 158]---> BDD-cost:  743
c ---[ 157]---> BDD-cost:  743
c ---[ 156]---> BDD-cost:  743
c ---[ 155]---> BDD-cost:  743
c ---[ 154]---> BDD-cost:  743
c ---[ 153]---> BDD-cost:  743
c ---[ 152]---> BDD-cost:   29
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   29
c ---[ 149]---> BDD-cost:   29
c ---[ 148]---> BDD-cost:   29
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   21
c ---[ 145]---> BDD-cost:   21
c ---[ 144]---> BDD-cost:   21
c ---[ 143]---> BDD-cost:   21
c ---[ 142]---> BDD-cost:   21
c ---[ 141]---> BDD-cost:   21
c ---[ 140]---> BDD-cost:   19
c ---[ 139]---> BDD-cost:   19
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   19
c ---[ 135]---> BDD-cost:   19
c ---[ 134]---> BDD-cost:   19
c ---[ 133]---> BDD-cost:   19
c ---[ 132]---> BDD-cost:   19
c ---[ 131]---> BDD-cost:   19
c ---[ 130]---> BDD-cost:   19
c ---[ 129]---> BDD-cost:   19
c ---[ 128]---> BDD-cost:   19
c ---[ 127]---> BDD-cost:   19
c ---[ 126]---> BDD-cost:   19
c ---[ 125]---> BDD-cost:   19
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   19
c ---[ 122]---> BDD-cost:  743
c ---[ 121]---> BDD-cost:  743
c ---[ 120]---> BDD-cost:  743
c ---[ 119]---> BDD-cost:  743
c ---[ 118]---> BDD-cost:  743
c ---[ 117]---> BDD-cost:  743
c ---[ 116]---> BDD-cost:  620
c ---[ 115]---> BDD-cost:  620
c ---[ 114]---> BDD-cost:  620
c ---[ 113]---> BDD-cost:  620
c ---[ 112]---> BDD-cost:  620
c ---[ 111]---> BDD-cost:  620
c ---[ 110]---> BDD-cost:  620
c ---[ 109]---> BDD-cost:  706
c ---[ 108]---> BDD-cost:  706
c ---[ 107]---> BDD-cost:  706
c ---[ 106]---> BDD-cost:  706
c ---[ 105]---> BDD-cost:  706
c ---[ 104]---> BDD-cost:  706
c ---[ 103]---> BDD-cost:  465
c ---[ 102]---> BDD-cost:  465
c ---[ 101]---> BDD-cost:  465
c ---[ 100]---> BDD-cost:  465
c ---[  99]---> BDD-cost:  465
c ---[  98]---> BDD-cost:  465
c ---[  97]---> BDD-cost:   19
c ---[  96]---> BDD-cost:   19
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   19
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   19
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   18
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   18
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   19
c ---[  78]---> BDD-cost:   19
c ---[  77]---> BDD-cost:   19
c ---[  76]---> BDD-cost:   19
c ---[  75]---> BDD-cost:   19
c ---[  74]---> BDD-cost:   19
c ---[  73]---> BDD-cost:  706
c ---[  72]---> BDD-cost:  706
c ---[  71]---> BDD-cost:  706
c ---[  70]---> BDD-cost:  706
c ---[  69]---> BDD-cost:  706
c ---[  68]---> BDD-cost:  706
c ---[  67]---> BDD-cost:  703
c ---[  66]---> BDD-cost:  703
c ---[  65]---> BDD-cost:  703
c ---[  64]---> BDD-cost:  703
c ---[  63]---> BDD-cost:  703
c ---[  62]---> BDD-cost:  703
c ---[  61]---> BDD-cost:  894
c ---[  60]---> BDD-cost:  894
c ---[  59]---> BDD-cost:  894
c ---[  58]---> BDD-cost:  894
c ---[  57]---> BDD-cost:  894
c ---[  56]---> BDD-cost:  894
c ---[  55]---> BDD-cost:  894
c ---[  54]---> BDD-cost:  465
c ---[  53]---> BDD-cost:  465
c ---[  52]---> BDD-cost:  465
c ---[  51]---> BDD-cost:  465
c ---[  50]---> BDD-cost:  465
c ---[  49]---> BDD-cost:  465
c ---[  48]---> BDD-cost:   18
c ---[  47]---> BDD-cost:   18
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   18
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   18
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   19
c ---[  35]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   19
c ---[  33]---> BDD-cost:   19
c ---[  32]---> BDD-cost:   19
c ---[  31]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   19
c ---[  28]---> BDD-cost:   19
c ---[  27]---> BDD-cost:   19
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   19
c ---[  24]---> BDD-cost:  696
c ---[  23]---> BDD-cost:  696
c ---[  22]---> BDD-cost:  696
c ---[  21]---> BDD-cost:  696
c ---[  20]---> BDD-cost:  696
c ---[  19]---> BDD-cost:  696
c ---[  18]---> BDD-cost:  156
c ---[  17]---> BDD-cost:  156
c ---[  16]---> BDD-cost:  156
c ---[  15]---> BDD-cost:  156
c ---[  14]---> BDD-cost:  156
c ---[  13]---> BDD-cost:  156
c ---[  12]---> BDD-cost:  668
c ---[  11]---> BDD-cost:  668
c ---[  10]---> BDD-cost:  668
c ---[   9]---> BDD-cost:  668
c ---[   8]---> BDD-cost:  668
c ---[   7]---> BDD-cost:  668
c ---[   6]---> BDD-cost:  743
c ---[   5]---> BDD-cost:  743
c ---[   4]---> BDD-cost:  743
c ---[   3]---> BDD-cost:  743
c ---[   2]---> BDD-cost:  743
c ---[   1]---> BDD-cost:  743
c ---[   0]---> BDD-cost:  743
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  841383  2408754 |  280461       0        0     nan |  0.000 % |
c |       100 |  841383  2408754 |  308507     100     5835    58.4 |  0.993 % |
c |       250 |  841161  2408218 |  339357     242     9668    40.0 |  1.011 % |
c |       475 |  841127  2408123 |  373293     466    22795    48.9 |  1.012 % |
c |       816 |  841092  2408025 |  410622     805    54207    67.3 |  1.014 % |
c |      1322 |  840878  2407437 |  451685    1303    72702    55.8 |  1.024 % |
c |      2083 |  840878  2407437 |  496853    2064   114055    55.3 |  1.024 % |
c |      3223 |  840322  2405917 |  546539    3186   228013    71.6 |  1.059 % |
c |      4931 |  840322  2405917 |  601193    4894   367104    75.0 |  1.059 % |
c |      7493 |  840237  2405691 |  661312    7453   446617    59.9 |  1.064 % |
c |     11337 |  840237  2405691 |  727443   11297   737717    65.3 |  1.064 % |
c |     17103 |  840237  2405691 |  800187   17063  1473431    86.4 |  1.064 % |
c |     25752 |  839939  2404909 |  880206   25705  2333641    90.8 |  1.088 % |
c |     38726 |  839385  2403386 |  968227   38653  3880528   100.4 |  1.119 % |
c |     58187 |  839243  2403005 | 1065050   58106  8118389   139.7 |  1.128 % |
c |     87379 |  839221  2402942 | 1171555   87297 12277017   140.6 |  1.130 % |
c ==============================================================================
c [1mFound solution: 523257[0m
c ---[   0]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110677 |  839988  2404652 |  279996  110588 18618905   168.4 |  1.130 % |
c |    110777 |  839920  2404472 |  307995  110686 18622494   168.2 |  1.152 % |
c |    110929 |  839862  2404318 |  338795  110836 18625228   168.0 |  1.156 % |
c |    111155 |  839589  2403587 |  372674  111054 18629938   167.8 |  1.175 % |
c |    111492 |  839589  2403587 |  409942  111391 18659077   167.5 |  1.175 % |
c |    111999 |  839456  2403222 |  450936  111892 18693139   167.1 |  1.184 % |
c |    112758 |  839315  2402820 |  496029  112645 18746983   166.4 |  1.193 % |
c |    113897 |  839315  2402820 |  545632  113784 18802288   165.2 |  1.193 % |
c |    115605 |  839315  2402820 |  600196  115492 18953531   164.1 |  1.193 % |
c |    118168 |  839104  2402221 |  660215  118047 19107908   161.9 |  1.208 % |
c |    122013 |  839104  2402221 |  726237  121892 19462600   159.7 |  1.208 % |
c |    127782 |  838769  2401254 |  798861  127649 20761322   162.6 |  1.229 % |
c |    136433 |  837986  2399006 |  878747  136260 21731870   159.5 |  1.287 % |
c |    149407 |  837781  2398441 |  966622  149195 23639548   158.4 |  1.300 % |
c |    168869 |  837570  2397856 | 1063284  168650 27138461   160.9 |  1.314 % |
c |    198061 |  837529  2397746 | 1169612  197841 34385344   173.8 |  1.317 % |
c |    241851 |  837134  2396616 | 1286574  241620 47402740   196.2 |  1.348 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 15686 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.93 0.97 0.91 1/54 15682
Raw data (stat): 15682 (runsolver) R 15681 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 797090390 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99989 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0047 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.006 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0127 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0153 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0157 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0166 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0173 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.93 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 15686
Raw data (stat): 15682 (minisat+_script) S 15681 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797090390 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.93
CPU time (s): 1229.98
CPU user time (s): 1227.42
CPU system time (s): 2.56061
CPU usage (%): 100.004
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####