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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen2.opb
MD5SUM	30256c883dd8af773c334a2b26410bd9
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	9400
Biggest coefficient in the objective function	2494038016
Number of bits for the biggest coefficient in the objective function	32
Sum of the numbers in the objective function	391862963250
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	2494038016
Number of bits of the biggest number in a constraint	32
Biggest sum of numbers in a constraint	391862963250
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.092985
Number of variables	10680
Total number of constraints	444
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	40
Maximum length of a constraint	1700
Trace number 31026

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-25 21:23:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22391 boxname=wulflinc12 idbench=1207 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  30256c883dd8af773c334a2b26410bd9  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-degen2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-degen2.opb
IDLAUNCH: 22391
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        614304 kB
Buffers:         34112 kB
Cached:         364492 kB
SwapCached:        488 kB
Active:          17408 kB
Inactive:       383572 kB
HighTotal:      131008 kB
HighFree:        65408 kB
LowTotal:       903652 kB
LowFree:        548896 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13664 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:44:26 (client local time) WITH STATUS 152 IN 1229.91 SECONDS
stats: 22391 7 1229.91 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 665 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[ 667]---> Adder-cost: 1514   maxlim: 182446   bits: 18/18
c ---[ 666]---> Adder-cost: 1514   maxlim: 103596   bits: 17/17
c ---[ 665]---> Adder-cost: 1168   maxlim: 90177   bits: 17/17
c ---[ 663]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 659]---> Adder-cost: 256   maxlim: 2167   bits: 13/12
c ---[ 657]---> Adder-cost: 256   maxlim: 2295   bits: 13/12
c ---[ 655]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 647]---> Adder-cost: 496   maxlim: 4335   bits: 13/13
c ---[ 645]---> Adder-cost: 528   maxlim: 4335   bits: 14/13
c ---[ 643]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 639]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 637]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 635]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 631]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 629]---> Adder-cost: 336   maxlim: 2805   bits: 13/12
c ---[ 627]---> BDD-cost:   22
c ---[ 625]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 623]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 621]---> Adder-cost: 632   maxlim: 5228   bits: 14/13
c ---[ 619]---> Adder-cost: 600   maxlim: 4845   bits: 14/13
c ---[ 617]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 832   maxlim: 6375   bits: 14/13
c ---[ 607]---> Adder-cost: 848   maxlim: 6758   bits: 14/13
c ---[ 605]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 585]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[ 583]---> Adder-cost: 224   maxlim: 2040   bits: 12/11
c ---[ 581]---> Adder-cost: 464   maxlim: 3825   bits: 13/12
c ---[ 579]---> Adder-cost: 480   maxlim: 4080   bits: 13/12
c ---[ 577]---> BDD-cost:   64
c ---[ 576]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[ 571]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 570]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 568]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> BDD-cost:   67
c ---[ 564]---> BDD-cost:   67
c ---[ 563]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 7
c ---[ 561]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 1652     Base: 2 2 2 2 2 2 2 7
c ---[ 559]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 7
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   67
c ---[ 556]---> BDD-cost:   67
c ---[ 555]---> BDD-cost:   68
c ---[ 554]---> BDD-cost:   67
c ---[ 553]---> BDD-cost:   67
c ---[ 552]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost:  854     Base: 2 2 2 2 2 2 2 7
c ---[ 546]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 544]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 543]---> Adder-cost: 167   maxlim: 1529   bits: 12/11
c ---[ 542]---> Sorter-cost: 1815     Base: 2 2 2 2 2 2 2 7
c ---[ 541]---> Sorter-cost: 1815     Base: 2 2 2 2 2 2 2 7
c ---[ 540]---> Adder-cost: 217   maxlim: 2039   bits: 12/11
c ---[ 539]---> Adder-cost: 230   maxlim: 1911   bits: 12/11
c ---[ 538]---> Adder-cost: 230   maxlim: 2039   bits: 12/11
c ---[ 537]---> Adder-cost: 217   maxlim: 2294   bits: 13/12
c ---[ 536]---> Adder-cost: 224   maxlim: 2166   bits: 13/12
c ---[ 535]---> Adder-cost: 240   maxlim: 2294   bits: 13/12
c ---[ 534]---> Adder-cost: 262   maxlim: 3059   bits: 13/12
c ---[ 533]---> Adder-cost: 295   maxlim: 2931   bits: 13/12
c ---[ 532]---> Adder-cost: 311   maxlim: 3059   bits: 13/12
c ---[ 531]---> Adder-cost: 346   maxlim: 3314   bits: 13/12
c ---[ 530]---> Adder-cost: 361   maxlim: 3186   bits: 13/12
c ---[ 529]---> Adder-cost: 361   maxlim: 3314   bits: 13/12
c ---[ 528]---> Adder-cost: 346   maxlim: 3569   bits: 13/12
c ---[ 527]---> Adder-cost: 377   maxlim: 3441   bits: 13/12
c ---[ 526]---> Adder-cost: 393   maxlim: 3569   bits: 13/12
c ---[ 525]---> Adder-cost: 304   maxlim: 3824   bits: 13/12
c ---[ 524]---> Adder-cost: 323   maxlim: 3696   bits: 13/12
c ---[ 523]---> Adder-cost: 405   maxlim: 3824   bits: 13/12
c ---[ 522]---> BDD-cost:   68
c ---[ 521]---> BDD-cost:   67
c ---[ 520]---> BDD-cost:   67
c ---[ 519]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 513]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 511]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 7
c ---[ 509]---> BDD-cost:   67
c ---[ 508]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 167   maxlim: 1784   bits: 12/11
c ---[ 506]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 2 7
c ---[ 505]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 504]---> Adder-cost: 199   maxlim: 2294   bits: 13/12
c ---[ 503]---> Adder-cost: 214   maxlim: 2294   bits: 13/12
c ---[ 502]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 7
c ---[ 501]---> Adder-cost: 225   maxlim: 2549   bits: 13/12
c ---[ 500]---> Adder-cost: 240   maxlim: 2549   bits: 13/12
c ---[ 499]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> BDD-cost:   68
c ---[ 496]---> BDD-cost:   67
c ---[ 495]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1359     Base: 2 2 2 2 2 2 2 7
c ---[ 493]---> Adder-cost: 185   maxlim: 1274   bits: 12/11
c ---[ 492]---> Adder-cost: 196   maxlim: 1274   bits: 12/11
c ---[ 491]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> BDD-cost:   68
c ---[ 489]---> BDD-cost:   67
c ---[ 488]---> BDD-cost:   67
c ---[ 487]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  456     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 481]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 479]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 478]---> Adder-cost: 135   maxlim: 1274   bits: 12/11
c ---[ 477]---> Sorter-cost: 1720     Base: 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1720     Base: 2 2 2 2 2 2 2 7
c ---[ 475]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 7
c ---[ 471]---> Adder-cost: 149   maxlim: 764   bits: 11/10
c ---[ 470]---> BDD-cost:   67
c ---[ 469]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Adder-cost: 249   maxlim: 1784   bits: 12/11
c ---[ 467]---> Adder-cost: 230   maxlim: 1657   bits: 12/11
c ---[ 466]---> Adder-cost: 210   maxlim: 2039   bits: 12/11
c ---[ 465]---> Adder-cost: 206   maxlim: 1912   bits: 12/11
c ---[ 464]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 463]---> Adder-cost: 297   maxlim: 2167   bits: 13/12
c ---[ 462]---> Adder-cost: 294   maxlim: 2422   bits: 13/12
c ---[ 461]---> Adder-cost: 286   maxlim: 2677   bits: 13/12
c ---[ 460]---> Adder-cost: 269   maxlim: 2422   bits: 13/12
c ---[ 459]---> Sorter-cost: 1587     Base: 2 2 2 2 2 2 2 7
c ---[ 458]---> Adder-cost: 426   maxlim: 2804   bits: 13/12
c ---[ 457]---> Adder-cost: 456   maxlim: 3186   bits: 13/12
c ---[ 456]---> Adder-cost: 439   maxlim: 3059   bits: 13/12
c ---[ 455]---> BDD-cost:   66
c ---[ 454]---> BDD-cost:   65
c ---[ 453]---> BDD-cost:   67
c ---[ 452]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> BDD-cost:   68
c ---[ 446]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 442]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:  475     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 438]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 7
c ---[ 437]---> Adder-cost: 185   maxlim: 1912   bits: 12/11
c ---[ 436]---> Adder-cost: 200   maxlim: 2167   bits: 13/12
c ---[ 435]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 434]---> Adder-cost: 266   maxlim: 2677   bits: 13/12
c ---[ 433]---> Adder-cost: 279   maxlim: 2932   bits: 13/12
c ---[ 432]---> Adder-cost: 256   maxlim: 2677   bits: 13/12
c ---[ 431]---> Adder-cost: 314   maxlim: 2932   bits: 13/12
c ---[ 430]---> Adder-cost: 309   maxlim: 3187   bits: 13/12
c ---[ 429]---> Adder-cost: 222   maxlim: 3187   bits: 13/12
c ---[ 428]---> Adder-cost: 296   maxlim: 3569   bits: 13/12
c ---[ 427]---> Adder-cost: 339   maxlim: 3952   bits: 13/12
c ---[ 426]---> Adder-cost: 287   maxlim: 3442   bits: 13/12
c ---[ 425]---> Adder-cost: 258   maxlim: 3442   bits: 13/12
c ---[ 424]---> Adder-cost: 422   maxlim: 4079   bits: 13/12
c ---[ 423]---> Adder-cost: 442   maxlim: 4462   bits: 14/13
c ---[ 422]---> Adder-cost: 391   maxlim: 3952   bits: 13/12
c ---[ 421]---> Adder-cost: 421   maxlim: 4844   bits: 14/13
c ---[ 420]---> Adder-cost: 420   maxlim: 5227   bits: 14/13
c ---[ 419]---> Adder-cost: 490   maxlim: 4462   bits: 14/13
c ---[ 418]---> Adder-cost: 493   maxlim: 5609   bits: 14/13
c ---[ 417]---> Adder-cost: 470   maxlim: 5992   bits: 14/13
c ---[ 416]---> Adder-cost: 496   maxlim: 5227   bits: 14/13
c ---[ 415]---> Adder-cost: 553   maxlim: 5864   bits: 14/13
c ---[ 414]---> Adder-cost: 562   maxlim: 6247   bits: 14/13
c ---[ 413]---> Adder-cost: 610   maxlim: 5482   bits: 14/13
c ---[ 412]---> Adder-cost: 597   maxlim: 6119   bits: 14/13
c ---[ 411]---> Adder-cost: 598   maxlim: 6502   bits: 14/13
c ---[ 410]---> Adder-cost: 564   maxlim: 5737   bits: 14/13
c ---[ 409]---> BDD-cost:   27
c ---[ 408]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> BDD-cost:   67
c ---[ 406]---> BDD-cost:   67
c ---[ 405]---> BDD-cost:   68
c ---[ 404]---> BDD-cost:   67
c ---[ 403]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 7
c ---[ 399]---> BDD-cost:   68
c ---[ 398]---> BDD-cost:   67
c ---[ 397]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> BDD-cost:   67
c ---[ 394]---> BDD-cost:   66
c ---[ 393]---> BDD-cost:   65
c ---[ 392]---> BDD-cost:   67
c ---[ 391]---> BDD-cost:   66
c ---[ 390]---> BDD-cost:   65
c ---[ 389]---> BDD-cost:   67
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> BDD-cost:   68
c ---[ 383]---> BDD-cost:   67
c ---[ 382]---> BDD-cost:   67
c ---[ 381]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 7
c ---[ 377]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 7
c ---[ 376]---> BDD-cost:   67
c ---[ 374]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Adder-cost: 167   maxlim: 1275   bits: 12/11
c ---[ 370]---> Adder-cost: 184   maxlim: 1274   bits: 12/11
c ---[ 369]---> Adder-cost: 185   maxlim: 1785   bits: 12/11
c ---[ 368]---> Adder-cost: 182   maxlim: 1784   bits: 12/11
c ---[ 367]---> Adder-cost: 233   maxlim: 2040   bits: 12/11
c ---[ 366]---> Adder-cost: 240   maxlim: 2039   bits: 12/11
c ---[ 365]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 7
c ---[ 364]---> Adder-cost: 228   maxlim: 2295   bits: 13/12
c ---[ 363]---> Adder-cost: 245   maxlim: 2294   bits: 13/12
c ---[ 362]---> Adder-cost: 410   maxlim: 2294   bits: 13/12
c ---[ 361]---> Adder-cost: 409   maxlim: 2549   bits: 13/12
c ---[ 360]---> Adder-cost: 304   maxlim: 2549   bits: 13/12
c ---[ 359]---> Adder-cost: 335   maxlim: 2804   bits: 13/12
c ---[ 358]---> BDD-cost:   65
c ---[ 357]---> BDD-cost:   67
c ---[ 355]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   35
c ---[ 351]---> BDD-cost:   35
c ---[ 349]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   35
c ---[ 343]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   35
c ---[ 333]---> BDD-cost:   35
c ---[ 331]---> BDD-cost:   35
c ---[ 329]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 323]---> BDD-cost:   35
c ---[ 321]---> BDD-cost:   35
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   35
c ---[ 313]---> BDD-cost:   35
c ---[ 311]---> BDD-cost:   35
c ---[ 309]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   35
c ---[ 305]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   35
c ---[ 295]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   35
c ---[ 287]---> BDD-cost:   35
c ---[ 285]---> BDD-cost:   35
c ---[ 283]---> BDD-cost:   35
c ---[ 281]---> BDD-cost:   35
c ---[ 279]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   35
c ---[ 275]---> BDD-cost:   35
c ---[ 273]---> BDD-cost:   35
c ---[ 271]---> BDD-cost:   35
c ---[ 269]---> BDD-cost:   35
c ---[ 267]---> BDD-cost:   35
c ---[ 265]---> BDD-cost:   35
c ---[ 263]---> BDD-cost:   35
c ---[ 261]---> BDD-cost:   35
c ---[ 259]---> BDD-cost:   35
c ---[ 257]---> BDD-cost:   35
c ---[ 255]---> BDD-cost:   35
c ---[ 253]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   35
c ---[ 243]---> BDD-cost:   35
c ---[ 241]---> BDD-cost:   35
c ---[ 239]---> BDD-cost:   35
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   35
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 143]---> BDD-cost:   76
c ---[ 141]---> BDD-cost:   76
c ---[ 139]---> BDD-cost:   76
c ---[ 137]---> BDD-cost:   76
c ---[ 135]---> BDD-cost:   76
c ---[ 133]---> BDD-cost:   76
c ---[ 131]---> BDD-cost:   76
c ---[ 129]---> BDD-cost:   76
c ---[ 127]---> BDD-cost:   76
c ---[ 125]---> BDD-cost:   76
c ---[ 123]---> BDD-cost:   76
c ---[ 121]---> BDD-cost:   76
c ---[ 119]---> BDD-cost:   76
c ---[ 117]---> BDD-cost:   76
c ---[ 115]---> BDD-cost:   76
c ---[ 113]---> BDD-cost:   76
c ---[ 111]---> BDD-cost:   35
c ---[ 109]---> BDD-cost:   76
c ---[ 107]---> BDD-cost:   76
c ---[ 105]---> BDD-cost:   76
c ---[ 103]---> BDD-cost:   76
c ---[ 101]---> BDD-cost:   76
c ---[  99]---> BDD-cost:   76
c ---[  97]---> BDD-cost:   76
c ---[  95]---> BDD-cost:   76
c ---[  93]---> BDD-cost:   76
c ---[  91]---> BDD-cost:   76
c ---[  89]---> BDD-cost:   76
c ---[  87]---> BDD-cost:   76
c ---[  85]---> BDD-cost:   76
c ---[  83]---> BDD-cost:   76
c ---[  81]---> BDD-cost:   76
c ---[  79]---> BDD-cost:   76
c ---[  77]---> BDD-cost:   76
c ---[  75]---> BDD-cost:   76
c ---[  73]---> BDD-cost:   76
c ---[  71]---> BDD-cost:   76
c ---[  69]---> BDD-cost:   76
c ---[  67]---> BDD-cost:   76
c ---[  65]---> BDD-cost:   76
c ---[  63]---> BDD-cost:   76
c ---[  61]---> BDD-cost:   76
c ---[  59]---> BDD-cost:   76
c ---[  57]---> BDD-cost:   76
c ---[  55]---> BDD-cost:   76
c ---[  53]---> BDD-cost:   76
c ---[  51]---> BDD-cost:   76
c ---[  49]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  41]---> BDD-cost:   76
c ---[  39]---> BDD-cost:   76
c ---[  37]---> BDD-cost:   76
c ---[  35]---> BDD-cost:   76
c ---[  33]---> BDD-cost:   76
c ---[  31]---> BDD-cost:   35
c ---[  29]---> BDD-cost:   35
c ---[  27]---> BDD-cost:   76
c ---[  25]---> BDD-cost:   76
c ---[  23]---> BDD-cost:   76
c ---[  21]---> BDD-cost:   76
c ---[  19]---> BDD-cost:   76
c ---[  17]---> BDD-cost:   76
c ---[  15]---> BDD-cost:   76
c ---[  13]---> BDD-cost:   76
c ---[  11]---> BDD-cost:   76
c ---[   9]---> BDD-cost:   76
c ---[   7]---> BDD-cost:   76
c ---[   5]---> BDD-cost:   76
c ---[   3]---> BDD-cost:   76
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  517734  1531647 |  172578       0        0     nan |  0.000 % |
c |       100 |  517717  1531609 |  189835      99      453     4.6 |  5.871 % |
c |       250 |  517717  1531609 |  208819     249     1150     4.6 |  5.871 % |
c |       476 |  517679  1531525 |  229701     463     2089     4.5 |  5.879 % |
c |       813 |  517675  1531517 |  252671     798     4142     5.2 |  5.881 % |
c |      1319 |  517561  1531264 |  277938    1289     7041     5.5 |  5.903 % |
c |      2078 |  517493  1531112 |  305732    2040    10468     5.1 |  5.915 % |
c |      3217 |  517318  1530722 |  336305    3153    16763     5.3 |  5.949 % |
c |      4925 |  517256  1530584 |  369936    4855    26338     5.4 |  5.962 % |
c |      7487 |  517100  1530237 |  406929    7399    44864     6.1 |  5.992 % |
c |     11331 |  516686  1529314 |  447622   11187    68385     6.1 |  6.072 % |
c |     17097 |  516269  1528373 |  492385   16897   109055     6.5 |  6.153 % |
c |     25746 |  516084  1527923 |  541623   25523   328866    12.9 |  6.186 % |
c |     38720 |  515683  1526983 |  595786   38439   440277    11.5 |  6.260 % |
c |     58181 |  515503  1526540 |  655364   57867  1081332    18.7 |  6.291 % |
c |     87374 |  515359  1526115 |  720901   87039  2438431    28.0 |  6.314 % |
c |    131163 |  515177  1525635 |  792991  130797  3879866    29.7 |  6.345 % |
c |    196847 |  514859  1524856 |  872290  196429  7837911    39.9 |  6.401 % |
c |    295373 |  514520  1523952 |  959519  294904 11429805    38.8 |  6.460 % |
c |    443163 |  514380  1523577 | 1055471  442666 19716307    44.5 |  6.480 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 16791 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.91 0.95 0.90 2/54 16787
Raw data (stat): 16787 (runsolver) R 16786 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783865746 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.0028 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.0046 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.048 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.05 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.17 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.169 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.178 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.178 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.178 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.178 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.179 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.179 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.18 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.18 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.18 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.18 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.181 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.181 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.182 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.182 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.182 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.184 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.184 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.18 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.78 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 16791
Raw data (stat): 16787 (minisat+_script) S 16786 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783865746 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.78
CPU time (s): 1229.91
CPU user time (s): 1228.45
CPU system time (s): 1.45678
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####