PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-nsrand_ipx.opb
MD5SUM	1b24e93bee48f2c98e7d4820cbb13e8e
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483485
Optimality of the best value was proved	NO
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1073741824
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	26715880447
Number of bits of the biggest sum of numbers	35
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1225.16
Number of variables	6651
Total number of constraints	7355
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	6951
Number of constraints which are nor clauses,nor cardinality constraints	404
Minimum length of a constraint	1
Maximum length of a constraint	6651
Trace number 30969

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-05-25 21:09:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22351 boxname=wulflinc29 idbench=1167 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  1b24e93bee48f2c98e7d4820cbb13e8e  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-nsrand_ipx.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-nsrand_ipx.opb
IDLAUNCH: 22351
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        535112 kB
Buffers:         35356 kB
Cached:         438424 kB
SwapCached:        452 kB
Active:          39884 kB
Inactive:       439248 kB
HighTotal:      131008 kB
HighFree:        13692 kB
LowTotal:       903652 kB
LowFree:        521420 kB
SwapTotal:     2097892 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            14608 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:30:26 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22351 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 721 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): ss.ssss.sssssssss.s.ssss.s.sss.ss.ss.ss.sssssssssssssssssssssssssssssssssssss.ssssssssssss..sssssssssssssssssssssssss.sssss..ssssssssss.ss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssss.sssssssssssssssssssssssssssssssssssssss.s.sss.ssss.sssss.ssss..sssssssssssssss.sssssssssss.s.ss.sssssssssssss.ss.sss..ss.s.ssssssss.s.s.s.ss.s.sss.ssssss.ss.s.sss.s.ss.ssssssssssssss.
c ---[1049]---> Adder-cost: 38230   maxlim: 24568396799   bits: 35/35
c ---[ 967]---> Adder-cost: 2264   maxlim: 44   bits: 7/6
c ---[ 966]---> Adder-cost: 1410   maxlim: 36   bits: 7/6
c ---[ 965]---> Adder-cost: 1190   maxlim: 36   bits: 7/6
c ---[ 949]---> Adder-cost: 2364   maxlim: 37   bits: 7/6
c ---[ 948]---> Adder-cost: 1680   maxlim: 32   bits: 7/6
c ---[ 659]---> BDD-cost:   37
c ---[ 658]---> BDD-cost:   37
c ---[ 657]---> BDD-cost:   37
c ---[ 656]---> BDD-cost:   37
c ---[ 655]---> BDD-cost:   37
c ---[ 654]---> BDD-cost:   37
c ---[ 653]---> BDD-cost:   37
c ---[ 652]---> BDD-cost:   37
c ---[ 651]---> BDD-cost:   37
c ---[ 650]---> BDD-cost:   37
c ---[ 649]---> BDD-cost:   37
c ---[ 648]---> BDD-cost:   37
c ---[ 647]---> BDD-cost:   37
c ---[ 646]---> BDD-cost:   37
c ---[ 645]---> BDD-cost:   37
c ---[ 644]---> BDD-cost:   37
c ---[ 643]---> BDD-cost:   37
c ---[ 642]---> BDD-cost:   37
c ---[ 641]---> BDD-cost:   37
c ---[ 640]---> BDD-cost:   37
c ---[ 639]---> BDD-cost:   37
c ---[ 638]---> BDD-cost:   37
c ---[ 637]---> BDD-cost:   37
c ---[ 636]---> BDD-cost:   37
c ---[ 635]---> BDD-cost:   37
c ---[ 634]---> BDD-cost:   37
c ---[ 633]---> BDD-cost:   37
c ---[ 632]---> BDD-cost:   37
c ---[ 631]---> BDD-cost:   37
c ---[ 630]---> BDD-cost:   37
c ---[ 629]---> BDD-cost:   37
c ---[ 628]---> BDD-cost:   37
c ---[ 627]---> BDD-cost:   37
c ---[ 626]---> BDD-cost:   37
c ---[ 625]---> BDD-cost:   37
c ---[ 624]---> BDD-cost:   37
c ---[ 623]---> BDD-cost:   37
c ---[ 622]---> BDD-cost:   37
c ---[ 621]---> BDD-cost:   37
c ---[ 620]---> BDD-cost:   37
c ---[ 619]---> BDD-cost:   37
c ---[ 618]---> BDD-cost:   37
c ---[ 617]---> BDD-cost:   37
c ---[ 616]---> BDD-cost:   37
c ---[ 615]---> BDD-cost:   37
c ---[ 614]---> BDD-cost:   37
c ---[ 613]---> BDD-cost:   37
c ---[ 612]---> BDD-cost:   37
c ---[ 611]---> BDD-cost:   37
c ---[ 610]---> BDD-cost:   37
c ---[ 609]---> BDD-cost:   37
c ---[ 608]---> BDD-cost:   37
c ---[ 607]---> BDD-cost:   37
c ---[ 606]---> BDD-cost:   37
c ---[ 605]---> BDD-cost:   37
c ---[ 604]---> BDD-cost:   37
c ---[ 603]---> BDD-cost:   37
c ---[ 602]---> BDD-cost:   37
c ---[ 601]---> BDD-cost:   37
c ---[ 600]---> BDD-cost:   37
c ---[ 599]---> BDD-cost:   37
c ---[ 598]---> BDD-cost:   37
c ---[ 597]---> BDD-cost:   37
c ---[ 596]---> BDD-cost:   37
c ---[ 595]---> BDD-cost:   37
c ---[ 594]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   37
c ---[ 592]---> BDD-cost:   37
c ---[ 591]---> BDD-cost:   37
c ---[ 590]---> BDD-cost:   37
c ---[ 589]---> BDD-cost:   37
c ---[ 588]---> BDD-cost:   37
c ---[ 587]---> BDD-cost:   37
c ---[ 586]---> BDD-cost:   37
c ---[ 585]---> BDD-cost:   37
c ---[ 584]---> BDD-cost:   37
c ---[ 583]---> BDD-cost:   37
c ---[ 582]---> BDD-cost:   37
c ---[ 581]---> BDD-cost:   37
c ---[ 580]---> BDD-cost:   37
c ---[ 579]---> BDD-cost:   37
c ---[ 578]---> BDD-cost:   37
c ---[ 577]---> BDD-cost:   37
c ---[ 576]---> BDD-cost:   37
c ---[ 575]---> BDD-cost:   37
c ---[ 574]---> BDD-cost:   37
c ---[ 573]---> BDD-cost:   37
c ---[ 572]---> BDD-cost:   37
c ---[ 571]---> BDD-cost:   37
c ---[ 570]---> BDD-cost:   37
c ---[ 569]---> BDD-cost:   37
c ---[ 568]---> BDD-cost:   37
c ---[ 567]---> BDD-cost:   37
c ---[ 566]---> BDD-cost:   37
c ---[ 565]---> BDD-cost:   37
c ---[ 564]---> BDD-cost:   37
c ---[ 563]---> BDD-cost:   37
c ---[ 562]---> BDD-cost:   37
c ---[ 561]---> BDD-cost:   37
c ---[ 560]---> BDD-cost:   37
c ---[ 559]---> BDD-cost:   37
c ---[ 558]---> BDD-cost:   37
c ---[ 557]---> BDD-cost:   37
c ---[ 556]---> BDD-cost:   37
c ---[ 555]---> BDD-cost:   37
c ---[ 554]---> BDD-cost:   37
c ---[ 553]---> BDD-cost:   37
c ---[ 552]---> BDD-cost:   37
c ---[ 551]---> BDD-cost:   37
c ---[ 550]---> BDD-cost:   37
c ---[ 549]---> BDD-cost:   37
c ---[ 548]---> BDD-cost:   37
c ---[ 547]---> BDD-cost:   37
c ---[ 546]---> BDD-cost:   37
c ---[ 545]---> BDD-cost:   37
c ---[ 544]---> BDD-cost:   37
c ---[ 543]---> BDD-cost:   37
c ---[ 542]---> BDD-cost:   37
c ---[ 541]---> BDD-cost:   37
c ---[ 540]---> BDD-cost:   37
c ---[ 539]---> BDD-cost:   37
c ---[ 538]---> BDD-cost:   37
c ---[ 537]---> BDD-cost:   37
c ---[ 536]---> BDD-cost:   37
c ---[ 535]---> BDD-cost:   37
c ---[ 534]---> BDD-cost:   37
c ---[ 533]---> BDD-cost:   37
c ---[ 532]---> BDD-cost:   37
c ---[ 531]---> BDD-cost:   37
c ---[ 530]---> BDD-cost:   37
c ---[ 529]---> BDD-cost:   37
c ---[ 528]---> BDD-cost:   37
c ---[ 527]---> BDD-cost:   37
c ---[ 526]---> BDD-cost:   37
c ---[ 525]---> BDD-cost:   37
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:   37
c ---[ 521]---> BDD-cost:   37
c ---[ 520]---> BDD-cost:   37
c ---[ 519]---> BDD-cost:   37
c ---[ 518]---> BDD-cost:   37
c ---[ 517]---> BDD-cost:   37
c ---[ 516]---> BDD-cost:   37
c ---[ 515]---> BDD-cost:   37
c ---[ 514]---> BDD-cost:   37
c ---[ 513]---> BDD-cost:   37
c ---[ 512]---> BDD-cost:   37
c ---[ 511]---> BDD-cost:   37
c ---[ 510]---> BDD-cost:   37
c ---[ 509]---> BDD-cost:   37
c ---[ 508]---> BDD-cost:   37
c ---[ 507]---> BDD-cost:   37
c ---[ 506]---> BDD-cost:   37
c ---[ 505]---> BDD-cost:   37
c ---[ 504]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   37
c ---[ 502]---> BDD-cost:   37
c ---[ 501]---> BDD-cost:   37
c ---[ 500]---> BDD-cost:   37
c ---[ 499]---> BDD-cost:   37
c ---[ 498]---> BDD-cost:   37
c ---[ 497]---> BDD-cost:   37
c ---[ 496]---> BDD-cost:   37
c ---[ 495]---> BDD-cost:   37
c ---[ 494]---> BDD-cost:   37
c ---[ 493]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   37
c ---[ 491]---> BDD-cost:   37
c ---[ 490]---> BDD-cost:   37
c ---[ 489]---> BDD-cost:   37
c ---[ 488]---> BDD-cost:   37
c ---[ 487]---> BDD-cost:   37
c ---[ 486]---> BDD-cost:   37
c ---[ 485]---> BDD-cost:   37
c ---[ 484]---> BDD-cost:   37
c ---[ 483]---> BDD-cost:   37
c ---[ 482]---> BDD-cost:   37
c ---[ 481]---> BDD-cost:   37
c ---[ 480]---> BDD-cost:   37
c ---[ 479]---> BDD-cost:   37
c ---[ 478]---> BDD-cost:   37
c ---[ 477]---> BDD-cost:   37
c ---[ 476]---> BDD-cost:   37
c ---[ 475]---> BDD-cost:   37
c ---[ 474]---> BDD-cost:   37
c ---[ 473]---> BDD-cost:   37
c ---[ 472]---> BDD-cost:   37
c ---[ 471]---> BDD-cost:   37
c ---[ 470]---> BDD-cost:   37
c ---[ 469]---> BDD-cost:   37
c ---[ 468]---> BDD-cost:   37
c ---[ 467]---> BDD-cost:   37
c ---[ 466]---> BDD-cost:   37
c ---[ 465]---> BDD-cost:   37
c ---[ 464]---> BDD-cost:   37
c ---[ 463]---> BDD-cost:   37
c ---[ 462]---> BDD-cost:   37
c ---[ 461]---> BDD-cost:   37
c ---[ 460]---> BDD-cost:   37
c ---[ 459]---> BDD-cost:   37
c ---[ 458]---> BDD-cost:   37
c ---[ 457]---> BDD-cost:   37
c ---[ 456]---> BDD-cost:   37
c ---[ 455]---> BDD-cost:   37
c ---[ 454]---> BDD-cost:   37
c ---[ 453]---> BDD-cost:   37
c ---[ 452]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   37
c ---[ 450]---> BDD-cost:   37
c ---[ 449]---> BDD-cost:   37
c ---[ 448]---> BDD-cost:   37
c ---[ 447]---> BDD-cost:   37
c ---[ 446]---> BDD-cost:   37
c ---[ 445]---> BDD-cost:   37
c ---[ 444]---> BDD-cost:   37
c ---[ 443]---> BDD-cost:   37
c ---[ 442]---> BDD-cost:   37
c ---[ 441]---> BDD-cost:   37
c ---[ 440]---> BDD-cost:   37
c ---[ 439]---> BDD-cost:   37
c ---[ 438]---> BDD-cost:   37
c ---[ 437]---> BDD-cost:   37
c ---[ 436]---> BDD-cost:   37
c ---[ 435]---> BDD-cost:   37
c ---[ 434]---> BDD-cost:   37
c ---[ 433]---> BDD-cost:   37
c ---[ 432]---> BDD-cost:   37
c ---[ 431]---> BDD-cost:   37
c ---[ 430]---> BDD-cost:   37
c ---[ 429]---> BDD-cost:   37
c ---[ 428]---> BDD-cost:   37
c ---[ 427]---> BDD-cost:   37
c ---[ 426]---> BDD-cost:   37
c ---[ 425]---> BDD-cost:   37
c ---[ 424]---> BDD-cost:   37
c ---[ 423]---> BDD-cost:   37
c ---[ 422]---> BDD-cost:   37
c ---[ 421]---> BDD-cost:   37
c ---[ 420]---> BDD-cost:   37
c ---[ 419]---> BDD-cost:   37
c ---[ 418]---> BDD-cost:   37
c ---[ 417]---> BDD-cost:   37
c ---[ 416]---> BDD-cost:   37
c ---[ 415]---> BDD-cost:   37
c ---[ 414]---> BDD-cost:   37
c ---[ 413]---> BDD-cost:   37
c ---[ 412]---> BDD-cost:   37
c ---[ 411]---> BDD-cost:   37
c ---[ 410]---> BDD-cost:   37
c ---[ 409]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 406]---> BDD-cost:   37
c ---[ 405]---> BDD-cost:   37
c ---[ 404]---> BDD-cost:   37
c ---[ 403]---> BDD-cost:   37
c ---[ 402]---> BDD-cost:   37
c ---[ 401]---> BDD-cost:   37
c ---[ 400]---> BDD-cost:   37
c ---[ 399]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   37
c ---[ 397]---> BDD-cost:   37
c ---[ 396]---> BDD-cost:   37
c ---[ 395]---> BDD-cost:   37
c ---[ 394]---> BDD-cost:   37
c ---[ 393]---> BDD-cost:   37
c ---[ 392]---> BDD-cost:   37
c ---[ 391]---> BDD-cost:   37
c ---[ 390]---> BDD-cost:   37
c ---[ 389]---> BDD-cost:   37
c ---[ 388]---> BDD-cost:   37
c ---[ 387]---> BDD-cost:   37
c ---[ 386]---> BDD-cost:   37
c ---[ 385]---> BDD-cost:   37
c ---[ 384]---> BDD-cost:   37
c ---[ 383]---> BDD-cost:   37
c ---[ 382]---> BDD-cost:   37
c ---[ 381]---> BDD-cost:   37
c ---[ 380]---> BDD-cost:   37
c ---[ 379]---> BDD-cost:   37
c ---[ 378]---> BDD-cost:   37
c ---[ 377]---> BDD-cost:   37
c ---[ 376]---> BDD-cost:   37
c ---[ 375]---> BDD-cost:   37
c ---[ 374]---> BDD-cost:   37
c ---[ 373]---> BDD-cost:   37
c ---[ 372]---> BDD-cost:   37
c ---[ 371]---> BDD-cost:   37
c ---[ 370]---> BDD-cost:   37
c ---[ 369]---> BDD-cost:   37
c ---[ 368]---> BDD-cost:   37
c ---[ 367]---> BDD-cost:   37
c ---[ 366]---> BDD-cost:   37
c ---[ 365]---> BDD-cost:   37
c ---[ 364]---> BDD-cost:   37
c ---[ 363]---> BDD-cost:   37
c ---[ 362]---> BDD-cost:   37
c ---[ 361]---> BDD-cost:   37
c ---[ 360]---> BDD-cost:   37
c ---[ 359]---> BDD-cost:   37
c ---[ 358]---> BDD-cost:   37
c ---[ 357]---> BDD-cost:   37
c ---[ 356]---> BDD-cost:   37
c ---[ 355]---> BDD-cost:   37
c ---[ 354]---> BDD-cost:   37
c ---[ 353]---> BDD-cost:   37
c ---[ 352]---> BDD-cost:   37
c ---[ 351]---> BDD-cost:   37
c ---[ 350]---> BDD-cost:   37
c ---[ 349]---> BDD-cost:   37
c ---[ 348]---> BDD-cost:   37
c ---[ 347]---> BDD-cost:   37
c ---[ 346]---> BDD-cost:   37
c ---[ 345]---> BDD-cost:   37
c ---[ 344]---> BDD-cost:   37
c ---[ 343]---> BDD-cost:   37
c ---[ 342]---> BDD-cost:   37
c ---[ 341]---> BDD-cost:   37
c ---[ 340]---> BDD-cost:   37
c ---[ 339]---> BDD-cost:   37
c ---[ 338]---> BDD-cost:   37
c ---[ 337]---> BDD-cost:   37
c ---[ 336]---> BDD-cost:   37
c ---[ 335]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   37
c ---[ 333]---> BDD-cost:   37
c ---[ 332]---> BDD-cost:   37
c ---[ 331]---> BDD-cost:   37
c ---[ 330]---> BDD-cost:   37
c ---[ 329]---> BDD-cost:   37
c ---[ 328]---> BDD-cost:   34
c ---[ 327]---> BDD-cost: 1577
c ---[ 326]---> Adder-cost: 1635   maxlim: 8   bits: 5/4
c ---[ 325]---> Adder-cost: 2523   maxlim: 19   bits: 6/5
c ---[ 324]---> BDD-cost:  932
c ---[ 323]---> Adder-cost: 1387   maxlim: 24   bits: 6/5
c ---[ 322]---> BDD-cost: 1516
c ---[ 321]---> Adder-cost: 1571   maxlim: 17   bits: 6/5
c ---[ 320]---> BDD-cost:  242
c ---[ 319]---> Adder-cost: 324   maxlim: 24   bits: 6/5
c ---[ 318]---> BDD-cost:    1
c ---[ 317]---> BDD-cost:   36
c ---[ 316]---> Adder-cost: 747   maxlim: 20   bits: 6/5
c ---[ 315]---> BDD-cost:    1
c ---[ 314]---> Adder-cost: 615   maxlim: 17   bits: 6/5
c ---[ 313]---> BDD-cost:   18
c ---[ 312]---> BDD-cost:  497
c ---[ 311]---> Adder-cost: 430   maxlim: 16   bits: 6/5
c ---[ 310]---> BDD-cost:  151
c ---[ 309]---> BDD-cost:  101
c ---[ 308]---> Adder-cost: 939   maxlim: 14   bits: 5/4
c ---[ 307]---> BDD-cost:   46
c ---[ 306]---> Adder-cost: 705   maxlim: 11   bits: 5/4
c ---[ 305]---> BDD-cost:   70
c ---[ 304]---> BDD-cost:    1
c ---[ 303]---> Adder-cost: 150   maxlim: 11   bits: 5/4
c ---[ 302]---> BDD-cost:    6
c ---[ 301]---> BDD-cost:    1
c ---[ 300]---> BDD-cost:    1
c ---[ 299]---> BDD-cost:    2
c ---[ 298]---> BDD-cost:   79
c ---[ 297]---> Adder-cost: 533   maxlim: 17   bits: 6/5
c ---[ 296]---> Adder-cost: 616   maxlim: 21   bits: 6/5
c ---[ 295]---> BDD-cost:   32
c ---[ 294]---> Adder-cost: 1111   maxlim: 14   bits: 5/4
c ---[ 293]---> BDD-cost:   24
c ---[ 292]---> Adder-cost: 1229   maxlim: 12   bits: 5/4
c ---[ 291]---> BDD-cost: 1540
c ---[ 290]---> BDD-cost: 2152
c ---[ 289]---> BDD-cost:  135
c ---[ 288]---> BDD-cost: 1724
c ---[ 287]---> Adder-cost: 2144   maxlim: 23   bits: 6/5
c ---[ 286]---> BDD-cost:  135
c ---[ 285]---> Adder-cost: 1076   maxlim: 19   bits: 6/5
c ---[ 284]---> BDD-cost: 1261
c ---[ 283]---> BDD-cost:    1
c ---[ 282]---> BDD-cost:    1
c ---[ 281]---> BDD-cost: 1963
c ---[ 280]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 279]---> BDD-cost:    1
c ---[ 278]---> Adder-cost: 513   maxlim: 20   bits: 6/5
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:  382
c ---[ 275]---> BDD-cost:  656
c ---[ 274]---> Adder-cost: 1496   maxlim: 16   bits: 6/5
c ---[ 273]---> BDD-cost:   14
c ---[ 272]---> BDD-cost:  308
c ---[ 271]---> Adder-cost: 508   maxlim: 12   bits: 5/4
c ---[ 270]---> Adder-cost: 789   maxlim: 11   bits: 5/4
c ---[ 269]---> Adder-cost: 979   maxlim: 10   bits: 5/4
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:    1
c ---[ 266]---> Adder-cost: 858   maxlim: 13   bits: 5/4
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> Adder-cost: 300   maxlim: 13   bits: 5/4
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:   68
c ---[ 260]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 259]---> Adder-cost: 748   maxlim: 28   bits: 6/5
c ---[ 258]---> BDD-cost:  156
c ---[ 257]---> Adder-cost: 568   maxlim: 10   bits: 5/4
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:    1
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 252]---> BDD-cost:   26
c ---[ 251]---> BDD-cost:   37
c ---[ 250]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 249]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 248]---> BDD-cost:   32
c ---[ 247]---> Adder-cost: 373   maxlim: 13   bits: 5/4
c ---[ 246]---> Adder-cost: 807   maxlim: 16   bits: 6/5
c ---[ 245]---> Adder-cost: 988   maxlim: 20   bits: 6/5
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> Adder-cost: 802   maxlim: 17   bits: 6/5
c ---[ 242]---> Adder-cost: 516   maxlim: 16   bits: 6/5
c ---[ 241]---> Adder-cost: 607   maxlim: 20   bits: 6/5
c ---[ 240]---> BDD-cost:   18
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> Adder-cost: 259   maxlim: 13   bits: 5/4
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> Adder-cost: 565   maxlim: 17   bits: 6/5
c ---[ 235]---> BDD-cost:    1
c ---[ 234]---> Adder-cost: 166   maxlim: 17   bits: 6/5
c ---[ 233]---> Adder-cost: 262   maxlim: 22   bits: 6/5
c ---[ 232]---> Adder-cost: 539   maxlim: 20   bits: 6/5
c ---[ 231]---> BDD-cost:    1
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 228]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 227]---> BDD-cost:    1
c ---[ 226]---> Adder-cost: 343   maxlim: 20   bits: 6/5
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> Adder-cost: 1671   maxlim: 15   bits: 5/4
c ---[ 223]---> Adder-cost: 938   maxlim: 13   bits: 5/4
c ---[ 222]---> BDD-cost:   64
c ---[ 221]---> BDD-cost:  250
c ---[ 220]---> Adder-cost: 579   maxlim: 9   bits: 5/4
c ---[ 219]---> BDD-cost:  769
c ---[ 218]---> BDD-cost:   37
c ---[ 217]---> BDD-cost:  977
c ---[ 216]---> BDD-cost:  171
c ---[ 215]---> BDD-cost:   42
c ---[ 214]---> BDD-cost:  250
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[ 211]---> BDD-cost:  817
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   88
c ---[ 208]---> BDD-cost:  491
c ---[ 207]---> BDD-cost:  747
c ---[ 206]---> BDD-cost:  375
c ---[ 205]---> BDD-cost:  471
c ---[ 204]---> Adder-cost: 2690   maxlim: 22   bits: 6/5
c ---[ 203]---> Adder-cost: 1141   maxlim: 12   bits: 5/4
c ---[ 202]---> BDD-cost:   51
c ---[ 201]---> Adder-cost: 1301   maxlim: 12   bits: 5/4
c ---[ 200]---> BDD-cost:  326
c ---[ 199]---> Adder-cost: 752   maxlim: 12   bits: 5/4
c ---[ 198]---> BDD-cost:  394
c ---[ 197]---> Adder-cost: 1099   maxlim: 12   bits: 5/4
c ---[ 196]---> BDD-cost:  232
c ---[ 195]---> BDD-cost: 1615
c ---[ 194]---> Adder-cost: 2354   maxlim: 19   bits: 6/5
c ---[ 193]---> BDD-cost: 2419
c ---[ 192]---> Adder-cost: 1509   maxlim: 17   bits: 6/5
c ---[ 191]---> BDD-cost:  253
c ---[ 190]---> BDD-cost: 1026
c ---[ 189]---> BDD-cost: 1706
c ---[ 188]---> BDD-cost:  242
c ---[ 187]---> Adder-cost: 1293   maxlim: 14   bits: 5/4
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> Adder-cost: 539   maxlim: 22   bits: 6/5
c ---[ 183]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 182]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> Adder-cost: 446   maxlim: 10   bits: 5/4
c ---[ 179]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> Adder-cost: 603   maxlim: 21   bits: 6/5
c ---[ 173]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 172]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 169]---> BDD-cost:  565
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 166]---> Adder-cost: 548   maxlim: 10   bits: 5/4
c ---[ 165]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  871
c ---[ 163]---> BDD-cost: 1115
c ---[ 162]---> BDD-cost:   32
c ---[ 161]---> BDD-cost:  802
c ---[ 160]---> BDD-cost:   25
c ---[ 159]---> Adder-cost: 821   maxlim: 10   bits: 5/4
c ---[ 158]---> BDD-cost:  107
c ---[ 157]---> Adder-cost: 505   maxlim: 9   bits: 5/4
c ---[ 156]---> Adder-cost: 1073   maxlim: 20   bits: 6/5
c ---[ 155]---> Adder-cost: 280   maxlim: 10   bits: 5/4
c ---[ 154]---> Adder-cost: 363   maxlim: 10   bits: 5/4
c ---[ 153]---> Adder-cost: 704   maxlim: 19   bits: 6/5
c ---[ 152]---> BDD-cost:  848
c ---[ 151]---> Adder-cost: 1191   maxlim: 14   bits: 5/4
c ---[ 150]---> BDD-cost:   65
c ---[ 149]---> BDD-cost:  102
c ---[ 148]---> Adder-cost: 479   maxlim: 21   bits: 6/5
c ---[ 147]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 146]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 145]---> BDD-cost:   78
c ---[ 144]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 143]---> BDD-cost:   90
c ---[ 142]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 141]---> BDD-cost: 1065
c ---[ 140]---> BDD-cost:  164
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> Adder-cost: 861   maxlim: 15   bits: 5/4
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost: 1376
c ---[ 135]---> Adder-cost: 635   maxlim: 19   bits: 6/5
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:  688
c ---[ 132]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[ 131]---> BDD-cost:   96
c ---[ 130]---> BDD-cost:   72
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[ 127]---> BDD-cost:  161
c ---[ 126]---> BDD-cost:  170
c ---[ 125]---> Adder-cost: 513   maxlim: 18   bits: 6/5
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> Adder-cost: 215   maxlim: 19   bits: 6/5
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   93
c ---[ 118]---> Adder-cost: 291   maxlim: 18   bits: 6/5
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> Adder-cost: 471   maxlim: 11   bits: 5/4
c ---[ 113]---> BDD-cost:   30
c ---[ 112]---> Adder-cost: 698   maxlim: 14   bits: 5/4
c ---[ 111]---> BDD-cost:   32
c ---[ 110]---> BDD-cost:  879
c ---[ 109]---> Adder-cost: 1221   maxlim: 13   bits: 5/4
c ---[ 108]---> BDD-cost:   72
c ---[ 107]---> BDD-cost:   75
c ---[ 106]---> BDD-cost:  302
c ---[ 105]---> BDD-cost:  303
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:   46
c ---[ 102]---> BDD-cost:  532
c ---[ 101]---> Adder-cost: 480   maxlim: 10   bits: 5/4
c ---[ 100]---> Adder-cost: 807   maxlim: 22   bits: 6/5
c ---[  99]---> BDD-cost:   12
c ---[  98]---> BDD-cost:   86
c ---[  97]---> BDD-cost:  971
c ---[  96]---> Adder-cost: 1489   maxlim: 21   bits: 6/5
c ---[  95]---> BDD-cost:  173
c ---[  94]---> Adder-cost: 689   maxlim: 10   bits: 5/4
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:  170
c ---[  91]---> Adder-cost: 793   maxlim: 19   bits: 6/5
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> Adder-cost: 211   maxlim: 19   bits: 6/5
c ---[  87]---> BDD-cost:   78
c ---[  86]---> Adder-cost: 287   maxlim: 12   bits: 5/4
c ---[  85]---> BDD-cost:   98
c ---[  84]---> Adder-cost: 211   maxlim: 19   bits: 6/5
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> Adder-cost: 687   maxlim: 17   bits: 6/5
c ---[  80]---> BDD-cost:    1
c ---[  79]---> Adder-cost: 542   maxlim: 16   bits: 6/5
c ---[  78]---> BDD-cost:   33
c ---[  77]---> BDD-cost:   92
c ---[  76]---> BDD-cost:  157
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:   22
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:  249
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  62]---> BDD-cost:  182
c ---[  61]---> Adder-cost: 367   maxlim: 12   bits: 5/4
c ---[  60]---> BDD-cost:  135
c ---[  59]---> BDD-cost:   35
c ---[  58]---> BDD-cost:  505
c ---[  57]---> Adder-cost: 468   maxlim: 15   bits: 5/4
c ---[  56]---> Adder-cost: 743   maxlim: 15   bits: 5/4
c ---[  55]---> BDD-cost:    1
c ---[  54]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:  794
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[  48]---> BDD-cost:  132
c ---[  47]---> BDD-cost:    1
c ---[  46]---> Adder-cost: 203   maxlim: 12   bits: 5/4
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:  906
c ---[  43]---> BDD-cost:   62
c ---[  42]---> BDD-cost:  167
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:   19
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:  145
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:  930
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:   24
c ---[  28]---> BDD-cost:    1
c ---[  27]---> Adder-cost: 293   maxlim: 10   bits: 5/4
c ---[  26]---> BDD-cost:    1
c ---[  25]---> Adder-cost: 586   maxlim: 14   bits: 5/4
c ---[  24]---> BDD-cost:    1
c ---[  23]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  22]---> BDD-cost: 2088
c ---[  21]---> Adder-cost: 2558   maxlim: 17   bits: 6/5
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost: 2736
c ---[  18]---> Adder-cost: 371   maxlim: 19   bits: 6/5
c ---[  17]---> Adder-cost: 340   maxlim: 10   bits: 5/4
c ---[  16]---> BDD-cost:  463
c ---[  15]---> BDD-cost:    1
c ---[  14]---> Adder-cost: 748   maxlim: 16   bits: 6/5
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:   72
c ---[  11]---> BDD-cost:  100
c ---[  10]---> Adder-cost: 723   maxlim: 19   bits: 6/5
c ---[   9]---> Adder-cost: 366   maxlim: 13   bits: 5/4
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    2
c ---[   6]---> Adder-cost: 430   maxlim: 18   bits: 6/5
c ---[   5]---> BDD-cost:  767
c ---[   4]---> Adder-cost: 880   maxlim: 9   bits: 5/4
c ---[   3]---> Adder-cost: 1466   maxlim: 21   bits: 6/5
c ---[   2]---> BDD-cost:  889
c ---[   1]---> Adder-cost: 1028   maxlim: 17   bits: 6/5
c ---[   0]---> Adder-cost: 575   maxlim: 9   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  891487  3234678 |  297162       0        0     nan |  0.000 % |
c |       100 |  891487  3234678 |  326878     100      405     4.0 |  0.503 % |
c |       252 |  891487  3234678 |  359566     252     1077     4.3 |  0.503 % |
c |       477 |  891487  3234678 |  395522     477     2177     4.6 |  0.503 % |
c |       814 |  891487  3234678 |  435074     814     3673     4.5 |  0.503 % |
c |      1321 |  891487  3234678 |  478582    1321     6765     5.1 |  0.503 % |
c |      2080 |  891387  3234302 |  526440    2075    11341     5.5 |  0.504 % |
c |      3220 |  891332  3234097 |  579084    3212    17639     5.5 |  0.504 % |
c |      4928 |  891332  3234097 |  636993    4920    29000     5.9 |  0.504 % |
c |      7490 |  891297  3233968 |  700692    7480    55593     7.4 |  0.505 % |
c |     11334 |  891244  3233771 |  770761   11322    84351     7.5 |  0.507 % |
c |     17100 |  890843  3232294 |  847837   17052   136746     8.0 |  0.516 % |
c |     25751 |  890187  3229870 |  932621   25640   212199     8.3 |  0.537 % |
c |     38726 |  890021  3229272 | 1025883   38596   350458     9.1 |  0.543 % |
c |     58188 |  889784  3228417 | 1128472   58030   581949    10.0 |  0.551 % |
c |     87381 |  888966  3225439 | 1241319   87163   972798    11.2 |  0.577 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5165 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 1.07 1.00 0.95 2/54 5161
Raw data (stat): 5161 (runsolver) R 5160 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842005451 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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 s]
Raw data (loadavg): 1.06 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9998 s]
Raw data (loadavg): 1.05 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0006 s]
Raw data (loadavg): 1.04 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0013 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0011 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0009 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0007 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0005 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0003 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.001 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.001 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.005 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.005 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.005 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.01 s]
Raw data (loadavg): 1.08 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.01 s]
Raw data (loadavg): 1.07 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.01 s]
Raw data (loadavg): 1.06 1.01 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.01 s]
Raw data (loadavg): 1.13 1.03 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.01 s]
Raw data (loadavg): 1.11 1.03 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.01 s]
Raw data (loadavg): 1.09 1.03 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.01 s]
Raw data (loadavg): 1.08 1.03 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.01 s]
Raw data (loadavg): 1.06 1.03 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.01 s]
Raw data (loadavg): 1.05 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.01 s]
Raw data (loadavg): 1.04 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.01 s]
Raw data (loadavg): 1.04 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.01 s]
Raw data (loadavg): 1.03 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.01 s]
Raw data (loadavg): 1.03 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.01 s]
Raw data (loadavg): 1.02 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.01 s]
Raw data (loadavg): 1.02 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.01 s]
Raw data (loadavg): 1.01 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.01 s]
Raw data (loadavg): 1.01 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.01 s]
Raw data (loadavg): 1.01 1.02 0.96 2/55 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 1.09 1.03 0.97 1/53 5165
Raw data (stat): 5161 (minisat+_script) S 5160 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842005451 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.89
CPU user time (s): 1228.11
CPU system time (s): 1.78373
CPU usage (%): 100.016
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####