PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-set1ch.opb
MD5SUM	154c7c542b6df7aab333fa859438b34f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	65634210
Optimality of the best value was proved	NO
Number of terms in the objective function	4880
Biggest coefficient in the objective function	10485760
Number of bits for the biggest coefficient in the objective function	24
Sum of the numbers in the objective function	1662757407
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	10485760
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	1662757407
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1252.14
Number of variables	9680
Total number of constraints	732
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	240
Number of constraints which are nor clauses,nor cardinality constraints	492
Minimum length of a constraint	1
Maximum length of a constraint	420
Trace number 31171

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-05-25 22:42:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22569 boxname=wulflinc13 idbench=1385 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  154c7c542b6df7aab333fa859438b34f  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-set1ch.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-set1ch.opb
IDLAUNCH: 22569
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        903852 kB
Buffers:         19068 kB
Cached:          91564 kB
SwapCached:        412 kB
Active:          17820 kB
Inactive:        95108 kB
HighTotal:      131008 kB
HighFree:       105280 kB
LowTotal:       903652 kB
LowFree:        798572 kB
SwapTotal:     2097136 kB
SwapFree:      2096060 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5948 kB
Slab:            12312 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:03:03 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22569 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 732 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): s
c ---[ 731]---> BDD-cost:   43
c ---[ 729]---> BDD-cost:   49
c ---[ 727]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 725]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 723]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 721]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 719]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 717]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 715]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 713]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 711]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 709]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 707]---> BDD-cost:   61
c ---[ 705]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 703]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 701]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 699]---> BDD-cost:  158
c ---[ 697]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 695]---> BDD-cost:  158
c ---[ 693]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 691]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 689]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 685]---> BDD-cost:   46
c ---[ 683]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 681]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 679]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 677]---> Sorter-cost:  352     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 675]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 673]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 669]---> BDD-cost:  147
c ---[ 667]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 663]---> BDD-cost:   46
c ---[ 661]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 657]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> BDD-cost:   46
c ---[ 639]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 621]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 619]---> BDD-cost:   46
c ---[ 617]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 605]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> BDD-cost:   61
c ---[ 595]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 583]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 579]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 577]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> BDD-cost:   66
c ---[ 573]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 567]---> BDD-cost:  141
c ---[ 565]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> BDD-cost:   57
c ---[ 551]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> BDD-cost:  123
c ---[ 543]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 541]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> BDD-cost:  119
c ---[ 535]---> BDD-cost:  132
c ---[ 533]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> BDD-cost:   49
c ---[ 529]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 527]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> BDD-cost:  129
c ---[ 523]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 521]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 519]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> BDD-cost:  124
c ---[ 513]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> BDD-cost:   49
c ---[ 507]---> BDD-cost:   49
c ---[ 505]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> BDD-cost:  125
c ---[ 501]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> BDD-cost:  118
c ---[ 497]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> BDD-cost:  118
c ---[ 489]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> BDD-cost:  118
c ---[ 485]---> BDD-cost:  132
c ---[ 483]---> BDD-cost:  130
c ---[ 481]---> BDD-cost:  117
c ---[ 479]---> BDD-cost:  125
c ---[ 477]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> BDD-cost:  115
c ---[ 471]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> BDD-cost:  124
c ---[ 465]---> Sorter-cost:  325     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> BDD-cost:  124
c ---[ 459]---> BDD-cost:   60
c ---[ 457]---> BDD-cost:   60
c ---[ 455]---> BDD-cost:   55
c ---[ 453]---> BDD-cost:   60
c ---[ 451]---> BDD-cost:   65
c ---[ 449]---> BDD-cost:   65
c ---[ 447]---> BDD-cost:   55
c ---[ 445]---> BDD-cost:   60
c ---[ 443]---> BDD-cost:   60
c ---[ 441]---> BDD-cost:  132
c ---[ 439]---> BDD-cost:   65
c ---[ 437]---> BDD-cost:   55
c ---[ 435]---> BDD-cost:   55
c ---[ 433]---> BDD-cost:   60
c ---[ 431]---> BDD-cost:   60
c ---[ 429]---> BDD-cost:   60
c ---[ 427]---> BDD-cost:   60
c ---[ 425]---> BDD-cost:   60
c ---[ 423]---> BDD-cost:   60
c ---[ 421]---> BDD-cost:   60
c ---[ 419]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> BDD-cost:   65
c ---[ 416]---> Adder-cost: 658   maxlim: 1784683   bits: 22/21
c ---[ 415]---> Adder-cost: 658   maxlim: 1784683   bits: 22/21
c ---[ 414]---> Adder-cost: 650   maxlim: 1391467   bits: 22/21
c ---[ 413]---> Adder-cost: 648   maxlim: 1358699   bits: 22/21
c ---[ 412]---> Adder-cost: 644   maxlim: 1293163   bits: 22/21
c ---[ 411]---> Adder-cost: 636   maxlim: 1162091   bits: 22/21
c ---[ 410]---> Adder-cost: 633   maxlim: 916331   bits: 21/20
c ---[ 409]---> Adder-cost: 610   maxlim: 637803   bits: 21/20
c ---[ 408]---> Adder-cost: 608   maxlim: 605035   bits: 21/20
c ---[ 406]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Adder-cost: 594   maxlim: 383851   bits: 20/19
c ---[ 404]---> Adder-cost: 569   maxlim: 228203   bits: 19/18
c ---[ 402]---> BDD-cost:   23
c ---[ 401]---> BDD-cost:   27
c ---[ 400]---> BDD-cost:   22
c ---[ 399]---> BDD-cost:   25
c ---[ 398]---> BDD-cost:   29
c ---[ 397]---> BDD-cost:   29
c ---[ 396]---> BDD-cost:   22
c ---[ 394]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> BDD-cost:   25
c ---[ 392]---> BDD-cost:   24
c ---[ 391]---> BDD-cost:   27
c ---[ 390]---> BDD-cost:   22
c ---[ 389]---> BDD-cost:   24
c ---[ 388]---> BDD-cost:   24
c ---[ 387]---> BDD-cost:   24
c ---[ 386]---> BDD-cost:   25
c ---[ 385]---> BDD-cost:   25
c ---[ 384]---> BDD-cost:   27
c ---[ 382]---> BDD-cost:  132
c ---[ 381]---> BDD-cost:   25
c ---[ 380]---> BDD-cost:   25
c ---[ 379]---> BDD-cost:   27
c ---[ 378]---> BDD-cost:   23
c ---[ 377]---> BDD-cost:   27
c ---[ 376]---> BDD-cost:   22
c ---[ 375]---> BDD-cost:   23
c ---[ 374]---> BDD-cost:   29
c ---[ 373]---> BDD-cost:   29
c ---[ 372]---> BDD-cost:   22
c ---[ 370]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> BDD-cost:   25
c ---[ 368]---> BDD-cost:   24
c ---[ 367]---> BDD-cost:   27
c ---[ 366]---> BDD-cost:   25
c ---[ 365]---> BDD-cost:   24
c ---[ 364]---> BDD-cost:   24
c ---[ 363]---> BDD-cost:   24
c ---[ 362]---> BDD-cost:   25
c ---[ 361]---> BDD-cost:   24
c ---[ 360]---> BDD-cost:   26
c ---[ 358]---> BDD-cost:  141
c ---[ 357]---> BDD-cost:   25
c ---[ 356]---> BDD-cost:   25
c ---[ 355]---> BDD-cost:   27
c ---[ 354]---> BDD-cost:   23
c ---[ 353]---> BDD-cost:   21
c ---[ 352]---> BDD-cost:   22
c ---[ 351]---> BDD-cost:   22
c ---[ 350]---> BDD-cost:   27
c ---[ 349]---> BDD-cost:   27
c ---[ 348]---> BDD-cost:   22
c ---[ 346]---> BDD-cost:   43
c ---[ 344]---> BDD-cost:  150
c ---[ 343]---> BDD-cost:   22
c ---[ 342]---> BDD-cost:   24
c ---[ 341]---> BDD-cost:   27
c ---[ 340]---> BDD-cost:   23
c ---[ 339]---> BDD-cost:   24
c ---[ 338]---> BDD-cost:   24
c ---[ 337]---> BDD-cost:   24
c ---[ 336]---> BDD-cost:   25
c ---[ 335]---> BDD-cost:   25
c ---[ 334]---> BDD-cost:   24
c ---[ 332]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> BDD-cost:   25
c ---[ 330]---> BDD-cost:   25
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   23
c ---[ 327]---> BDD-cost:   24
c ---[ 326]---> BDD-cost:   22
c ---[ 325]---> BDD-cost:   25
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   23
c ---[ 322]---> BDD-cost:   22
c ---[ 320]---> BDD-cost:  141
c ---[ 319]---> BDD-cost:   24
c ---[ 318]---> BDD-cost:   24
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   23
c ---[ 315]---> BDD-cost:   21
c ---[ 314]---> BDD-cost:   25
c ---[ 313]---> BDD-cost:   24
c ---[ 312]---> BDD-cost:   25
c ---[ 311]---> BDD-cost:   21
c ---[ 310]---> BDD-cost:   25
c ---[ 308]---> BDD-cost:  141
c ---[ 307]---> BDD-cost:   25
c ---[ 306]---> BDD-cost:   27
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   23
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:   23
c ---[ 300]---> BDD-cost:   27
c ---[ 299]---> BDD-cost:   24
c ---[ 298]---> BDD-cost:   22
c ---[ 296]---> BDD-cost:  141
c ---[ 295]---> BDD-cost:   22
c ---[ 294]---> BDD-cost:   24
c ---[ 293]---> BDD-cost:   22
c ---[ 292]---> BDD-cost:   21
c ---[ 291]---> BDD-cost:   23
c ---[ 290]---> BDD-cost:   23
c ---[ 289]---> BDD-cost:   25
c ---[ 288]---> BDD-cost:   25
c ---[ 287]---> BDD-cost:   20
c ---[ 286]---> BDD-cost:   24
c ---[ 284]---> BDD-cost:  141
c ---[ 283]---> BDD-cost:   20
c ---[ 282]---> BDD-cost:   27
c ---[ 281]---> BDD-cost:   27
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:   25
c ---[ 276]---> BDD-cost:   27
c ---[ 275]---> BDD-cost:   26
c ---[ 274]---> BDD-cost:   22
c ---[ 272]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 271]---> BDD-cost:   25
c ---[ 270]---> BDD-cost:   25
c ---[ 269]---> BDD-cost:   27
c ---[ 268]---> BDD-cost:   22
c ---[ 267]---> BDD-cost:   22
c ---[ 266]---> BDD-cost:   21
c ---[ 265]---> BDD-cost:   23
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   23
c ---[ 262]---> BDD-cost:   24
c ---[ 260]---> BDD-cost:  158
c ---[ 259]---> BDD-cost:   21
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   27
c ---[ 256]---> BDD-cost:   23
c ---[ 255]---> BDD-cost:   21
c ---[ 254]---> BDD-cost:   19
c ---[ 253]---> BDD-cost:   25
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   24
c ---[ 250]---> BDD-cost:   16
c ---[ 248]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> BDD-cost:   24
c ---[ 246]---> BDD-cost:   25
c ---[ 245]---> BDD-cost:   25
c ---[ 244]---> BDD-cost:   23
c ---[ 243]---> BDD-cost:   23
c ---[ 242]---> BDD-cost:   21
c ---[ 241]---> BDD-cost:   21
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   23
c ---[ 238]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:  150
c ---[ 235]---> BDD-cost:   22
c ---[ 234]---> BDD-cost:   25
c ---[ 233]---> BDD-cost:   22
c ---[ 232]---> BDD-cost:   22
c ---[ 231]---> BDD-cost:   22
c ---[ 230]---> BDD-cost:   16
c ---[ 229]---> BDD-cost:   21
c ---[ 228]---> BDD-cost:   24
c ---[ 227]---> BDD-cost:   24
c ---[ 226]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   61
c ---[ 222]---> BDD-cost:  150
c ---[ 221]---> BDD-cost:   22
c ---[ 220]---> BDD-cost:   20
c ---[ 219]---> BDD-cost:   24
c ---[ 218]---> BDD-cost:   23
c ---[ 217]---> BDD-cost:   22
c ---[ 216]---> BDD-cost:   22
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:   22
c ---[ 212]---> BDD-cost:   20
c ---[ 210]---> BDD-cost:  137
c ---[ 209]---> BDD-cost:   22
c ---[ 208]---> BDD-cost:   25
c ---[ 207]---> BDD-cost:   24
c ---[ 206]---> BDD-cost:   23
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   19
c ---[ 203]---> BDD-cost:   23
c ---[ 202]---> BDD-cost:   25
c ---[ 201]---> BDD-cost:   23
c ---[ 200]---> BDD-cost:   21
c ---[ 198]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> BDD-cost:   23
c ---[ 196]---> BDD-cost:   22
c ---[ 195]---> BDD-cost:   22
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   20
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   23
c ---[ 188]---> BDD-cost:   23
c ---[ 186]---> BDD-cost:  137
c ---[ 185]---> BDD-cost:   23
c ---[ 184]---> BDD-cost:   24
c ---[ 183]---> BDD-cost:   25
c ---[ 182]---> BDD-cost:   21
c ---[ 181]---> BDD-cost:   18
c ---[ 180]---> BDD-cost:   19
c ---[ 179]---> BDD-cost:   20
c ---[ 178]---> BDD-cost:   24
c ---[ 177]---> BDD-cost:   25
c ---[ 176]---> BDD-cost:   20
c ---[ 174]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   21
c ---[ 172]---> BDD-cost:   22
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   21
c ---[ 168]---> BDD-cost:   21
c ---[ 167]---> BDD-cost:   20
c ---[ 166]---> BDD-cost:   21
c ---[ 165]---> BDD-cost:   21
c ---[ 164]---> BDD-cost:   23
c ---[ 162]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> BDD-cost:   20
c ---[ 160]---> BDD-cost:   23
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   21
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   21
c ---[ 154]---> BDD-cost:   22
c ---[ 153]---> BDD-cost:   21
c ---[ 152]---> BDD-cost:   18
c ---[ 150]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> BDD-cost:   21
c ---[ 148]---> BDD-cost:   21
c ---[ 147]---> BDD-cost:   23
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   21
c ---[ 144]---> BDD-cost:   21
c ---[ 143]---> BDD-cost:   21
c ---[ 142]---> BDD-cost:   21
c ---[ 141]---> BDD-cost:   18
c ---[ 140]---> BDD-cost:   21
c ---[ 138]---> BDD-cost:  137
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   23
c ---[ 134]---> BDD-cost:   18
c ---[ 133]---> BDD-cost:   16
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   17
c ---[ 129]---> BDD-cost:   21
c ---[ 128]---> BDD-cost:   17
c ---[ 126]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   21
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   19
c ---[ 117]---> BDD-cost:   19
c ---[ 116]---> BDD-cost:   18
c ---[ 114]---> BDD-cost:  146
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   21
c ---[ 109]---> BDD-cost:   52
c ---[ 107]---> BDD-cost:  155
c ---[ 105]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:  146
c ---[  97]---> BDD-cost:  146
c ---[  95]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> BDD-cost:   52
c ---[  85]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> BDD-cost:  142
c ---[  81]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> BDD-cost:  142
c ---[  77]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  73]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> BDD-cost:  142
c ---[  69]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:   43
c ---[  63]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> BDD-cost:   46
c ---[  41]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> BDD-cost:  147
c ---[  37]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> BDD-cost:  144
c ---[  25]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   46
c ---[  19]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Adder-cost: 542   maxlim: 31595   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  213123   572938 |   71041       0        0     nan |  0.000 % |
c |       100 |  213092   572871 |   78145      93      282     3.0 | 12.471 % |
c |       250 |  212317   571110 |   85959     175      512     2.9 | 12.770 % |
c |       475 |  211215   568625 |   94555     279      782     2.8 | 13.188 % |
c |       812 |  209691   565191 |  104011     435     1224     2.8 | 13.785 % |
c |      1318 |  207628   560569 |  114412     698     2196     3.1 | 14.550 % |
c |      2077 |  204726   553982 |  125853    1161     3629     3.1 | 15.693 % |
c |      3217 |  201059   545651 |  138438    1901     6283     3.3 | 17.171 % |
c |      4925 |  197435   537407 |  152282    3221    11293     3.5 | 18.571 % |
c |      7487 |  194895   531586 |  167510    5488    20505     3.7 | 19.619 % |
c |     11331 |  191383   523570 |  184262    8915    34541     3.9 | 21.091 % |
c |     17097 |  186900   513162 |  202688   14243    65247     4.6 | 22.957 % |
c ==============================================================================
c [1mFound solution: 142981640[0m
c ---[   0]---> Adder-cost: 14654   maxlim: 270876695   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21199 |  288335   876626 |   96111   18225    83576     4.6 | 22.957 % |
c |     21300 |  288335   876626 |  105722   18326    84003     4.6 | 19.646 % |
c |     21450 |  288132   876081 |  116294   18456    84658     4.6 | 19.705 % |
c |     21675 |  288069   875932 |  127923   18675    85737     4.6 | 19.727 % |
c |     22012 |  288069   875932 |  140716   19012    87449     4.6 | 19.727 % |
c |     22519 |  287967   875646 |  154787   19505    90349     4.6 | 19.752 % |
c |     23278 |  287769   875113 |  170266   20249    94751     4.7 | 19.806 % |
c |     24418 |  287744   875054 |  187293   21387   104632     4.9 | 19.815 % |
c ==============================================================================
c [1mFound solution: 142151892[0m
c ---[   0]---> Adder-cost: 6604   maxlim: 268036427   bits: 29/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25840 |  333775  1039682 |  111258   22800   117943     5.2 | 19.815 % |
c |     25940 |  333737  1039563 |  122383   22899   118505     5.2 | 18.535 % |
c |     26090 |  333737  1039563 |  134622   23049   119375     5.2 | 18.535 % |
c |     26315 |  333722  1039530 |  148084   23272   120717     5.2 | 18.540 % |
c |     26653 |  333603  1039202 |  162892   23605   122597     5.2 | 18.571 % |
c |     27159 |  333402  1038617 |  179182   24103   125377     5.2 | 18.613 % |
c |     27918 |  333237  1038152 |  197100   24845   130059     5.2 | 18.652 % |
c |     29057 |  333201  1038071 |  216810   25980   136714     5.3 | 18.663 % |
c |     30765 |  333031  1037590 |  238491   27675   147503     5.3 | 18.704 % |
c |     33327 |  332871  1037160 |  262340   30228   162588     5.4 | 18.750 % |
c |     37171 |  332839  1037088 |  288574   34068   188184     5.5 | 18.759 % |
c |     42937 |  332794  1036982 |  317432   39829   230111     5.8 | 18.773 % |
c |     51586 |  332665  1036659 |  349175   48461   294776     6.1 | 18.812 % |
c |     64560 |  332539  1036366 |  384092   61424   399166     6.5 | 18.849 % |
c |     84021 |  332363  1035948 |  422502   80863   616696     7.6 | 18.908 % |
c |    113213 |  332205  1035564 |  464752  110042   995056     9.0 | 18.960 % |
c |    157002 |  332170  1035481 |  511227  153827  1771857    11.5 | 18.971 % |
c |    222686 |  332024  1035138 |  562350  219492  2799315    12.8 | 19.018 % |
c |    321212 |  331930  1034916 |  618585  318009  5913412    18.6 | 19.049 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 17549 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.93 2/54 17545
Raw data (stat): 17545 (runsolver) R 17544 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784350829 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99992 s]
Raw data (loadavg): 0.93 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0007 s]
Raw data (loadavg): 0.96 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0091 s]
Raw data (loadavg): 0.97 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0133 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0126 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 17549
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 17550
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.07 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 1.06 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 1.05 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.04 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.03 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.03 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.02 0.99 0.94 2/55 17602
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.02 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.02 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 0.99 0.94 1/53 17604
Raw data (stat): 17545 (minisat+_script) S 17544 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784350829 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.71
CPU time (s): 1229.88
CPU user time (s): 1228.96
CPU system time (s): 0.921859
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####