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/miplib3/normalized-mps-v2-13-7-danoint.opb
MD5SUM	bf9bbda6f586f0b888182a433f63f010
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.39179
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 15189

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        566320 kB
Buffers:         35476 kB
Cached:         409984 kB
SwapCached:          8 kB
Active:          99016 kB
Inactive:       349244 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        566068 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14428 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:38:29 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 18277 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: ppppp
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: 2897
c ---[ 823]---> BDD-cost: 2910
c ---[ 821]---> BDD-cost: 2801
c ---[ 819]---> BDD-cost: 2775
c ---[ 817]---> BDD-cost: 2801
c ---[ 815]---> BDD-cost: 2897
c ---[ 813]---> BDD-cost: 2801
c ---[ 811]---> BDD-cost: 2961
c ---[ 809]---> BDD-cost: 2974
c ---[ 807]---> BDD-cost: 2974
c ---[ 805]---> BDD-cost: 2948
c ---[ 803]---> BDD-cost: 2974
c ---[ 801]---> BDD-cost: 2974
c ---[ 799]---> BDD-cost: 2974
c ---[ 797]---> BDD-cost: 2727
c ---[ 795]---> BDD-cost: 2727
c ---[ 793]---> BDD-cost: 2727
c ---[ 791]---> BDD-cost: 2714
c ---[ 789]---> BDD-cost: 2727
c ---[ 787]---> BDD-cost: 2727
c ---[ 785]---> BDD-cost: 2688
c ---[ 783]---> BDD-cost: 2727
c ---[ 781]---> BDD-cost: 2688
c ---[ 779]---> BDD-cost: 2727
c ---[ 777]---> BDD-cost: 2727
c ---[ 775]---> BDD-cost: 2714
c ---[ 773]---> BDD-cost: 2727
c ---[ 771]---> BDD-cost: 2727
c ---[ 769]---> BDD-cost: 2891
c ---[ 767]---> BDD-cost: 2786
c ---[ 765]---> BDD-cost: 2786
c ---[ 763]---> BDD-cost: 2930
c ---[ 761]---> BDD-cost: 2930
c ---[ 759]---> BDD-cost: 2799
c ---[ 757]---> BDD-cost: 2930
c ---[ 755]---> BDD-cost: 2861
c ---[ 753]---> BDD-cost: 2770
c ---[ 751]---> BDD-cost: 2770
c ---[ 749]---> BDD-cost: 2770
c ---[ 747]---> BDD-cost: 2770
c ---[ 745]---> BDD-cost: 2770
c ---[ 743]---> BDD-cost: 2744
c ---[ 741]---> BDD-cost: 2737
c ---[ 739]---> BDD-cost: 2750
c ---[ 737]---> BDD-cost: 2750
c ---[ 735]---> BDD-cost: 2737
c ---[ 733]---> BDD-cost: 2737
c ---[ 731]---> BDD-cost: 2724
c ---[ 729]---> BDD-cost: 2750
c ---[ 727]---> BDD-cost: 2727
c ---[ 725]---> BDD-cost: 2727
c ---[ 723]---> BDD-cost: 2688
c ---[ 721]---> BDD-cost: 2714
c ---[ 719]---> BDD-cost: 2714
c ---[ 717]---> BDD-cost: 2727
c ---[ 715]---> BDD-cost: 2714
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:  110
c ---[ 712]---> BDD-cost:  110
c ---[ 711]---> BDD-cost:  110
c ---[ 710]---> BDD-cost:  110
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 ---[ 699]---> BDD-cost:  110
c ---[ 698]---> BDD-cost:  110
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:  110
c ---[ 691]---> BDD-cost:  110
c ---[ 690]---> BDD-cost:  110
c ---[ 689]---> BDD-cost:  110
c ---[ 688]---> BDD-cost:  110
c ---[ 687]---> BDD-cost:  110
c ---[ 686]---> BDD-cost:  110
c ---[ 685]---> BDD-cost:  110
c ---[ 684]---> BDD-cost:  110
c ---[ 683]---> BDD-cost:  110
c ---[ 682]---> BDD-cost:  110
c ---[ 681]---> BDD-cost:  110
c ---[ 680]---> BDD-cost:  110
c ---[ 679]---> BDD-cost:  110
c ---[ 678]---> BDD-cost:  110
c ---[ 677]---> BDD-cost:  110
c ---[ 676]---> BDD-cost:  110
c ---[ 675]---> BDD-cost:  110
c ---[ 674]---> BDD-cost:  110
c ---[ 673]---> BDD-cost:  110
c ---[ 672]---> BDD-cost:  110
c ---[ 671]---> BDD-cost:  110
c ---[ 670]---> BDD-cost:  110
c ---[ 669]---> BDD-cost:  110
c ---[ 668]---> BDD-cost:  110
c ---[ 667]---> BDD-cost:  110
c ---[ 666]---> BDD-cost:  110
c ---[ 665]---> BDD-cost:  110
c ---[ 664]---> BDD-cost:  110
c ---[ 663]---> BDD-cost:  110
c ---[ 662]---> BDD-cost:  110
c ---[ 661]---> BDD-cost:  110
c ---[ 660]---> BDD-cost:  110
c ---[ 659]---> BDD-cost:  110
c ---[ 657]---> BDD-cost: 1007
c ---[ 655]---> BDD-cost: 1011
c ---[ 653]---> BDD-cost: 1011
c ---[ 651]---> BDD-cost: 1007
c ---[ 649]---> BDD-cost: 1007
c ---[ 647]---> BDD-cost: 1011
c ---[ 645]---> BDD-cost: 1011
c ---[ 643]---> BDD-cost:  999
c ---[ 641]---> BDD-cost: 1003
c ---[ 639]---> BDD-cost: 1003
c ---[ 637]---> BDD-cost: 1003
c ---[ 635]---> BDD-cost: 1003
c ---[ 633]---> BDD-cost: 1003
c ---[ 631]---> BDD-cost: 1003
c ---[ 629]---> BDD-cost:  999
c ---[ 627]---> BDD-cost:  999
c ---[ 625]---> BDD-cost: 1003
c ---[ 623]---> BDD-cost: 1003
c ---[ 621]---> BDD-cost: 1003
c ---[ 619]---> BDD-cost: 1003
c ---[ 617]---> BDD-cost: 1003
c ---[ 615]---> BDD-cost: 1003
c ---[ 613]---> BDD-cost:  999
c ---[ 611]---> BDD-cost: 1003
c ---[ 609]---> BDD-cost:  999
c ---[ 607]---> BDD-cost: 1003
c ---[ 605]---> BDD-cost: 1003
c ---[ 603]---> BDD-cost: 1003
c ---[ 601]---> BDD-cost: 1003
c ---[ 599]---> BDD-cost:  999
c ---[ 597]---> BDD-cost: 1003
c ---[ 595]---> BDD-cost: 1003
c ---[ 593]---> BDD-cost: 1003
c ---[ 591]---> BDD-cost: 1003
c ---[ 589]---> BDD-cost: 1003
c ---[ 587]---> BDD-cost: 1007
c ---[ 585]---> BDD-cost: 1003
c ---[ 583]---> BDD-cost: 1007
c ---[ 581]---> BDD-cost: 1007
c ---[ 579]---> BDD-cost: 1003
c ---[ 577]---> BDD-cost: 1007
c ---[ 575]---> BDD-cost: 1007
c ---[ 573]---> BDD-cost: 1003
c ---[ 571]---> BDD-cost: 1003
c ---[ 569]---> BDD-cost: 1007
c ---[ 567]---> BDD-cost: 1007
c ---[ 565]---> BDD-cost: 1007
c ---[ 563]---> BDD-cost: 1007
c ---[ 561]---> BDD-cost: 1007
c ---[ 559]---> BDD-cost: 1003
c ---[ 557]---> BDD-cost:  999
c ---[ 555]---> BDD-cost: 1003
c ---[ 553]---> BDD-cost: 1003
c ---[ 551]---> BDD-cost:  999
c ---[ 549]---> BDD-cost: 1003
c ---[ 547]---> BDD-cost: 1003
c ---[ 545]---> BDD-cost:44747
c ---[ 543]---> BDD-cost:46823
c ---[ 541]---> BDD-cost:43148
c ---[ 539]---> BDD-cost:43148
c ---[ 537]---> BDD-cost:45192
c ---[ 535]---> BDD-cost:43886
c ---[ 533]---> BDD-cost:43523
c ---[ 531]---> BDD-cost:43148
c ---[ 529]---> BDD-cost:   15
c ---[ 527]---> BDD-cost:   15
c ---[ 525]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   15
c ---[ 521]---> BDD-cost:   15
c ---[ 519]---> BDD-cost:   15
c ---[ 517]---> BDD-cost:   15
c ---[ 515]---> BDD-cost:   15
c ---[ 513]---> BDD-cost:   15
c ---[ 511]---> BDD-cost:   15
c ---[ 509]---> BDD-cost:   15
c ---[ 507]---> BDD-cost:   15
c ---[ 505]---> BDD-cost:   15
c ---[ 503]---> BDD-cost:   15
c ---[ 501]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> BDD-cost:  868
c ---[ 497]---> BDD-cost:  887
c ---[ 496]---> BDD-cost:  938
c ---[ 495]---> BDD-cost:  798
c ---[ 494]---> BDD-cost:  938
c ---[ 493]---> BDD-cost:  817
c ---[ 492]---> BDD-cost:  938
c ---[ 491]---> BDD-cost:  868
c ---[ 490]---> BDD-cost:  950
c ---[ 489]---> BDD-cost:  950
c ---[ 488]---> BDD-cost:  810
c ---[ 487]---> BDD-cost:  950
c ---[ 486]---> BDD-cost:  950
c ---[ 485]---> BDD-cost:  950
c ---[ 484]---> BDD-cost:  849
c ---[ 483]---> BDD-cost:  859
c ---[ 482]---> BDD-cost:  859
c ---[ 481]---> BDD-cost:  747
c ---[ 480]---> BDD-cost:  817
c ---[ 479]---> BDD-cost:  859
c ---[ 478]---> BDD-cost:  670
c ---[ 477]---> BDD-cost:  807
c ---[ 476]---> BDD-cost:  670
c ---[ 475]---> BDD-cost:  859
c ---[ 474]---> BDD-cost:  817
c ---[ 473]---> BDD-cost:  747
c ---[ 472]---> BDD-cost:  859
c ---[ 471]---> BDD-cost:  859
c ---[ 470]---> BDD-cost:  730
c ---[ 469]---> BDD-cost:  798
c ---[ 468]---> BDD-cost:  798
c ---[ 467]---> BDD-cost:  950
c ---[ 466]---> BDD-cost:  950
c ---[ 465]---> BDD-cost:  868
c ---[ 464]---> BDD-cost:  950
c ---[ 463]---> BDD-cost:  877
c ---[ 462]---> BDD-cost:  938
c ---[ 461]---> BDD-cost:  938
c ---[ 460]---> BDD-cost:  875
c ---[ 459]---> BDD-cost:  938
c ---[ 458]---> BDD-cost:  938
c ---[ 457]---> BDD-cost:  798
c ---[ 456]---> BDD-cost:  795
c ---[ 455]---> BDD-cost:  938
c ---[ 454]---> BDD-cost:  875
c ---[ 453]---> BDD-cost:  868
c ---[ 452]---> BDD-cost:  868
c ---[ 451]---> BDD-cost:  798
c ---[ 450]---> BDD-cost:  875
c ---[ 449]---> BDD-cost:  849
c ---[ 448]---> BDD-cost:  817
c ---[ 447]---> BDD-cost:  670
c ---[ 446]---> BDD-cost:  747
c ---[ 445]---> BDD-cost:  789
c ---[ 444]---> BDD-cost:  817
c ---[ 443]---> BDD-cost:  789
c ---[ 441]---> BDD-cost: 1004
c ---[ 439]---> BDD-cost: 1018
c ---[ 437]---> BDD-cost: 1038
c ---[ 435]---> BDD-cost: 1038
c ---[ 433]---> BDD-cost: 1012
c ---[ 431]---> BDD-cost: 1004
c ---[ 429]---> BDD-cost: 1057
c ---[ 427]---> BDD-cost: 1038
c ---[ 410]---> BDD-cost:   22
c ---[ 409]---> BDD-cost:   22
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   22
c ---[ 406]---> BDD-cost:   22
c ---[ 405]---> BDD-cost:   22
c ---[ 404]---> BDD-cost:   22
c ---[ 403]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 401]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 399]---> BDD-cost:   15
c ---[ 398]---> BDD-cost:   15
c ---[ 397]---> BDD-cost:   22
c ---[ 396]---> BDD-cost:   22
c ---[ 395]---> BDD-cost:   22
c ---[ 394]---> BDD-cost:   22
c ---[ 393]---> BDD-cost:   22
c ---[ 392]---> BDD-cost:   22
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:   19
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   19
c ---[ 387]---> BDD-cost:   19
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   18
c ---[ 384]---> BDD-cost:   18
c ---[ 383]---> BDD-cost:   18
c ---[ 382]---> BDD-cost:   18
c ---[ 381]---> BDD-cost:   18
c ---[ 380]---> BDD-cost:   18
c ---[ 379]---> BDD-cost:   19
c ---[ 378]---> BDD-cost:   19
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:   19
c ---[ 375]---> BDD-cost:   19
c ---[ 374]---> BDD-cost:   19
c ---[ 373]---> BDD-cost:   22
c ---[ 372]---> BDD-cost:   22
c ---[ 371]---> BDD-cost:   22
c ---[ 370]---> BDD-cost:   22
c ---[ 369]---> BDD-cost:   22
c ---[ 368]---> BDD-cost:   22
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> BDD-cost:   19
c ---[ 365]---> BDD-cost:   19
c ---[ 364]---> BDD-cost:   19
c ---[ 363]---> BDD-cost:   19
c ---[ 362]---> BDD-cost:   19
c ---[ 361]---> BDD-cost:   22
c ---[ 360]---> BDD-cost:   22
c ---[ 359]---> BDD-cost:   22
c ---[ 358]---> BDD-cost:   22
c ---[ 357]---> BDD-cost:   22
c ---[ 356]---> BDD-cost:   22
c ---[ 355]---> BDD-cost:   22
c ---[ 354]---> BDD-cost:   22
c ---[ 353]---> BDD-cost:   22
c ---[ 352]---> BDD-cost:   22
c ---[ 351]---> BDD-cost:   22
c ---[ 350]---> BDD-cost:   22
c ---[ 349]---> BDD-cost:   22
c ---[ 348]---> BDD-cost:   20
c ---[ 347]---> BDD-cost:   20
c ---[ 346]---> BDD-cost:   20
c ---[ 345]---> BDD-cost:   20
c ---[ 344]---> BDD-cost:   20
c ---[ 343]---> BDD-cost:   20
c ---[ 342]---> BDD-cost:   22
c ---[ 341]---> BDD-cost:   22
c ---[ 340]---> BDD-cost:   22
c ---[ 339]---> BDD-cost:   22
c ---[ 338]---> BDD-cost:   22
c ---[ 337]---> BDD-cost:   22
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   22
c ---[ 334]---> BDD-cost:   22
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   22
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:   22
c ---[ 329]---> BDD-cost:   22
c ---[ 328]---> BDD-cost:   22
c ---[ 327]---> BDD-cost:   22
c ---[ 326]---> BDD-cost:   22
c ---[ 325]---> BDD-cost:   22
c ---[ 324]---> BDD-cost:   22
c ---[ 323]---> BDD-cost:   22
c ---[ 322]---> BDD-cost:   22
c ---[ 321]---> BDD-cost:   22
c ---[ 320]---> BDD-cost:   22
c ---[ 319]---> BDD-cost:   22
c ---[ 318]---> BDD-cost:   22
c ---[ 317]---> BDD-cost:   22
c ---[ 316]---> BDD-cost:   22
c ---[ 315]---> BDD-cost:   22
c ---[ 314]---> BDD-cost:   22
c ---[ 313]---> BDD-cost:   22
c ---[ 312]---> BDD-cost:   18
c ---[ 311]---> BDD-cost:   18
c ---[ 310]---> BDD-cost:   18
c ---[ 309]---> BDD-cost:   18
c ---[ 308]---> BDD-cost:   18
c ---[ 307]---> BDD-cost:   18
c ---[ 306]---> BDD-cost:   18
c ---[ 305]---> BDD-cost:   18
c ---[ 304]---> BDD-cost:   18
c ---[ 303]---> BDD-cost:   18
c ---[ 302]---> BDD-cost:   18
c ---[ 301]---> BDD-cost:   18
c ---[ 300]---> BDD-cost:   19
c ---[ 299]---> BDD-cost:   19
c ---[ 298]---> BDD-cost:   19
c ---[ 297]---> BDD-cost:   19
c ---[ 296]---> BDD-cost:   19
c ---[ 295]---> BDD-cost:   19
c ---[ 294]---> BDD-cost:   19
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   17
c ---[ 291]---> BDD-cost:   17
c ---[ 290]---> BDD-cost:   17
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   17
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:   19
c ---[ 284]---> BDD-cost:   19
c ---[ 283]---> BDD-cost:   19
c ---[ 282]---> BDD-cost:   19
c ---[ 281]---> BDD-cost:   18
c ---[ 280]---> BDD-cost:   18
c ---[ 279]---> BDD-cost:   18
c ---[ 278]---> BDD-cost:   18
c ---[ 277]---> BDD-cost:   18
c ---[ 276]---> BDD-cost:   18
c ---[ 275]---> BDD-cost:   17
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:   19
c ---[ 268]---> BDD-cost:   19
c ---[ 267]---> BDD-cost:   19
c ---[ 266]---> BDD-cost:   19
c ---[ 265]---> BDD-cost:   19
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   16
c ---[ 262]---> BDD-cost:   16
c ---[ 261]---> BDD-cost:   16
c ---[ 260]---> BDD-cost:   16
c ---[ 259]---> BDD-cost:   16
c ---[ 258]---> BDD-cost:   16
c ---[ 257]---> BDD-cost:   19
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:   19
c ---[ 254]---> BDD-cost:   19
c ---[ 253]---> BDD-cost:   19
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   15
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   15
c ---[ 245]---> BDD-cost:   19
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   19
c ---[ 242]---> BDD-cost:   19
c ---[ 241]---> BDD-cost:   19
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   16
c ---[ 235]---> BDD-cost:   16
c ---[ 234]---> BDD-cost:   16
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   19
c ---[ 231]---> BDD-cost:   19
c ---[ 230]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   19
c ---[ 228]---> BDD-cost:   19
c ---[ 227]---> BDD-cost:   19
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   17
c ---[ 221]---> BDD-cost:   17
c ---[ 220]---> BDD-cost:   18
c ---[ 219]---> BDD-cost:   18
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:   18
c ---[ 215]---> BDD-cost:   18
c ---[ 214]---> BDD-cost:   22
c ---[ 213]---> BDD-cost:   22
c ---[ 212]---> BDD-cost:   22
c ---[ 211]---> BDD-cost:   22
c ---[ 210]---> BDD-cost:   22
c ---[ 209]---> BDD-cost:   22
c ---[ 208]---> BDD-cost:   19
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:   19
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   19
c ---[ 203]---> BDD-cost:   19
c ---[ 202]---> BDD-cost:   19
c ---[ 201]---> BDD-cost:   19
c ---[ 200]---> BDD-cost:   19
c ---[ 199]---> BDD-cost:   19
c ---[ 198]---> BDD-cost:   19
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:   20
c ---[ 195]---> BDD-cost:   20
c ---[ 194]---> BDD-cost:   20
c ---[ 193]---> BDD-cost:   20
c ---[ 192]---> BDD-cost:   20
c ---[ 191]---> BDD-cost:   20
c ---[ 190]---> BDD-cost:   22
c ---[ 189]---> BDD-cost:   22
c ---[ 188]---> BDD-cost:   22
c ---[ 187]---> BDD-cost:   22
c ---[ 186]---> BDD-cost:   22
c ---[ 185]---> BDD-cost:   22
c ---[ 184]---> BDD-cost:   22
c ---[ 183]---> BDD-cost:   20
c ---[ 182]---> BDD-cost:   20
c ---[ 181]---> BDD-cost:   20
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   20
c ---[ 178]---> BDD-cost:   20
c ---[ 177]---> BDD-cost:   19
c ---[ 176]---> BDD-cost:   19
c ---[ 175]---> BDD-cost:   19
c ---[ 174]---> BDD-cost:   19
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> BDD-cost:   19
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   15
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   15
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   15
c ---[ 165]---> BDD-cost:   21
c ---[ 164]---> BDD-cost:   21
c ---[ 163]---> BDD-cost:   21
c ---[ 162]---> BDD-cost:   21
c ---[ 161]---> BDD-cost:   21
c ---[ 160]---> BDD-cost:   21
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 152]---> BDD-cost:   19
c ---[ 151]---> BDD-cost:   19
c ---[ 150]---> BDD-cost:   19
c ---[ 149]---> BDD-cost:   19
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   19
c ---[ 142]---> BDD-cost:   19
c ---[ 141]---> BDD-cost:   19
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:   22
c ---[ 134]---> BDD-cost:   22
c ---[ 133]---> BDD-cost:   22
c ---[ 132]---> BDD-cost:   22
c ---[ 131]---> BDD-cost:   22
c ---[ 130]---> BDD-cost:   22
c ---[ 129]---> BDD-cost:   22
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:   18
c ---[ 121]---> BDD-cost:   18
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   18
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   19
c ---[ 115]---> BDD-cost:   19
c ---[ 114]---> BDD-cost:   19
c ---[ 113]---> BDD-cost:   19
c ---[ 112]---> BDD-cost:   19
c ---[ 111]---> BDD-cost:   19
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   18
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   18
c ---[ 100]---> BDD-cost:   18
c ---[  99]---> BDD-cost:   18
c ---[  98]---> BDD-cost:   19
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:   19
c ---[  90]---> BDD-cost:   19
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   19
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   19
c ---[  82]---> BDD-cost:   19
c ---[  81]---> BDD-cost:   19
c ---[  80]---> BDD-cost:   21
c ---[  79]---> BDD-cost:   21
c ---[  78]---> BDD-cost:   21
c ---[  77]---> BDD-cost:   21
c ---[  76]---> BDD-cost:   21
c ---[  75]---> BDD-cost:   21
c ---[  74]---> BDD-cost:   21
c ---[  73]---> BDD-cost:   18
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   18
c ---[  69]---> BDD-cost:   18
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   18
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   18
c ---[  61]---> BDD-cost:   18
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   18
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   18
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   19
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   19
c ---[  50]---> BDD-cost:   19
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   19
c ---[  46]---> BDD-cost:   19
c ---[  45]---> BDD-cost:   19
c ---[  44]---> BDD-cost:   19
c ---[  43]---> BDD-cost:   19
c ---[  42]---> BDD-cost:   19
c ---[  41]---> BDD-cost:   19
c ---[  40]---> BDD-cost:   19
c ---[  39]---> BDD-cost:   19
c ---[  38]---> BDD-cost:   19
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   16
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:   19
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   19
c ---[  21]---> BDD-cost:   19
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:   49
c ---[  14]---> BDD-cost:   51
c ---[  13]---> BDD-cost:   54
c ---[  12]---> BDD-cost:   54
c ---[  11]---> BDD-cost:   51
c ---[  10]---> BDD-cost:   49
c ---[   9]---> BDD-cost:   54
c ---[   8]---> BDD-cost:   54
c ---[   7]---> BDD-cost:  123
c ---[   6]---> BDD-cost:  170
c ---[   5]---> BDD-cost:  132
c ---[   4]---> BDD-cost:  144
c ---[   3]---> BDD-cost:  165
c ---[   2]---> BDD-cost:  148
c ---[   1]---> BDD-cost:  152
c ---[   0]---> BDD-cost:  132
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1835838  5411810 |  611946       0        0     nan |  0.000 % |
c |       101 | 1835838  5411810 |  673140     101     7239    71.7 |  0.559 % |
c |       251 | 1835838  5411810 |  740454     251    16574    66.0 |  0.559 % |
c |       476 | 1835838  5411810 |  814500     476    44285    93.0 |  0.559 % |
c |       813 | 1835747  5411595 |  895950     797    61606    77.3 |  0.565 % |
c |      1319 | 1835747  5411595 |  985545    1303    99760    76.6 |  0.565 % |
c |      2079 | 1835747  5411595 | 1084099    2063   198935    96.4 |  0.565 % |
c |      3218 | 1835733  5411567 | 1192509    3201   310877    97.1 |  0.566 % |
c |      4926 | 1835733  5411567 | 1311760    4909   496164   101.1 |  0.566 % |
c |      7488 | 1835733  5411567 | 1442936    7471  1066912   142.8 |  0.566 % |
c |     11332 | 1835733  5411567 | 1587230   11315  2084347   184.2 |  0.566 % |
c |     17105 | 1835733  5411567 | 1745953   17088  3094670   181.1 |  0.566 % |
c |     25754 | 1835733  5411567 | 1920548   25737  4787739   186.0 |  0.566 % |
#### 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.85 0.97 0.96 2/54 385
Raw data (stat): 385 (runsolver) R 384 30854 30853 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 483559412 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99993 s]
Raw data (loadavg): 0.87 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 50971 0 0 0 875 123 0 0 25 0 1 0 483559412 238870528 47284 4294967295 134512640 134672761 3221224544 3221070664 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58318 47286 603 41 0 58277 0
vsize: 233272
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57573 0 0 0 1859 140 0 0 25 0 1 0 483559412 257929216 53886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62971 53886 603 41 0 62930 0
vsize: 251884
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57629 0 0 0 2859 140 0 0 25 0 1 0 483559412 258199552 53942 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63037 53942 603 41 0 62996 0
vsize: 252148
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57698 0 0 0 3858 141 0 0 25 0 1 0 483559412 258469888 54011 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63103 54011 603 41 0 63062 0
vsize: 252412
[startup+50.0176 s]
Raw data (loadavg): 0.93 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57756 0 0 0 4859 141 0 0 25 0 1 0 483559412 258605056 54069 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63136 54069 603 41 0 63095 0
vsize: 252544
[startup+60.0176 s]
Raw data (loadavg): 0.94 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57822 0 0 0 5859 141 0 0 25 0 1 0 483559412 258875392 54135 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63202 54135 603 41 0 63161 0
vsize: 252808
[startup+70.0188 s]
Raw data (loadavg): 0.95 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57860 0 0 0 6859 141 0 0 25 0 1 0 483559412 259141632 54173 4294967295 134512640 134672761 3221224544 3221223636 1075351142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63267 54173 603 41 0 63226 0
vsize: 253068
[startup+80.0196 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57882 0 0 0 7859 141 0 0 25 0 1 0 483559412 259141632 54195 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63267 54195 603 41 0 63226 0
vsize: 253068
[startup+90.019 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 57987 0 0 0 8858 141 0 0 25 0 1 0 483559412 259543040 54300 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63365 54300 603 41 0 63324 0
vsize: 253460
[startup+100.02 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58053 0 0 0 9859 141 0 0 25 0 1 0 483559412 259813376 54366 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63431 54366 603 41 0 63390 0
vsize: 253724
[startup+110.021 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58157 0 0 0 10858 142 0 0 25 0 1 0 483559412 260354048 54470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63563 54470 603 41 0 63522 0
vsize: 254252
[startup+120.021 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58217 0 0 0 11858 142 0 0 25 0 1 0 483559412 260489216 54530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63596 54530 603 41 0 63555 0
vsize: 254384
[startup+130.022 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58259 0 0 0 12858 142 0 0 25 0 1 0 483559412 260759552 54572 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63662 54572 603 41 0 63621 0
vsize: 254648
[startup+140.021 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58300 0 0 0 13858 143 0 0 25 0 1 0 483559412 260894720 54613 4294967295 134512640 134672761 3221224544 3221223648 134560267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63695 54613 603 41 0 63654 0
vsize: 254780
[startup+150.022 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58376 0 0 0 14858 143 0 0 25 0 1 0 483559412 261165056 54689 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63761 54689 603 41 0 63720 0
vsize: 255044
[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58463 0 0 0 15858 143 0 0 25 0 1 0 483559412 261570560 54776 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63860 54776 603 41 0 63819 0
vsize: 255440
[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58535 0 0 0 16858 143 0 0 25 0 1 0 483559412 261931008 54848 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63948 54848 603 41 0 63907 0
vsize: 255792
[startup+180.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58590 0 0 0 17858 143 0 0 25 0 1 0 483559412 262066176 54903 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63981 54903 603 41 0 63940 0
vsize: 255924
[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58606 0 0 0 18858 143 0 0 25 0 1 0 483559412 262201344 54919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64014 54919 603 41 0 63973 0
vsize: 256056
[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58686 0 0 0 19858 144 0 0 25 0 1 0 483559412 262467584 54999 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64079 54999 603 41 0 64038 0
vsize: 256316
[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58802 0 0 0 20858 144 0 0 25 0 1 0 483559412 262995968 55115 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64208 55115 603 41 0 64167 0
vsize: 256832
[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58812 0 0 0 21858 144 0 0 25 0 1 0 483559412 262995968 55125 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64208 55125 603 41 0 64167 0
vsize: 256832
[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58826 0 0 0 22859 144 0 0 25 0 1 0 483559412 263131136 55139 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64241 55139 603 41 0 64200 0
vsize: 256964
[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 58894 0 0 0 23859 144 0 0 25 0 1 0 483559412 263393280 55207 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64305 55207 603 41 0 64264 0
vsize: 257220
[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59146 0 0 0 24858 144 0 0 25 0 1 0 483559412 264470528 55459 4294967295 134512640 134672761 3221224544 3221223472 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64568 55459 603 41 0 64527 0
vsize: 258272
[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59328 0 0 0 25858 145 0 0 25 0 1 0 483559412 265142272 55641 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64732 55641 603 41 0 64691 0
vsize: 258928
[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59726 0 0 0 26857 147 0 0 25 0 1 0 483559412 266752000 56039 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65125 56039 603 41 0 65084 0
vsize: 260500
[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59848 0 0 0 27856 147 0 0 25 0 1 0 483559412 267309056 56161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65261 56161 603 41 0 65220 0
vsize: 261044
[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59866 0 0 0 28857 147 0 0 25 0 1 0 483559412 267309056 56179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65261 56179 603 41 0 65220 0
vsize: 261044
[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59888 0 0 0 29857 147 0 0 25 0 1 0 483559412 267440128 56201 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65293 56201 603 41 0 65252 0
vsize: 261172
[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59902 0 0 0 30857 147 0 0 25 0 1 0 483559412 267440128 56215 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65293 56215 603 41 0 65252 0
vsize: 261172
[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59919 0 0 0 31857 147 0 0 25 0 1 0 483559412 267571200 56232 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65325 56232 603 41 0 65284 0
vsize: 261300
[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59941 0 0 0 32857 147 0 0 25 0 1 0 483559412 267706368 56254 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65358 56254 603 41 0 65317 0
vsize: 261432
[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 59973 0 0 0 33857 147 0 0 25 0 1 0 483559412 267837440 56286 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65390 56286 603 41 0 65349 0
vsize: 261560
[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60000 0 0 0 34858 147 0 0 25 0 1 0 483559412 267837440 56313 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65390 56313 603 41 0 65349 0
vsize: 261560
[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60019 0 0 0 35858 147 0 0 25 0 1 0 483559412 267972608 56332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65423 56332 603 41 0 65382 0
vsize: 261692
[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60033 0 0 0 36858 147 0 0 25 0 1 0 483559412 267972608 56346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65423 56346 603 41 0 65382 0
vsize: 261692
[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60065 0 0 0 37858 148 0 0 25 0 1 0 483559412 268107776 56378 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65456 56378 603 41 0 65415 0
vsize: 261824
[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60087 0 0 0 38858 148 0 0 25 0 1 0 483559412 268242944 56400 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65489 56400 603 41 0 65448 0
vsize: 261956
[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60109 0 0 0 39858 148 0 0 25 0 1 0 483559412 268378112 56422 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65522 56422 603 41 0 65481 0
vsize: 262088
[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60142 0 0 0 40858 148 0 0 25 0 1 0 483559412 268513280 56455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65555 56455 603 41 0 65514 0
vsize: 262220
[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60172 0 0 0 41858 148 0 0 25 0 1 0 483559412 268644352 56485 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65587 56485 603 41 0 65546 0
vsize: 262348
[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60197 0 0 0 42859 148 0 0 25 0 1 0 483559412 268644352 56510 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65587 56510 603 41 0 65546 0
vsize: 262348
[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60226 0 0 0 43859 148 0 0 25 0 1 0 483559412 268779520 56539 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65620 56539 603 41 0 65579 0
vsize: 262480
[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60247 0 0 0 44859 148 0 0 25 0 1 0 483559412 268910592 56560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65652 56560 603 41 0 65611 0
vsize: 262608
[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60274 0 0 0 45859 148 0 0 25 0 1 0 483559412 269045760 56587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65685 56587 603 41 0 65644 0
vsize: 262740
[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60302 0 0 0 46859 149 0 0 25 0 1 0 483559412 269180928 56615 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65718 56615 603 41 0 65677 0
vsize: 262872
[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60347 0 0 0 47859 149 0 0 25 0 1 0 483559412 269316096 56660 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65751 56660 603 41 0 65710 0
vsize: 263004
[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60378 0 0 0 48859 149 0 0 25 0 1 0 483559412 269451264 56691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65784 56691 603 41 0 65743 0
vsize: 263136
[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60403 0 0 0 49859 149 0 0 25 0 1 0 483559412 269578240 56716 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65815 56716 603 41 0 65774 0
vsize: 263260
[startup+510.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60425 0 0 0 50859 149 0 0 25 0 1 0 483559412 269578240 56738 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65815 56738 603 41 0 65774 0
vsize: 263260
[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60447 0 0 0 51859 149 0 0 25 0 1 0 483559412 269709312 56760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65847 56760 603 41 0 65806 0
vsize: 263388
[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60469 0 0 0 52859 149 0 0 25 0 1 0 483559412 269840384 56782 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65879 56782 603 41 0 65838 0
vsize: 263516
[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60492 0 0 0 53860 149 0 0 25 0 1 0 483559412 269840384 56805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65879 56805 603 41 0 65838 0
vsize: 263516
[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60533 0 0 0 54859 150 0 0 25 0 1 0 483559412 270102528 56846 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65943 56846 603 41 0 65902 0
vsize: 263772
[startup+560.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60560 0 0 0 55860 150 0 0 25 0 1 0 483559412 270237696 56873 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65976 56873 603 41 0 65935 0
vsize: 263904
[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60599 0 0 0 56860 150 0 0 25 0 1 0 483559412 270368768 56912 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66008 56912 603 41 0 65967 0
vsize: 264032
[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60630 0 0 0 57860 150 0 0 25 0 1 0 483559412 270503936 56943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66041 56943 603 41 0 66000 0
vsize: 264164
[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60664 0 0 0 58860 150 0 0 25 0 1 0 483559412 270630912 56977 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66072 56977 603 41 0 66031 0
vsize: 264288
[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60693 0 0 0 59860 150 0 0 25 0 1 0 483559412 270766080 57006 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66105 57006 603 41 0 66064 0
vsize: 264420
[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60733 0 0 0 60860 150 0 0 25 0 1 0 483559412 271007744 57046 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66164 57046 603 41 0 66123 0
vsize: 264656
[startup+620.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60758 0 0 0 61860 150 0 0 25 0 1 0 483559412 271007744 57071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66164 57071 603 41 0 66123 0
vsize: 264656
[startup+630.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60793 0 0 0 62860 151 0 0 25 0 1 0 483559412 271138816 57106 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66196 57106 603 41 0 66155 0
vsize: 264784
[startup+640.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60820 0 0 0 63860 151 0 0 25 0 1 0 483559412 271269888 57133 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66228 57133 603 41 0 66187 0
vsize: 264912
[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60854 0 0 0 64860 151 0 0 25 0 1 0 483559412 271405056 57167 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66261 57167 603 41 0 66220 0
vsize: 265044
[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60886 0 0 0 65860 151 0 0 25 0 1 0 483559412 271540224 57199 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66294 57199 603 41 0 66253 0
vsize: 265176
[startup+670.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60903 0 0 0 66860 151 0 0 25 0 1 0 483559412 271675392 57216 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66327 57216 603 41 0 66286 0
vsize: 265308
[startup+680.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60908 0 0 0 67860 151 0 0 25 0 1 0 483559412 271675392 57221 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66327 57221 603 41 0 66286 0
vsize: 265308
[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 60949 0 0 0 68860 151 0 0 25 0 1 0 483559412 271810560 57262 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66360 57262 603 41 0 66319 0
vsize: 265440
[startup+700.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61073 0 0 0 69860 151 0 0 25 0 1 0 483559412 272216064 57386 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66459 57386 603 41 0 66418 0
vsize: 265836
[startup+710.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61083 0 0 0 70860 151 0 0 25 0 1 0 483559412 272347136 57396 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66491 57396 603 41 0 66450 0
vsize: 265964
[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61101 0 0 0 71861 151 0 0 25 0 1 0 483559412 272347136 57414 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66491 57414 603 41 0 66450 0
vsize: 265964
[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61121 0 0 0 72861 151 0 0 25 0 1 0 483559412 272482304 57434 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66524 57434 603 41 0 66483 0
vsize: 266096
[startup+740.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61154 0 0 0 73861 151 0 0 25 0 1 0 483559412 272617472 57467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66557 57467 603 41 0 66516 0
vsize: 266228
[startup+750.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61170 0 0 0 74861 151 0 0 25 0 1 0 483559412 272617472 57483 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66557 57483 603 41 0 66516 0
vsize: 266228
[startup+760.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61219 0 0 0 75861 152 0 0 25 0 1 0 483559412 272887808 57532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66623 57532 603 41 0 66582 0
vsize: 266492
[startup+770.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61262 0 0 0 76861 152 0 0 25 0 1 0 483559412 273022976 57575 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66656 57575 603 41 0 66615 0
vsize: 266624
[startup+780.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61323 0 0 0 77861 152 0 0 25 0 1 0 483559412 273293312 57636 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66722 57636 603 41 0 66681 0
vsize: 266888
[startup+790.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61364 0 0 0 78861 152 0 0 25 0 1 0 483559412 273428480 57677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66755 57677 603 41 0 66714 0
vsize: 267020
[startup+800.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61399 0 0 0 79861 152 0 0 25 0 1 0 483559412 273563648 57712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66788 57712 603 41 0 66747 0
vsize: 267152
[startup+810.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61424 0 0 0 80861 152 0 0 25 0 1 0 483559412 273698816 57737 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66821 57737 603 41 0 66780 0
vsize: 267284
[startup+820.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61474 0 0 0 81861 153 0 0 25 0 1 0 483559412 273829888 57787 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66853 57787 603 41 0 66812 0
vsize: 267412
[startup+830.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61510 0 0 0 82862 153 0 0 25 0 1 0 483559412 274087936 57823 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66916 57823 603 41 0 66875 0
vsize: 267664
[startup+840.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61545 0 0 0 83861 153 0 0 25 0 1 0 483559412 274219008 57858 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66948 57858 603 41 0 66907 0
vsize: 267792
[startup+850.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61584 0 0 0 84862 153 0 0 25 0 1 0 483559412 274350080 57897 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66980 57897 603 41 0 66939 0
vsize: 267920
[startup+860.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61695 0 0 0 85861 153 0 0 25 0 1 0 483559412 274755584 58008 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67079 58008 603 41 0 67038 0
vsize: 268316
[startup+870.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61720 0 0 0 86861 154 0 0 25 0 1 0 483559412 274890752 58033 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67112 58033 603 41 0 67071 0
vsize: 268448
[startup+880.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61750 0 0 0 87861 154 0 0 25 0 1 0 483559412 275025920 58063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67145 58063 603 41 0 67104 0
vsize: 268580
[startup+890.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61773 0 0 0 88862 154 0 0 25 0 1 0 483559412 275161088 58086 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67178 58086 603 41 0 67137 0
vsize: 268712
[startup+900.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61808 0 0 0 89862 154 0 0 25 0 1 0 483559412 275292160 58121 4294967295 134512640 134672761 3221224544 3221223728 134559463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67210 58121 603 41 0 67169 0
vsize: 268840
[startup+910.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 61971 0 0 0 90861 154 0 0 25 0 1 0 483559412 275968000 58284 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67375 58284 603 41 0 67334 0
vsize: 269500
[startup+920.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62284 0 0 0 91861 155 0 0 25 0 1 0 483559412 277176320 58597 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67670 58597 603 41 0 67629 0
vsize: 270680
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62316 0 0 0 92861 155 0 0 25 0 1 0 483559412 277311488 58629 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67703 58629 603 41 0 67662 0
vsize: 270812
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62456 0 0 0 93861 155 0 0 25 0 1 0 483559412 277852160 58769 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67835 58769 603 41 0 67794 0
vsize: 271340
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62610 0 0 0 94861 155 0 0 25 0 1 0 483559412 278532096 58923 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68001 58923 603 41 0 67960 0
vsize: 272004
[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62668 0 0 0 95861 156 0 0 25 0 1 0 483559412 278802432 58981 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68067 58981 603 41 0 68026 0
vsize: 272268
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62691 0 0 0 96860 156 0 0 25 0 1 0 483559412 278802432 59004 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68067 59004 603 41 0 68026 0
vsize: 272268
[startup+980.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62738 0 0 0 97860 157 0 0 25 0 1 0 483559412 279068672 59051 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68132 59051 603 41 0 68091 0
vsize: 272528
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62774 0 0 0 98859 157 0 0 25 0 1 0 483559412 279203840 59087 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68165 59087 603 41 0 68124 0
vsize: 272660
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62809 0 0 0 99859 157 0 0 25 0 1 0 483559412 279339008 59122 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68198 59122 603 41 0 68157 0
vsize: 272792
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62853 0 0 0 100859 158 0 0 25 0 1 0 483559412 279474176 59166 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68231 59166 603 41 0 68190 0
vsize: 272924
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62868 0 0 0 101859 158 0 0 25 0 1 0 483559412 279605248 59181 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68263 59181 603 41 0 68222 0
vsize: 273052
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62882 0 0 0 102859 158 0 0 25 0 1 0 483559412 279605248 59195 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68263 59195 603 41 0 68222 0
vsize: 273052
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62900 0 0 0 103859 159 0 0 25 0 1 0 483559412 279736320 59213 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68295 59213 603 41 0 68254 0
vsize: 273180
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62914 0 0 0 104858 159 0 0 25 0 1 0 483559412 279736320 59227 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68295 59227 603 41 0 68254 0
vsize: 273180
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62929 0 0 0 105858 160 0 0 25 0 1 0 483559412 279871488 59242 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68328 59242 603 41 0 68287 0
vsize: 273312
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62954 0 0 0 106857 160 0 0 25 0 1 0 483559412 279871488 59267 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68328 59267 603 41 0 68287 0
vsize: 273312
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 62984 0 0 0 107857 160 0 0 25 0 1 0 483559412 280002560 59297 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68360 59297 603 41 0 68319 0
vsize: 273440
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63019 0 0 0 108857 161 0 0 25 0 1 0 483559412 280133632 59332 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68392 59332 603 41 0 68351 0
vsize: 273568
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63049 0 0 0 109857 161 0 0 25 0 1 0 483559412 280264704 59362 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68424 59362 603 41 0 68383 0
vsize: 273696
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63082 0 0 0 110856 162 0 0 25 0 1 0 483559412 280391680 59395 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68455 59395 603 41 0 68414 0
vsize: 273820
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63114 0 0 0 111856 162 0 0 25 0 1 0 483559412 280526848 59427 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68488 59427 603 41 0 68447 0
vsize: 273952
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63149 0 0 0 112855 163 0 0 25 0 1 0 483559412 280662016 59462 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68521 59462 603 41 0 68480 0
vsize: 274084
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63186 0 0 0 113855 163 0 0 25 0 1 0 483559412 280797184 59499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68554 59499 603 41 0 68513 0
vsize: 274216
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63224 0 0 0 114855 164 0 0 25 0 1 0 483559412 281067520 59537 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68620 59537 603 41 0 68579 0
vsize: 274480
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63262 0 0 0 115855 164 0 0 25 0 1 0 483559412 281198592 59575 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68652 59575 603 41 0 68611 0
vsize: 274608
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63291 0 0 0 116854 165 0 0 25 0 1 0 483559412 281329664 59604 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68684 59604 603 41 0 68643 0
vsize: 274736
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63322 0 0 0 117854 165 0 0 25 0 1 0 483559412 281464832 59635 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68717 59635 603 41 0 68676 0
vsize: 274868
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63349 0 0 0 118854 166 0 0 25 0 1 0 483559412 281464832 59662 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68717 59662 603 41 0 68676 0
vsize: 274868
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 385
Raw data (stat): 385 (minisat+) R 384 30854 30853 0 -1 0 63377 0 0 0 119854 166 0 0 25 0 1 0 483559412 281595904 59690 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68749 59690 603 41 0 68708 0
vsize: 274996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.96 1/54 385
Raw data (stat): 385 (minisat+) Z 384 30854 30853 0 -1 12 63379 0 0 0 119854 177 0 0 25 0 1 0 483559412 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.19
CPU time (s): 1200.33
CPU user time (s): 1198.55
CPU system time (s): 1.77973
CPU usage (%): 100.011
Max. virtual memory (Kb): 274996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####