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-danoint.opb
MD5SUM	32dd768e34cdc0e1cb04afadbe97060d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(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	13107200
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	52829966
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.36179
Number of variables	9304
Total number of constraints	728
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	72
Number of constraints which are nor clauses,nor cardinality constraints	656
Minimum length of a constraint	1
Maximum length of a constraint	1000
Trace number 15436

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 04:24:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17510 boxname=wulflinc20 idbench=1347 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  32dd768e34cdc0e1cb04afadbe97060d  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-danoint.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-danoint.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-danoint.opb
IDLAUNCH: 17510
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        875956 kB
Buffers:          1936 kB
Cached:         132868 kB
SwapCached:        516 kB
Active:          26748 kB
Inactive:       110080 kB
HighTotal:      131008 kB
HighFree:        36680 kB
LowTotal:       903652 kB
LowFree:        839276 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            16156 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:44:46 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 17510 7 1200.32 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssss
c ---[ 833]---> BDD-cost:   12
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:   13
c ---[ 825]---> BDD-cost:   15
c ---[ 823]---> BDD-cost:   15
c ---[ 821]---> BDD-cost: 2727
c ---[ 819]---> BDD-cost: 2891
c ---[ 817]---> BDD-cost: 2786
c ---[ 815]---> BDD-cost: 2786
c ---[ 813]---> BDD-cost: 2930
c ---[ 811]---> BDD-cost: 2930
c ---[ 809]---> BDD-cost: 2799
c ---[ 807]---> BDD-cost: 2930
c ---[ 805]---> BDD-cost: 2861
c ---[ 803]---> BDD-cost: 2770
c ---[ 801]---> BDD-cost:   15
c ---[ 799]---> BDD-cost: 2770
c ---[ 797]---> BDD-cost: 2770
c ---[ 795]---> BDD-cost: 2770
c ---[ 793]---> BDD-cost: 2770
c ---[ 791]---> BDD-cost: 2744
c ---[ 789]---> BDD-cost: 2737
c ---[ 787]---> BDD-cost: 2750
c ---[ 785]---> BDD-cost: 2750
c ---[ 783]---> BDD-cost: 2737
c ---[ 781]---> BDD-cost: 2737
c ---[ 779]---> BDD-cost:   15
c ---[ 777]---> BDD-cost: 2724
c ---[ 775]---> BDD-cost: 2750
c ---[ 773]---> BDD-cost: 2727
c ---[ 771]---> BDD-cost: 2727
c ---[ 769]---> BDD-cost: 2688
c ---[ 767]---> BDD-cost: 2714
c ---[ 765]---> BDD-cost: 2714
c ---[ 763]---> BDD-cost: 2727
c ---[ 761]---> BDD-cost: 2714
c ---[ 760]---> BDD-cost:  110
c ---[ 758]---> BDD-cost:   15
c ---[ 757]---> BDD-cost:  110
c ---[ 756]---> BDD-cost:  110
c ---[ 755]---> BDD-cost:  110
c ---[ 754]---> BDD-cost:  110
c ---[ 753]---> BDD-cost:  110
c ---[ 752]---> BDD-cost:  110
c ---[ 751]---> BDD-cost:  110
c ---[ 750]---> BDD-cost:  110
c ---[ 749]---> BDD-cost:  110
c ---[ 748]---> BDD-cost:  110
c ---[ 746]---> BDD-cost:   15
c ---[ 745]---> BDD-cost:  110
c ---[ 744]---> BDD-cost:  110
c ---[ 743]---> BDD-cost:  110
c ---[ 742]---> BDD-cost:  110
c ---[ 741]---> BDD-cost:  110
c ---[ 740]---> BDD-cost:  110
c ---[ 739]---> BDD-cost:  110
c ---[ 738]---> BDD-cost:  110
c ---[ 737]---> BDD-cost:  110
c ---[ 736]---> BDD-cost:  110
c ---[ 734]---> BDD-cost:   15
c ---[ 733]---> BDD-cost:  110
c ---[ 732]---> BDD-cost:  110
c ---[ 731]---> BDD-cost:  110
c ---[ 730]---> BDD-cost:  110
c ---[ 729]---> BDD-cost:  110
c ---[ 728]---> BDD-cost:  110
c ---[ 727]---> BDD-cost:  110
c ---[ 726]---> BDD-cost:  110
c ---[ 725]---> BDD-cost:  110
c ---[ 724]---> BDD-cost:  110
c ---[ 722]---> BDD-cost:   15
c ---[ 721]---> BDD-cost:  110
c ---[ 720]---> BDD-cost:  110
c ---[ 719]---> BDD-cost:  110
c ---[ 718]---> BDD-cost:  110
c ---[ 717]---> BDD-cost:  110
c ---[ 716]---> BDD-cost:  110
c ---[ 715]---> BDD-cost:  110
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:  110
c ---[ 712]---> BDD-cost:  110
c ---[ 710]---> BDD-cost: 1007
c ---[ 709]---> BDD-cost:  110
c ---[ 708]---> BDD-cost:  110
c ---[ 707]---> BDD-cost:  110
c ---[ 706]---> BDD-cost:  110
c ---[ 705]---> BDD-cost:  110
c ---[ 704]---> BDD-cost:  110
c ---[ 703]---> BDD-cost:  110
c ---[ 702]---> BDD-cost:  110
c ---[ 701]---> BDD-cost:  110
c ---[ 700]---> BDD-cost:  110
c ---[ 698]---> BDD-cost: 1011
c ---[ 697]---> BDD-cost:  110
c ---[ 696]---> BDD-cost:  110
c ---[ 695]---> BDD-cost:  110
c ---[ 694]---> BDD-cost:  110
c ---[ 693]---> BDD-cost:  110
c ---[ 692]---> BDD-cost:   22
c ---[ 691]---> BDD-cost:   18
c ---[ 690]---> BDD-cost:   16
c ---[ 689]---> BDD-cost:   22
c ---[ 688]---> BDD-cost:   21
c ---[ 686]---> BDD-cost: 1011
c ---[ 685]---> BDD-cost:   19
c ---[ 684]---> BDD-cost:   18
c ---[ 683]---> BDD-cost:   22
c ---[ 682]---> BDD-cost:   22
c ---[ 681]---> BDD-cost:   16
c ---[ 680]---> BDD-cost:   22
c ---[ 679]---> BDD-cost:   21
c ---[ 678]---> BDD-cost:   19
c ---[ 677]---> BDD-cost:   18
c ---[ 676]---> BDD-cost:   22
c ---[ 674]---> BDD-cost:   15
c ---[ 672]---> BDD-cost: 1007
c ---[ 671]---> BDD-cost:   22
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:   22
c ---[ 668]---> BDD-cost:   21
c ---[ 667]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:   18
c ---[ 665]---> BDD-cost:   22
c ---[ 664]---> BDD-cost:   22
c ---[ 663]---> BDD-cost:   18
c ---[ 662]---> BDD-cost:   16
c ---[ 660]---> BDD-cost: 1007
c ---[ 659]---> BDD-cost:   21
c ---[ 658]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   18
c ---[ 656]---> BDD-cost:   22
c ---[ 655]---> BDD-cost:   22
c ---[ 654]---> BDD-cost:   18
c ---[ 653]---> BDD-cost:   16
c ---[ 652]---> BDD-cost:   22
c ---[ 651]---> BDD-cost:   19
c ---[ 650]---> BDD-cost:   18
c ---[ 648]---> BDD-cost: 1011
c ---[ 647]---> BDD-cost:   22
c ---[ 646]---> BDD-cost:   22
c ---[ 645]---> BDD-cost:   18
c ---[ 644]---> BDD-cost:   16
c ---[ 643]---> BDD-cost:   22
c ---[ 642]---> BDD-cost:   21
c ---[ 641]---> BDD-cost:   18
c ---[ 640]---> BDD-cost:   22
c ---[ 639]---> BDD-cost:   22
c ---[ 638]---> BDD-cost:   18
c ---[ 636]---> BDD-cost: 1011
c ---[ 635]---> BDD-cost:   16
c ---[ 634]---> BDD-cost:   22
c ---[ 633]---> BDD-cost:   21
c ---[ 632]---> BDD-cost:   19
c ---[ 631]---> BDD-cost:   22
c ---[ 630]---> BDD-cost:   18
c ---[ 629]---> BDD-cost:   19
c ---[ 628]---> BDD-cost:   19
c ---[ 627]---> BDD-cost:   19
c ---[ 626]---> BDD-cost:   16
c ---[ 624]---> BDD-cost:  999
c ---[ 623]---> BDD-cost:   18
c ---[ 622]---> BDD-cost:   15
c ---[ 621]---> BDD-cost:   22
c ---[ 620]---> BDD-cost:   19
c ---[ 619]---> BDD-cost:   19
c ---[ 618]---> BDD-cost:   19
c ---[ 617]---> BDD-cost:   16
c ---[ 616]---> BDD-cost:   18
c ---[ 615]---> BDD-cost:   15
c ---[ 614]---> BDD-cost:   22
c ---[ 612]---> BDD-cost: 1003
c ---[ 611]---> BDD-cost:   18
c ---[ 610]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   19
c ---[ 608]---> BDD-cost:   16
c ---[ 607]---> BDD-cost:   18
c ---[ 606]---> BDD-cost:   15
c ---[ 605]---> BDD-cost:   22
c ---[ 604]---> BDD-cost:   18
c ---[ 603]---> BDD-cost:   19
c ---[ 602]---> BDD-cost:   19
c ---[ 600]---> BDD-cost: 1003
c ---[ 599]---> BDD-cost:   16
c ---[ 598]---> BDD-cost:   18
c ---[ 597]---> BDD-cost:   15
c ---[ 596]---> BDD-cost:   22
c ---[ 595]---> BDD-cost:   18
c ---[ 594]---> BDD-cost:   19
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:   18
c ---[ 590]---> BDD-cost:   15
c ---[ 588]---> BDD-cost: 1003
c ---[ 587]---> BDD-cost:   22
c ---[ 586]---> BDD-cost:   18
c ---[ 585]---> BDD-cost:   19
c ---[ 584]---> BDD-cost:   19
c ---[ 583]---> BDD-cost:   19
c ---[ 582]---> BDD-cost:   18
c ---[ 581]---> BDD-cost:   15
c ---[ 580]---> BDD-cost:   22
c ---[ 579]---> BDD-cost:   18
c ---[ 578]---> BDD-cost:   19
c ---[ 576]---> BDD-cost: 1003
c ---[ 575]---> BDD-cost:   19
c ---[ 574]---> BDD-cost:   19
c ---[ 573]---> BDD-cost:   16
c ---[ 572]---> BDD-cost:   20
c ---[ 571]---> BDD-cost:   19
c ---[ 570]---> BDD-cost:   15
c ---[ 569]---> BDD-cost:   19
c ---[ 568]---> BDD-cost:   19
c ---[ 567]---> BDD-cost:   18
c ---[ 566]---> BDD-cost:   19
c ---[ 564]---> BDD-cost: 1003
c ---[ 563]---> BDD-cost:   22
c ---[ 562]---> BDD-cost:   19
c ---[ 561]---> BDD-cost:   15
c ---[ 560]---> BDD-cost:   19
c ---[ 559]---> BDD-cost:   19
c ---[ 558]---> BDD-cost:   18
c ---[ 557]---> BDD-cost:   19
c ---[ 556]---> BDD-cost:   22
c ---[ 555]---> BDD-cost:   20
c ---[ 554]---> BDD-cost:   19
c ---[ 552]---> BDD-cost:   15
c ---[ 550]---> BDD-cost: 1003
c ---[ 549]---> BDD-cost:   19
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   18
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:   22
c ---[ 544]---> BDD-cost:   20
c ---[ 543]---> BDD-cost:   19
c ---[ 542]---> BDD-cost:   15
c ---[ 541]---> BDD-cost:   19
c ---[ 540]---> BDD-cost:   18
c ---[ 538]---> BDD-cost:  999
c ---[ 537]---> BDD-cost:   19
c ---[ 536]---> BDD-cost:   22
c ---[ 535]---> BDD-cost:   20
c ---[ 534]---> BDD-cost:   19
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:   19
c ---[ 531]---> BDD-cost:   18
c ---[ 530]---> BDD-cost:   19
c ---[ 529]---> BDD-cost:   22
c ---[ 528]---> BDD-cost:   20
c ---[ 526]---> BDD-cost:  999
c ---[ 525]---> BDD-cost:   19
c ---[ 524]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   19
c ---[ 522]---> BDD-cost:   19
c ---[ 521]---> BDD-cost:   19
c ---[ 520]---> BDD-cost:   22
c ---[ 519]---> BDD-cost:   20
c ---[ 518]---> BDD-cost:   19
c ---[ 517]---> BDD-cost:   15
c ---[ 516]---> BDD-cost:   19
c ---[ 514]---> BDD-cost: 1003
c ---[ 513]---> BDD-cost:   19
c ---[ 512]---> BDD-cost:   18
c ---[ 511]---> BDD-cost:   22
c ---[ 510]---> BDD-cost:   17
c ---[ 509]---> BDD-cost:   19
c ---[ 508]---> BDD-cost:   20
c ---[ 507]---> BDD-cost:   19
c ---[ 506]---> BDD-cost:   19
c ---[ 505]---> BDD-cost:   19
c ---[ 504]---> BDD-cost:   19
c ---[ 502]---> BDD-cost: 1003
c ---[ 501]---> BDD-cost:   17
c ---[ 500]---> BDD-cost:   19
c ---[ 499]---> BDD-cost:   20
c ---[ 498]---> BDD-cost:   19
c ---[ 497]---> BDD-cost:   19
c ---[ 496]---> BDD-cost:   19
c ---[ 495]---> BDD-cost:   19
c ---[ 494]---> BDD-cost:   22
c ---[ 493]---> BDD-cost:   19
c ---[ 492]---> BDD-cost:   20
c ---[ 490]---> BDD-cost: 1003
c ---[ 489]---> BDD-cost:   19
c ---[ 488]---> BDD-cost:   19
c ---[ 487]---> BDD-cost:   19
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   22
c ---[ 484]---> BDD-cost:   17
c ---[ 483]---> BDD-cost:   19
c ---[ 482]---> BDD-cost:   19
c ---[ 481]---> BDD-cost:   19
c ---[ 480]---> BDD-cost:   19
c ---[ 478]---> BDD-cost: 1003
c ---[ 477]---> BDD-cost:   19
c ---[ 476]---> BDD-cost:   22
c ---[ 475]---> BDD-cost:   17
c ---[ 474]---> BDD-cost:   19
c ---[ 473]---> BDD-cost:   20
c ---[ 472]---> BDD-cost:   19
c ---[ 471]---> BDD-cost:   19
c ---[ 470]---> BDD-cost:   19
c ---[ 469]---> BDD-cost:   22
c ---[ 468]---> BDD-cost:   17
c ---[ 466]---> BDD-cost: 1003
c ---[ 465]---> BDD-cost:   19
c ---[ 464]---> BDD-cost:   20
c ---[ 463]---> BDD-cost:   19
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:   19
c ---[ 460]---> BDD-cost:   22
c ---[ 459]---> BDD-cost:   17
c ---[ 458]---> BDD-cost:   19
c ---[ 457]---> BDD-cost:   20
c ---[ 456]---> BDD-cost:   19
c ---[ 454]---> BDD-cost: 1003
c ---[ 453]---> BDD-cost:   19
c ---[ 452]---> BDD-cost:   22
c ---[ 451]---> BDD-cost:   19
c ---[ 450]---> BDD-cost:   16
c ---[ 449]---> BDD-cost:   22
c ---[ 448]---> BDD-cost:   19
c ---[ 447]---> BDD-cost:   19
c ---[ 446]---> BDD-cost:   19
c ---[ 445]---> BDD-cost:   18
c ---[ 444]---> BDD-cost:   19
c ---[ 442]---> BDD-cost:  999
c ---[ 441]---> BDD-cost:   16
c ---[ 440]---> BDD-cost:   22
c ---[ 439]---> BDD-cost:   19
c ---[ 438]---> BDD-cost:   19
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:   18
c ---[ 435]---> BDD-cost:   22
c ---[ 434]---> BDD-cost:   16
c ---[ 433]---> BDD-cost:   22
c ---[ 432]---> BDD-cost:   19
c ---[ 430]---> BDD-cost:   15
c ---[ 428]---> BDD-cost: 1003
c ---[ 427]---> BDD-cost:   19
c ---[ 426]---> BDD-cost:   19
c ---[ 425]---> BDD-cost:   18
c ---[ 424]---> BDD-cost:   22
c ---[ 423]---> BDD-cost:   19
c ---[ 422]---> BDD-cost:   22
c ---[ 421]---> BDD-cost:   19
c ---[ 420]---> BDD-cost:   19
c ---[ 419]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   18
c ---[ 416]---> BDD-cost:  999
c ---[ 415]---> BDD-cost:   22
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:   16
c ---[ 412]---> BDD-cost:   22
c ---[ 411]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:   19
c ---[ 409]---> BDD-cost:   18
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:   16
c ---[ 404]---> BDD-cost: 1003
c ---[ 403]---> BDD-cost:   22
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   19
c ---[ 400]---> BDD-cost:   18
c ---[ 399]---> BDD-cost:   22
c ---[ 398]---> BDD-cost:   19
c ---[ 397]---> BDD-cost:   16
c ---[ 396]---> BDD-cost:   22
c ---[ 395]---> BDD-cost:   19
c ---[ 394]---> BDD-cost:   19
c ---[ 392]---> BDD-cost: 1003
c ---[ 391]---> BDD-cost:   22
c ---[ 390]---> BDD-cost:   18
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:   22
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   16
c ---[ 384]---> BDD-cost:   19
c ---[ 383]---> BDD-cost:   18
c ---[ 382]---> BDD-cost:   19
c ---[ 380]---> BDD-cost: 1003
c ---[ 379]---> BDD-cost:   20
c ---[ 378]---> BDD-cost:   22
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:   16
c ---[ 375]---> BDD-cost:   19
c ---[ 374]---> BDD-cost:   22
c ---[ 373]---> BDD-cost:   19
c ---[ 372]---> BDD-cost:   20
c ---[ 371]---> BDD-cost:   22
c ---[ 370]---> BDD-cost:   19
c ---[ 368]---> BDD-cost: 1003
c ---[ 367]---> BDD-cost:   16
c ---[ 366]---> BDD-cost:   19
c ---[ 365]---> BDD-cost:   22
c ---[ 364]---> BDD-cost:   18
c ---[ 363]---> BDD-cost:   20
c ---[ 362]---> BDD-cost:   22
c ---[ 361]---> BDD-cost:   19
c ---[ 360]---> BDD-cost:   16
c ---[ 359]---> BDD-cost:   19
c ---[ 358]---> BDD-cost:   22
c ---[ 356]---> BDD-cost:  999
c ---[ 355]---> BDD-cost:   18
c ---[ 354]---> BDD-cost:   19
c ---[ 353]---> BDD-cost:   22
c ---[ 352]---> BDD-cost:   19
c ---[ 351]---> BDD-cost:   16
c ---[ 350]---> BDD-cost:   19
c ---[ 349]---> BDD-cost:   22
c ---[ 348]---> BDD-cost:   18
c ---[ 347]---> BDD-cost:   19
c ---[ 346]---> BDD-cost:   20
c ---[ 344]---> BDD-cost: 1003
c ---[ 343]---> BDD-cost:   22
c ---[ 342]---> BDD-cost:   16
c ---[ 341]---> BDD-cost:   19
c ---[ 340]---> BDD-cost:   22
c ---[ 339]---> BDD-cost:   18
c ---[ 338]---> BDD-cost:   19
c ---[ 337]---> BDD-cost:   20
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   19
c ---[ 334]---> BDD-cost:   22
c ---[ 332]---> BDD-cost: 1003
c ---[ 331]---> BDD-cost:   17
c ---[ 330]---> BDD-cost:   17
c ---[ 329]---> BDD-cost:   19
c ---[ 328]---> BDD-cost:   19
c ---[ 327]---> BDD-cost:   21
c ---[ 326]---> BDD-cost:   19
c ---[ 325]---> BDD-cost:   22
c ---[ 324]---> BDD-cost:   17
c ---[ 323]---> BDD-cost:   17
c ---[ 322]---> BDD-cost:   19
c ---[ 320]---> BDD-cost: 1003
c ---[ 319]---> BDD-cost:   19
c ---[ 318]---> BDD-cost:   21
c ---[ 317]---> BDD-cost:   19
c ---[ 316]---> BDD-cost:   22
c ---[ 315]---> BDD-cost:   22
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:   21
c ---[ 310]---> BDD-cost:   19
c ---[ 308]---> BDD-cost:   15
c ---[ 306]---> BDD-cost: 1003
c ---[ 305]---> BDD-cost:   22
c ---[ 304]---> BDD-cost:   22
c ---[ 303]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:   19
c ---[ 300]---> BDD-cost:   21
c ---[ 299]---> BDD-cost:   19
c ---[ 298]---> BDD-cost:   22
c ---[ 297]---> BDD-cost:   22
c ---[ 296]---> BDD-cost:   17
c ---[ 294]---> BDD-cost: 1003
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   19
c ---[ 291]---> BDD-cost:   21
c ---[ 290]---> BDD-cost:   19
c ---[ 289]---> BDD-cost:   22
c ---[ 288]---> BDD-cost:   22
c ---[ 287]---> BDD-cost:   17
c ---[ 286]---> BDD-cost:   17
c ---[ 285]---> BDD-cost:   19
c ---[ 284]---> BDD-cost:   21
c ---[ 282]---> BDD-cost: 1007
c ---[ 281]---> BDD-cost:   19
c ---[ 280]---> BDD-cost:   22
c ---[ 279]---> BDD-cost:   22
c ---[ 278]---> BDD-cost:   17
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   19
c ---[ 274]---> BDD-cost:   21
c ---[ 273]---> BDD-cost:   22
c ---[ 272]---> BDD-cost:   19
c ---[ 270]---> BDD-cost: 1003
c ---[ 269]---> BDD-cost:   18
c ---[ 268]---> BDD-cost:   15
c ---[ 267]---> BDD-cost:   18
c ---[ 266]---> BDD-cost:   18
c ---[ 265]---> BDD-cost:   19
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   19
c ---[ 262]---> BDD-cost:   18
c ---[ 261]---> BDD-cost:   15
c ---[ 260]---> BDD-cost:   18
c ---[ 258]---> BDD-cost: 1007
c ---[ 257]---> BDD-cost:   18
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:   19
c ---[ 254]---> BDD-cost:   22
c ---[ 253]---> BDD-cost:   18
c ---[ 252]---> BDD-cost:   15
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   19
c ---[ 246]---> BDD-cost: 1007
c ---[ 245]---> BDD-cost:   22
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   18
c ---[ 241]---> BDD-cost:   18
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> BDD-cost:   22
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   18
c ---[ 234]---> BDD-cost: 1003
c ---[ 233]---> BDD-cost:   18
c ---[ 232]---> BDD-cost:   18
c ---[ 231]---> BDD-cost:   19
c ---[ 230]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   22
c ---[ 228]---> BDD-cost:   19
c ---[ 227]---> BDD-cost:   18
c ---[ 226]---> BDD-cost:   15
c ---[ 225]---> BDD-cost:   18
c ---[ 224]---> BDD-cost:   19
c ---[ 222]---> BDD-cost: 1007
c ---[ 221]---> BDD-cost:   19
c ---[ 220]---> BDD-cost:   22
c ---[ 219]---> BDD-cost:   19
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   15
c ---[ 216]---> BDD-cost:   18
c ---[ 215]---> BDD-cost:   19
c ---[ 213]---> BDD-cost:44748
c ---[ 211]---> BDD-cost:46848
c ---[ 209]---> BDD-cost:43173
c ---[ 207]---> BDD-cost: 1007
c ---[ 205]---> BDD-cost:43140
c ---[ 203]---> BDD-cost:45192
c ---[ 201]---> BDD-cost:43886
c ---[ 199]---> BDD-cost:43523
c ---[ 197]---> BDD-cost:43148
c ---[ 190]---> BDD-cost: 1003
c ---[ 185]---> BDD-cost: 1004
c ---[ 182]---> BDD-cost: 1018
c ---[ 179]---> BDD-cost: 1038
c ---[ 176]---> BDD-cost: 1038
c ---[ 174]---> BDD-cost:   15
c ---[ 172]---> BDD-cost: 1003
c ---[ 169]---> BDD-cost: 1012
c ---[ 166]---> BDD-cost: 1004
c ---[ 163]---> BDD-cost: 1057
c ---[ 160]---> BDD-cost: 1038
c ---[ 158]---> BDD-cost:  880
c ---[ 156]---> BDD-cost: 1007
c ---[ 155]---> BDD-cost:  887
c ---[ 154]---> BDD-cost:  938
c ---[ 153]---> BDD-cost:  798
c ---[ 152]---> BDD-cost:  938
c ---[ 151]---> BDD-cost:  817
c ---[ 150]---> BDD-cost:  938
c ---[ 149]---> BDD-cost:  870
c ---[ 148]---> BDD-cost:  950
c ---[ 147]---> BDD-cost:  950
c ---[ 146]---> BDD-cost:  810
c ---[ 144]---> BDD-cost: 1007
c ---[ 143]---> BDD-cost:  950
c ---[ 142]---> BDD-cost:  950
c ---[ 141]---> BDD-cost:  950
c ---[ 140]---> BDD-cost:  849
c ---[ 139]---> BDD-cost:  859
c ---[ 138]---> BDD-cost:  859
c ---[ 137]---> BDD-cost:  747
c ---[ 136]---> BDD-cost:  817
c ---[ 135]---> BDD-cost:  859
c ---[ 134]---> BDD-cost:  670
c ---[ 132]---> BDD-cost: 1007
c ---[ 131]---> BDD-cost:  817
c ---[ 130]---> BDD-cost:  670
c ---[ 129]---> BDD-cost:  859
c ---[ 128]---> BDD-cost:  817
c ---[ 127]---> BDD-cost:  747
c ---[ 126]---> BDD-cost:  859
c ---[ 125]---> BDD-cost:  859
c ---[ 124]---> BDD-cost:  730
c ---[ 123]---> BDD-cost:  798
c ---[ 122]---> BDD-cost:  798
c ---[ 120]---> BDD-cost: 1007
c ---[ 119]---> BDD-cost:  950
c ---[ 118]---> BDD-cost:  950
c ---[ 117]---> BDD-cost:  868
c ---[ 116]---> BDD-cost:  950
c ---[ 115]---> BDD-cost:  877
c ---[ 114]---> BDD-cost:  938
c ---[ 113]---> BDD-cost:  938
c ---[ 112]---> BDD-cost:  875
c ---[ 111]---> BDD-cost:  938
c ---[ 110]---> BDD-cost:  938
c ---[ 108]---> BDD-cost: 1007
c ---[ 107]---> BDD-cost:  798
c ---[ 106]---> BDD-cost:  795
c ---[ 105]---> BDD-cost:  938
c ---[ 104]---> BDD-cost:  875
c ---[ 103]---> BDD-cost:  868
c ---[ 102]---> BDD-cost:  868
c ---[ 101]---> BDD-cost:  798
c ---[ 100]---> BDD-cost:  875
c ---[  99]---> BDD-cost:  849
c ---[  98]---> BDD-cost:  817
c ---[  96]---> BDD-cost: 1003
c ---[  95]---> BDD-cost:  670
c ---[  94]---> BDD-cost:  747
c ---[  93]---> BDD-cost:  789
c ---[  92]---> BDD-cost:  817
c ---[  91]---> BDD-cost:  789
c ---[  89]---> BDD-cost:  999
c ---[  87]---> BDD-cost: 1003
c ---[  85]---> BDD-cost: 1003
c ---[  83]---> BDD-cost:   15
c ---[  81]---> BDD-cost:  999
c ---[  79]---> BDD-cost: 1003
c ---[  77]---> BDD-cost: 1003
c ---[  75]---> BDD-cost: 2885
c ---[  73]---> BDD-cost: 2910
c ---[  71]---> BDD-cost: 2801
c ---[  69]---> BDD-cost: 2775
c ---[  67]---> BDD-cost: 2801
c ---[  65]---> BDD-cost: 2897
c ---[  63]---> BDD-cost: 2801
c ---[  61]---> BDD-cost:   15
c ---[  59]---> BDD-cost: 2934
c ---[  57]---> BDD-cost: 2974
c ---[  55]---> BDD-cost: 2974
c ---[  53]---> BDD-cost: 2948
c ---[  51]---> BDD-cost: 2974
c ---[  49]---> BDD-cost: 2974
c ---[  47]---> BDD-cost: 2974
c ---[  45]---> BDD-cost: 2702
c ---[  43]---> BDD-cost: 2727
c ---[  41]---> BDD-cost: 2727
c ---[  39]---> BDD-cost:   15
c ---[  37]---> BDD-cost: 2714
c ---[  35]---> BDD-cost: 2727
c ---[  33]---> BDD-cost: 2727
c ---[  31]---> BDD-cost: 2688
c ---[  29]---> BDD-cost: 2727
c ---[  27]---> BDD-cost: 2688
c ---[  25]---> BDD-cost: 2727
c ---[  23]---> BDD-cost: 2727
c ---[  21]---> BDD-cost: 2714
c ---[  19]---> BDD-cost: 2727
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:  123
c ---[  14]---> BDD-cost:  170
c ---[  13]---> BDD-cost:  132
c ---[  12]---> BDD-cost:  144
c ---[  11]---> BDD-cost:  165
c ---[  10]---> BDD-cost:  148
c ---[   9]---> BDD-cost:  152
c ---[   8]---> BDD-cost:  132
c ---[   7]---> BDD-cost:   49
c ---[   6]---> BDD-cost:   51
c ---[   5]---> BDD-cost:   54
c ---[   4]---> BDD-cost:   54
c ---[   3]---> BDD-cost:   51
c ---[   2]---> BDD-cost:   49
c ---[   1]---> BDD-cost:   54
c ---[   0]---> BDD-cost:   54
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1835824  5411764 |  611941       0        0     nan |  0.000 % |
c |       100 | 1835818  5411746 |  673135      60     5768    96.1 |  0.559 % |
c |       250 | 1835796  5411702 |  740448     207    17254    83.4 |  0.561 % |
c |       476 | 1835796  5411702 |  814493     433    53325   123.2 |  0.561 % |
c |       815 | 1835796  5411702 |  895942     772    77057    99.8 |  0.561 % |
c |      1322 | 1835782  5411674 |  985537    1277   126111    98.8 |  0.562 % |
c |      2081 | 1835779  5411665 | 1084090    2024   204458   101.0 |  0.562 % |
c |      3220 | 1835779  5411665 | 1192499    3163   358960   113.5 |  0.562 % |
c |      4928 | 1835779  5411665 | 1311749    4871   643026   132.0 |  0.562 % |
c |      7492 | 1835779  5411665 | 1442924    7435  1141464   153.5 |  0.562 % |
c |     11336 | 1835779  5411665 | 1587217   11279  2311221   204.9 |  0.562 % |
c |     17104 | 1835779  5411665 | 1745939   17047  3829709   224.7 |  0.562 % |
c |     25753 | 1835776  5411656 | 1920532   25684  6339619   246.8 |  0.562 % |
c |     38728 | 1835776  5411656 | 2112586   38659  9972194   258.0 |  0.562 % |
c |     58191 | 1835776  5411656 | 2323844   58122 14315517   246.3 |  0.562 % |
#### 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.78 0.95 0.94 2/54 28627
Raw data (stat): 28627 (runsolver) R 28626 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542177677 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.81 0.95 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 52049 0 0 0 873 124 0 0 25 0 1 0 542177677 242036736 48362 4294967295 134512640 134672761 3221224528 3221185664 134542563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59091 48363 603 41 0 59050 0
vsize: 236364
[startup+20.0013 s]
Raw data (loadavg): 0.84 0.95 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 57523 0 0 0 1860 137 0 0 25 0 1 0 542177677 257851392 53836 4294967295 134512640 134672761 3221224528 3221223728 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62952 53836 603 41 0 62911 0
vsize: 251808
[startup+30.0015 s]
Raw data (loadavg): 0.86 0.95 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 57578 0 0 0 2860 137 0 0 25 0 1 0 542177677 258121728 53891 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63018 53891 603 41 0 62977 0
vsize: 252072
[startup+40.0024 s]
Raw data (loadavg): 0.89 0.95 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 57610 0 0 0 3859 137 0 0 25 0 1 0 542177677 258256896 53923 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63051 53923 603 41 0 63010 0
vsize: 252204
[startup+50.0032 s]
Raw data (loadavg): 0.90 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 57682 0 0 0 4858 138 0 0 25 0 1 0 542177677 258392064 53995 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63084 53995 603 41 0 63043 0
vsize: 252336
[startup+60.0025 s]
Raw data (loadavg): 0.92 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 57763 0 0 0 5858 138 0 0 25 0 1 0 542177677 258662400 54076 4294967295 134512640 134672761 3221224528 3221223676 1074733097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63150 54076 603 41 0 63109 0
vsize: 252600
[startup+70.0035 s]
Raw data (loadavg): 0.93 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 57857 0 0 0 6858 139 0 0 25 0 1 0 542177677 259067904 54170 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63249 54170 603 41 0 63208 0
vsize: 252996
[startup+80.0042 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58055 0 0 0 7857 140 0 0 25 0 1 0 542177677 259743744 54368 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63414 54368 603 41 0 63373 0
vsize: 253656
[startup+90.0047 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58064 0 0 0 8857 140 0 0 25 0 1 0 542177677 259878912 54377 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63447 54377 603 41 0 63406 0
vsize: 253788
[startup+100.004 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58075 0 0 0 9857 140 0 0 25 0 1 0 542177677 259878912 54388 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63447 54388 603 41 0 63406 0
vsize: 253788
[startup+110.004 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58085 0 0 0 10858 140 0 0 25 0 1 0 542177677 259878912 54398 4294967295 134512640 134672761 3221224528 3221223696 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63447 54398 603 41 0 63406 0
vsize: 253788
[startup+120.005 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58107 0 0 0 11858 140 0 0 25 0 1 0 542177677 260014080 54420 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63480 54420 603 41 0 63439 0
vsize: 253920
[startup+130.01 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58133 0 0 0 12858 140 0 0 25 0 1 0 542177677 260145152 54446 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63512 54446 603 41 0 63471 0
vsize: 254048
[startup+140.015 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58167 0 0 0 13859 140 0 0 25 0 1 0 542177677 260276224 54480 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63544 54480 603 41 0 63503 0
vsize: 254176
[startup+150.019 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58205 0 0 0 14859 140 0 0 25 0 1 0 542177677 260419584 54518 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63579 54518 603 41 0 63538 0
vsize: 254316
[startup+160.019 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58230 0 0 0 15859 141 0 0 25 0 1 0 542177677 260554752 54543 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63612 54543 603 41 0 63571 0
vsize: 254448
[startup+170.019 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58252 0 0 0 16859 141 0 0 25 0 1 0 542177677 260554752 54565 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63612 54565 603 41 0 63571 0
vsize: 254448
[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58273 0 0 0 17859 141 0 0 25 0 1 0 542177677 260685824 54586 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63644 54586 603 41 0 63603 0
vsize: 254576
[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58293 0 0 0 18860 141 0 0 25 0 1 0 542177677 260820992 54606 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63677 54606 603 41 0 63636 0
vsize: 254708
[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58330 0 0 0 19860 141 0 0 25 0 1 0 542177677 261009408 54643 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63723 54643 603 41 0 63682 0
vsize: 254892
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58355 0 0 0 20860 141 0 0 25 0 1 0 542177677 261009408 54668 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63723 54668 603 41 0 63682 0
vsize: 254892
[startup+220.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58373 0 0 0 21859 141 0 0 25 0 1 0 542177677 261144576 54686 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63756 54686 603 41 0 63715 0
vsize: 255024
[startup+230.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58450 0 0 0 22859 141 0 0 25 0 1 0 542177677 261414912 54763 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63822 54763 603 41 0 63781 0
vsize: 255288
[startup+240.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 58880 0 0 0 23857 143 0 0 25 0 1 0 542177677 263168000 55193 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64250 55193 603 41 0 64209 0
vsize: 257000
[startup+250.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 59103 0 0 0 24856 144 0 0 25 0 1 0 542177677 264114176 55416 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64481 55416 603 41 0 64440 0
vsize: 257924
[startup+260.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 59523 0 0 0 25856 145 0 0 25 0 1 0 542177677 265863168 55836 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64908 55836 603 41 0 64867 0
vsize: 259632
[startup+270.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 59934 0 0 0 26855 146 0 0 25 0 1 0 542177677 267468800 56247 4294967295 134512640 134672761 3221224528 3221223632 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65300 56247 603 41 0 65259 0
vsize: 261200
[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 60064 0 0 0 27855 146 0 0 25 0 1 0 542177677 268005376 56377 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65431 56377 603 41 0 65390 0
vsize: 261724
[startup+290.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 60105 0 0 0 28855 146 0 0 25 0 1 0 542177677 268271616 56418 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65496 56418 603 41 0 65455 0
vsize: 261984
[startup+300.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 60223 0 0 0 29855 146 0 0 25 0 1 0 542177677 268677120 56536 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65595 56536 603 41 0 65554 0
vsize: 262380
[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 60566 0 0 0 30854 147 0 0 25 0 1 0 542177677 270028800 56879 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65925 56879 603 41 0 65884 0
vsize: 263700
[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 60926 0 0 0 31854 148 0 0 25 0 1 0 542177677 271507456 57239 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66286 57239 603 41 0 66245 0
vsize: 265144
[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 61314 0 0 0 32853 149 0 0 25 0 1 0 542177677 273125376 57627 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66681 57627 603 41 0 66640 0
vsize: 266724
[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 61626 0 0 0 33852 150 0 0 25 0 1 0 542177677 274550784 57939 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67029 57939 603 41 0 66988 0
vsize: 268116
[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 61691 0 0 0 34852 150 0 0 25 0 1 0 542177677 274821120 58004 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67095 58004 603 41 0 67054 0
vsize: 268380
[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 61965 0 0 0 35851 151 0 0 25 0 1 0 542177677 275898368 58278 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67358 58278 603 41 0 67317 0
vsize: 269432
[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62281 0 0 0 36850 153 0 0 25 0 1 0 542177677 277114880 58594 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67655 58594 603 41 0 67614 0
vsize: 270620
[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62335 0 0 0 37850 153 0 0 25 0 1 0 542177677 277385216 58648 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67721 58648 603 41 0 67680 0
vsize: 270884
[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62388 0 0 0 38850 153 0 0 25 0 1 0 542177677 277655552 58701 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67787 58701 603 41 0 67746 0
vsize: 271148
[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62464 0 0 0 39851 153 0 0 25 0 1 0 542177677 277913600 58777 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67850 58777 603 41 0 67809 0
vsize: 271400
[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62499 0 0 0 40851 153 0 0 25 0 1 0 542177677 278048768 58812 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67883 58812 603 41 0 67842 0
vsize: 271532
[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62554 0 0 0 41851 153 0 0 25 0 1 0 542177677 278319104 58867 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67949 58867 603 41 0 67908 0
vsize: 271796
[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62725 0 0 0 42850 154 0 0 25 0 1 0 542177677 278994944 59038 4294967295 134512640 134672761 3221224528 3221223632 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68114 59038 603 41 0 68073 0
vsize: 272456
[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62781 0 0 0 43850 155 0 0 25 0 1 0 542177677 279261184 59094 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68179 59094 603 41 0 68138 0
vsize: 272716
[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62810 0 0 0 44850 155 0 0 25 0 1 0 542177677 279261184 59123 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68179 59123 603 41 0 68138 0
vsize: 272716
[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62864 0 0 0 45850 155 0 0 25 0 1 0 542177677 279531520 59177 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68245 59177 603 41 0 68204 0
vsize: 272980
[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62940 0 0 0 46850 155 0 0 25 0 1 0 542177677 279801856 59253 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68311 59253 603 41 0 68270 0
vsize: 273244
[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 62988 0 0 0 47850 155 0 0 25 0 1 0 542177677 280068096 59301 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68376 59301 603 41 0 68335 0
vsize: 273504
[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63077 0 0 0 48850 155 0 0 25 0 1 0 542177677 280473600 59390 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68475 59390 603 41 0 68434 0
vsize: 273900
[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63159 0 0 0 49850 155 0 0 25 0 1 0 542177677 280743936 59472 4294967295 134512640 134672761 3221224528 3221223544 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68541 59472 603 41 0 68500 0
vsize: 274164
[startup+510.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63224 0 0 0 50850 155 0 0 25 0 1 0 542177677 281014272 59537 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68607 59537 603 41 0 68566 0
vsize: 274428
[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63268 0 0 0 51850 155 0 0 25 0 1 0 542177677 281149440 59581 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68640 59581 603 41 0 68599 0
vsize: 274560
[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63309 0 0 0 52851 155 0 0 25 0 1 0 542177677 281419776 59622 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68706 59622 603 41 0 68665 0
vsize: 274824
[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63341 0 0 0 53851 155 0 0 25 0 1 0 542177677 281419776 59654 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68706 59654 603 41 0 68665 0
vsize: 274824
[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63410 0 0 0 54850 156 0 0 25 0 1 0 542177677 281825280 59723 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68805 59723 603 41 0 68764 0
vsize: 275220
[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63446 0 0 0 55851 156 0 0 25 0 1 0 542177677 281960448 59759 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68838 59759 603 41 0 68797 0
vsize: 275352
[startup+570.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63507 0 0 0 56851 156 0 0 25 0 1 0 542177677 282095616 59820 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68871 59820 603 41 0 68830 0
vsize: 275484
[startup+580.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63554 0 0 0 57851 156 0 0 25 0 1 0 542177677 282365952 59867 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68937 59867 603 41 0 68896 0
vsize: 275748
[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63600 0 0 0 58851 156 0 0 25 0 1 0 542177677 282492928 59913 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68968 59913 603 41 0 68927 0
vsize: 275872
[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63646 0 0 0 59851 156 0 0 25 0 1 0 542177677 282763264 59959 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69034 59959 603 41 0 68993 0
vsize: 276136
[startup+610.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63688 0 0 0 60851 156 0 0 25 0 1 0 542177677 282890240 60001 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69065 60001 603 41 0 69024 0
vsize: 276260
[startup+620.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63724 0 0 0 61851 156 0 0 25 0 1 0 542177677 283021312 60037 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69097 60037 603 41 0 69056 0
vsize: 276388
[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63770 0 0 0 62851 156 0 0 25 0 1 0 542177677 283291648 60083 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69163 60083 603 41 0 69122 0
vsize: 276652
[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63836 0 0 0 63851 156 0 0 25 0 1 0 542177677 283561984 60149 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69229 60149 603 41 0 69188 0
vsize: 276916
[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63895 0 0 0 64851 157 0 0 25 0 1 0 542177677 283697152 60208 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69262 60208 603 41 0 69221 0
vsize: 277048
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63938 0 0 0 65851 157 0 0 25 0 1 0 542177677 283967488 60251 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69328 60251 603 41 0 69287 0
vsize: 277312
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 63983 0 0 0 66851 157 0 0 25 0 1 0 542177677 284098560 60296 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69360 60296 603 41 0 69319 0
vsize: 277440
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 64033 0 0 0 67851 158 0 0 25 0 1 0 542177677 284360704 60346 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69424 60346 603 41 0 69383 0
vsize: 277696
[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 64090 0 0 0 68851 158 0 0 25 0 1 0 542177677 284495872 60403 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69457 60403 603 41 0 69416 0
vsize: 277828
[startup+700.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 64128 0 0 0 69851 158 0 0 25 0 1 0 542177677 284762112 60441 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69522 60441 603 41 0 69481 0
vsize: 278088
[startup+710.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 64189 0 0 0 70851 158 0 0 25 0 1 0 542177677 284897280 60502 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69555 60502 603 41 0 69514 0
vsize: 278220
[startup+720.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 64276 0 0 0 71850 159 0 0 25 0 1 0 542177677 285302784 60589 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69654 60589 603 41 0 69613 0
vsize: 278616
[startup+730.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 64722 0 0 0 72850 159 0 0 25 0 1 0 542177677 287182848 61035 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70113 61035 603 41 0 70072 0
vsize: 280452
[startup+740.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 65137 0 0 0 73850 160 0 0 25 0 1 0 542177677 288788480 61450 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70505 61450 603 41 0 70464 0
vsize: 282020
[startup+750.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 65474 0 0 0 74849 160 0 0 25 0 1 0 542177677 290140160 61787 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70835 61787 603 41 0 70794 0
vsize: 283340
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 65874 0 0 0 75848 161 0 0 25 0 1 0 542177677 291889152 62187 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71262 62187 603 41 0 71221 0
vsize: 285048
[startup+770.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 66367 0 0 0 76847 162 0 0 25 0 1 0 542177677 294031360 62680 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71785 62680 603 41 0 71744 0
vsize: 287140
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 66704 0 0 0 77846 164 0 0 25 0 1 0 542177677 295383040 63017 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72115 63017 603 41 0 72074 0
vsize: 288460
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 67265 0 0 0 78845 166 0 0 25 0 1 0 542177677 297676800 63578 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72675 63578 603 41 0 72634 0
vsize: 290700
[startup+800.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 67759 0 0 0 79843 167 0 0 25 0 1 0 542177677 299696128 64072 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73168 64072 603 41 0 73127 0
vsize: 292672
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 67974 0 0 0 80843 168 0 0 25 0 1 0 542177677 300507136 64287 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73366 64287 603 41 0 73325 0
vsize: 293464
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 67988 0 0 0 81843 168 0 0 25 0 1 0 542177677 300642304 64301 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73399 64301 603 41 0 73358 0
vsize: 293596
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68001 0 0 0 82843 168 0 0 25 0 1 0 542177677 300642304 64314 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73399 64314 603 41 0 73358 0
vsize: 293596
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68012 0 0 0 83843 168 0 0 25 0 1 0 542177677 300642304 64325 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73399 64325 603 41 0 73358 0
vsize: 293596
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68023 0 0 0 84843 168 0 0 25 0 1 0 542177677 300773376 64336 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73431 64336 603 41 0 73390 0
vsize: 293724
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68062 0 0 0 85843 168 0 0 25 0 1 0 542177677 300908544 64375 4294967295 134512640 134672761 3221224528 3221223728 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73464 64375 603 41 0 73423 0
vsize: 293856
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68093 0 0 0 86844 168 0 0 25 0 1 0 542177677 301043712 64406 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73497 64406 603 41 0 73456 0
vsize: 293988
[startup+880.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68134 0 0 0 87844 168 0 0 25 0 1 0 542177677 301174784 64447 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73529 64447 603 41 0 73488 0
vsize: 294116
[startup+890.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68181 0 0 0 88844 168 0 0 25 0 1 0 542177677 301441024 64494 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73594 64494 603 41 0 73553 0
vsize: 294376
[startup+900.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68229 0 0 0 89844 168 0 0 25 0 1 0 542177677 301576192 64542 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73627 64542 603 41 0 73586 0
vsize: 294508
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68242 0 0 0 90844 168 0 0 25 0 1 0 542177677 301576192 64555 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73627 64555 603 41 0 73586 0
vsize: 294508
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68262 0 0 0 91844 168 0 0 25 0 1 0 542177677 301707264 64575 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73659 64575 603 41 0 73618 0
vsize: 294636
[startup+930.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68279 0 0 0 92844 168 0 0 25 0 1 0 542177677 301838336 64592 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73691 64592 603 41 0 73650 0
vsize: 294764
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68375 0 0 0 93844 169 0 0 25 0 1 0 542177677 302239744 64688 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73789 64688 603 41 0 73748 0
vsize: 295156
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68413 0 0 0 94844 169 0 0 25 0 1 0 542177677 302374912 64726 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73822 64726 603 41 0 73781 0
vsize: 295288
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68506 0 0 0 95844 169 0 0 25 0 1 0 542177677 302780416 64819 4294967295 134512640 134672761 3221224528 3221223728 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73921 64819 603 41 0 73880 0
vsize: 295684
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68520 0 0 0 96844 169 0 0 25 0 1 0 542177677 302776320 64833 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73920 64833 603 41 0 73879 0
vsize: 295680
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 68725 0 0 0 97844 170 0 0 25 0 1 0 542177677 303579136 65038 4294967295 134512640 134672761 3221224528 3221223632 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74116 65038 603 41 0 74075 0
vsize: 296464
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 69205 0 0 0 98843 171 0 0 25 0 1 0 542177677 305582080 65518 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74605 65518 603 41 0 74564 0
vsize: 298420
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 69699 0 0 0 99841 172 0 0 25 0 1 0 542177677 307593216 66012 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75096 66012 603 41 0 75055 0
vsize: 300384
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 70119 0 0 0 100840 174 0 0 25 0 1 0 542177677 309346304 66432 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75524 66432 603 41 0 75483 0
vsize: 302096
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 70416 0 0 0 101839 175 0 0 25 0 1 0 542177677 310546432 66729 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75817 66729 603 41 0 75776 0
vsize: 303268
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 70775 0 0 0 102839 176 0 0 25 0 1 0 542177677 312025088 67088 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76178 67088 603 41 0 76137 0
vsize: 304712
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 70994 0 0 0 103838 176 0 0 25 0 1 0 542177677 312832000 67307 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76375 67307 603 41 0 76334 0
vsize: 305500
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 71186 0 0 0 104838 177 0 0 25 0 1 0 542177677 313630720 67499 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76570 67499 603 41 0 76529 0
vsize: 306280
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 71448 0 0 0 105837 178 0 0 25 0 1 0 542177677 314703872 67761 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76832 67761 603 41 0 76791 0
vsize: 307328
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 71855 0 0 0 106837 178 0 0 25 0 1 0 542177677 316440576 68168 4294967295 134512640 134672761 3221224528 3221223680 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77256 68168 603 41 0 77215 0
vsize: 309024
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 72268 0 0 0 107836 179 0 0 25 0 1 0 542177677 318029824 68581 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77644 68581 603 41 0 77603 0
vsize: 310576
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 72473 0 0 0 108836 179 0 0 25 0 1 0 542177677 318951424 68786 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77869 68786 603 41 0 77828 0
vsize: 311476
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 72510 0 0 0 109836 180 0 0 25 0 1 0 542177677 319086592 68823 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77902 68823 603 41 0 77861 0
vsize: 311608
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 72537 0 0 0 110836 180 0 0 25 0 1 0 542177677 319221760 68850 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77935 68850 603 41 0 77894 0
vsize: 311740
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 72565 0 0 0 111836 180 0 0 25 0 1 0 542177677 319221760 68878 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77935 68878 603 41 0 77894 0
vsize: 311740
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 72712 0 0 0 112836 180 0 0 25 0 1 0 542177677 319889408 69025 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78098 69025 603 41 0 78057 0
vsize: 312392
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 73151 0 0 0 113835 181 0 0 25 0 1 0 542177677 321634304 69464 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78524 69464 603 41 0 78483 0
vsize: 314096
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 73558 0 0 0 114834 182 0 0 25 0 1 0 542177677 323383296 69871 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78951 69871 603 41 0 78910 0
vsize: 315804
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 74070 0 0 0 115832 184 0 0 25 0 1 0 542177677 325402624 70383 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79444 70383 603 41 0 79403 0
vsize: 317776
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 74551 0 0 0 116831 186 0 0 25 0 1 0 542177677 327684096 70864 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80001 70864 603 41 0 79960 0
vsize: 320004
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 74931 0 0 0 117830 187 0 0 25 0 1 0 542177677 329154560 71244 4294967295 134512640 134672761 3221224528 3221223632 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80360 71244 603 41 0 80319 0
vsize: 321440
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 75369 0 0 0 118829 188 0 0 25 0 1 0 542177677 331038720 71682 4294967295 134512640 134672761 3221224528 3221223632 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80820 71682 603 41 0 80779 0
vsize: 323280
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28627
Raw data (stat): 28627 (minisat+) R 28626 27565 27564 0 -1 0 75823 0 0 0 119828 189 0 0 25 0 1 0 542177677 332910592 72136 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81277 72136 603 41 0 81236 0
vsize: 325108
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 28627
Raw data (stat): 28627 (minisat+) Z 28626 27565 27564 0 -1 12 75825 0 0 0 119828 203 0 0 25 0 1 0 542177677 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.18
CPU time (s): 1200.32
CPU user time (s): 1198.29
CPU system time (s): 2.03469
CPU usage (%): 100.012
Max. virtual memory (Kb): 325108
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####