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 20097

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 20:04:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15688 boxname=wulflinc13 idbench=1207 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  30256c883dd8af773c334a2b26410bd9  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb
IDLAUNCH: 15688
/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:        809096 kB
Buffers:         10016 kB
Cached:         193452 kB
SwapCached:        260 kB
Active:          17116 kB
Inactive:       188768 kB
HighTotal:      131008 kB
HighFree:        70196 kB
LowTotal:       903652 kB
LowFree:        738900 kB
SwapTotal:     2097136 kB
SwapFree:      2096448 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13904 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:24:10 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 15688 7 1200.34 0
#### 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]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[ 661]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[ 659]---> Adder-cost: 256   maxlim: 2167   bits: 13/12
c ---[ 657]---> Adder-cost: 256   maxlim: 2295   bits: 13/12
c ---[ 655]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 653]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 651]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[ 649]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[ 647]---> Adder-cost: 496   maxlim: 4335   bits: 13/13
c ---[ 645]---> Adder-cost: 528   maxlim: 4335   bits: 14/13
c ---[ 643]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[ 641]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[ 639]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 637]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 635]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[ 633]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[ 631]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 629]---> Adder-cost: 336   maxlim: 2805   bits: 13/12
c ---[ 627]---> Adder-cost: 16   maxlim: 255   bits: 9/8
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]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 615]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 613]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 611]---> Adder-cost: 80   maxlim: 637   bits: 11/10
c ---[ 609]---> Adder-cost: 832   maxlim: 6375   bits: 14/13
c ---[ 607]---> Adder-cost: 848   maxlim: 6758   bits: 14/13
c ---[ 605]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 603]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 601]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[ 599]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[ 597]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[ 595]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 593]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[ 591]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[ 589]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[ 587]---> Adder-cost: 80   maxlim: 765   bits: 11/10
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]---> Adder-cost: 32   maxlim: 510   bits: 10/9
c ---[ 576]---> Adder-cost: 55   maxlim: 509   bits: 10/9
c ---[ 575]---> Adder-cost: 54   maxlim: 509   bits: 10/9
c ---[ 574]---> Adder-cost: 54   maxlim: 509   bits: 10/9
c ---[ 573]---> Adder-cost: 88   maxlim: 764   bits: 11/10
c ---[ 572]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[ 571]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[ 570]---> Adder-cost: 104   maxlim: 1019   bits: 11/10
c ---[ 569]---> Adder-cost: 103   maxlim: 1019   bits: 11/10
c ---[ 568]---> Adder-cost: 103   maxlim: 1019   bits: 11/10
c ---[ 567]---> Adder-cost: 21   maxlim: 126   bits: 8/7
c ---[ 566]---> Adder-cost: 55   maxlim: 381   bits: 10/9
c ---[ 565]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 564]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 563]---> Adder-cost: 120   maxlim: 891   bits: 11/10
c ---[ 562]---> Adder-cost: 101   maxlim: 764   bits: 11/10
c ---[ 561]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 560]---> Adder-cost: 137   maxlim: 1146   bits: 12/11
c ---[ 559]---> Adder-cost: 113   maxlim: 1019   bits: 11/10
c ---[ 558]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 557]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 556]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 555]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 554]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 553]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 552]---> Adder-cost: 51   maxlim: 509   bits: 10/9
c ---[ 551]---> Adder-cost: 50   maxlim: 509   bits: 10/9
c ---[ 550]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 549]---> Adder-cost: 70   maxlim: 764   bits: 11/10
c ---[ 548]---> Adder-cost: 69   maxlim: 764   bits: 11/10
c ---[ 547]---> Adder-cost: 85   maxlim: 764   bits: 11/10
c ---[ 546]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[ 545]---> Adder-cost: 101   maxlim: 636   bits: 11/10
c ---[ 544]---> Adder-cost: 101   maxlim: 764   bits: 11/10
c ---[ 543]---> Adder-cost: 167   maxlim: 1529   bits: 12/11
c ---[ 542]---> Adder-cost: 166   maxlim: 1401   bits: 12/11
c ---[ 541]---> Adder-cost: 166   maxlim: 1529   bits: 12/11
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]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 521]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 520]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 519]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[ 518]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 517]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 516]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[ 515]---> Adder-cost: 101   maxlim: 764   bits: 11/10
c ---[ 514]---> Adder-cost: 101   maxlim: 764   bits: 11/10
c ---[ 513]---> Adder-cost: 88   maxlim: 1019   bits: 11/10
c ---[ 512]---> Adder-cost: 87   maxlim: 1019   bits: 11/10
c ---[ 511]---> Adder-cost: 104   maxlim: 1274   bits: 12/11
c ---[ 510]---> Adder-cost: 103   maxlim: 1274   bits: 12/11
c ---[ 509]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 508]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 507]---> Adder-cost: 135   maxlim: 1784   bits: 12/11
c ---[ 506]---> Adder-cost: 134   maxlim: 1784   bits: 12/11
c ---[ 505]---> Adder-cost: 87   maxlim: 636   bits: 11/10
c ---[ 504]---> Adder-cost: 199   maxlim: 2294   bits: 13/12
c ---[ 503]---> Adder-cost: 198   maxlim: 2294   bits: 13/12
c ---[ 502]---> Adder-cost: 119   maxlim: 891   bits: 11/10
c ---[ 501]---> Adder-cost: 225   maxlim: 2549   bits: 13/12
c ---[ 500]---> Adder-cost: 224   maxlim: 2549   bits: 13/12
c ---[ 499]---> Adder-cost: 51   maxlim: 509   bits: 10/9
c ---[ 498]---> Adder-cost: 50   maxlim: 509   bits: 10/9
c ---[ 497]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 496]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 495]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[ 494]---> Adder-cost: 129   maxlim: 1019   bits: 11/10
c ---[ 493]---> Adder-cost: 185   maxlim: 1274   bits: 12/11
c ---[ 492]---> Adder-cost: 196   maxlim: 1274   bits: 12/11
c ---[ 491]---> Adder-cost: 52   maxlim: 254   bits: 9/8
c ---[ 490]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 489]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 488]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 487]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[ 486]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 485]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 484]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[ 483]---> Adder-cost: 85   maxlim: 764   bits: 11/10
c ---[ 482]---> Adder-cost: 101   maxlim: 764   bits: 11/10
c ---[ 481]---> Adder-cost: 98   maxlim: 1019   bits: 11/10
c ---[ 480]---> Adder-cost: 97   maxlim: 1019   bits: 11/10
c ---[ 479]---> Adder-cost: 113   maxlim: 1019   bits: 11/10
c ---[ 478]---> Adder-cost: 133   maxlim: 1274   bits: 12/11
c ---[ 477]---> Adder-cost: 132   maxlim: 1274   bits: 12/11
c ---[ 476]---> Adder-cost: 132   maxlim: 1274   bits: 12/11
c ---[ 475]---> Adder-cost: 53   maxlim: 254   bits: 9/8
c ---[ 474]---> Adder-cost: 54   maxlim: 382   bits: 10/9
c ---[ 473]---> Adder-cost: 119   maxlim: 509   bits: 10/9
c ---[ 472]---> Adder-cost: 119   maxlim: 637   bits: 11/10
c ---[ 471]---> Adder-cost: 117   maxlim: 764   bits: 11/10
c ---[ 470]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 469]---> Adder-cost: 66   maxlim: 509   bits: 10/9
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]---> Adder-cost: 101   maxlim: 764   bits: 11/10
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]---> Adder-cost: 134   maxlim: 1019   bits: 11/10
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]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 454]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 453]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 452]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[ 451]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 450]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 449]---> Adder-cost: 20   maxlim: 126   bits: 8/7
c ---[ 448]---> Adder-cost: 54   maxlim: 509   bits: 10/9
c ---[ 447]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 446]---> Adder-cost: 38   maxlim: 381   bits: 10/9
c ---[ 445]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[ 442]---> Adder-cost: 66   maxlim: 254   bits: 9/8
c ---[ 441]---> Adder-cost: 66   maxlim: 382   bits: 10/9
c ---[ 440]---> Adder-cost: 54   maxlim: 382   bits: 10/9
c ---[ 439]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 438]---> Adder-cost: 152   maxlim: 1657   bits: 12/11
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: 546   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]---> Adder-cost: 21   maxlim: 254   bits: 9/8
c ---[ 408]---> Adder-cost: 55   maxlim: 509   bits: 10/9
c ---[ 407]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 406]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 405]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 404]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 403]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[ 402]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 401]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[ 400]---> Adder-cost: 85   maxlim: 764   bits: 11/10
c ---[ 399]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 398]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 397]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[ 396]---> Adder-cost: 50   maxlim: 509   bits: 10/9
c ---[ 395]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 394]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 393]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 392]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 391]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 390]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 389]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 388]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 387]---> Adder-cost: 51   maxlim: 509   bits: 10/9
c ---[ 386]---> Adder-cost: 50   maxlim: 509   bits: 10/9
c ---[ 385]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 384]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[ 383]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 382]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 381]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[ 380]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 379]---> Adder-cost: 120   maxlim: 764   bits: 11/10
c ---[ 378]---> Adder-cost: 119   maxlim: 764   bits: 11/10
c ---[ 377]---> Adder-cost: 85   maxlim: 509   bits: 10/9
c ---[ 376]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 374]---> Adder-cost: 55   maxlim: 510   bits: 10/9
c ---[ 373]---> Adder-cost: 66   maxlim: 509   bits: 10/9
c ---[ 372]---> Adder-cost: 54   maxlim: 509   bits: 10/9
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]---> Adder-cost: 101   maxlim: 1019   bits: 11/10
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]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 357]---> Adder-cost: 35   maxlim: 254   bits: 9/8
c ---[ 355]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 353]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 351]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 349]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 347]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 345]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 343]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 341]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 339]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 337]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 335]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 333]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 331]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 329]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 327]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 325]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 323]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 321]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 319]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 317]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 315]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 313]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 311]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 309]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 307]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 305]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 303]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 301]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 299]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 297]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 295]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 293]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 291]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 289]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 287]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 285]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 283]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 281]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 279]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 277]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 275]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 273]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 271]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 269]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 267]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 265]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 263]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 261]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 259]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 257]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 255]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 253]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 251]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 249]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 247]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 245]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 243]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 241]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 239]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 237]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 235]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 233]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 231]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 229]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 227]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 225]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 223]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 221]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 219]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 217]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 215]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 213]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 211]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 209]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 207]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 205]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 203]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 201]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 199]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 197]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 195]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 193]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 191]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 189]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 187]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 185]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 183]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 181]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 179]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 177]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 175]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 173]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 171]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 169]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 167]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 165]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 163]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 161]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 159]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 157]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 155]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 153]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 151]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 149]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 147]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 145]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 143]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 141]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 139]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 137]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 135]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 133]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 131]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 129]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 127]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 125]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 123]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 121]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 119]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 117]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 115]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 113]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 111]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 109]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 107]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 105]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 103]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 101]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  99]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  97]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  95]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  93]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  91]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  89]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  87]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  85]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  83]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  81]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  79]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  77]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  75]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  73]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  71]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  69]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  67]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  65]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  63]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  61]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  59]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  57]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  55]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  53]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  51]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  49]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  47]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  45]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  43]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  41]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  39]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  37]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  35]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  33]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  31]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  29]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  27]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  25]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  23]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  21]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  19]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  17]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  15]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  13]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  11]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   9]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   7]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   5]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   3]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   2]---> Adder-cost: 15   maxlim: 127   bits: 8/7
c ---[   1]---> Adder-cost: 15   maxlim: 127   bits: 8/7
c ---[   0]---> Adder-cost: 17   maxlim: 255   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  348830  1244954 |  116276       0        0     nan |  0.000 % |
c |       100 |  348830  1244954 |  127903     100      294     2.9 | 18.421 % |
c |       250 |  348830  1244954 |  140693     250      715     2.9 | 18.421 % |
c |       475 |  348830  1244954 |  154763     475     1281     2.7 | 18.421 % |
c |       812 |  348830  1244954 |  170239     812     2287     2.8 | 18.421 % |
c |      1318 |  348830  1244954 |  187263    1318     4158     3.2 | 18.421 % |
c |      2077 |  348830  1244954 |  205990    2077     7060     3.4 | 18.421 % |
c |      3217 |  348830  1244954 |  226589    3217    13592     4.2 | 18.421 % |
c |      4925 |  348830  1244954 |  249247    4925    25220     5.1 | 18.421 % |
c |      7487 |  348822  1244928 |  274172    7486    37633     5.0 | 18.422 % |
c |     11331 |  348814  1244902 |  301589   11329    60768     5.4 | 18.424 % |
c |     17097 |  348690  1244489 |  331748   17082    98106     5.7 | 18.457 % |
c |     25746 |  348588  1244153 |  364923   25713   160842     6.3 | 18.478 % |
c |     38721 |  348512  1243907 |  401416   38673   382977     9.9 | 18.494 % |
c |     58183 |  348498  1243861 |  441557   58131  1722580    29.6 | 18.497 % |
c |     87375 |  348449  1243698 |  485713   87317  2662869    30.5 | 18.508 % |
c |    131165 |  348397  1243514 |  534285  131102  6003077    45.8 | 18.522 % |
c |    196849 |  348265  1243054 |  587713  196770  7830091    39.8 | 18.549 % |
c |    295375 |  348231  1242932 |  646484  295292 15698171    53.2 | 18.557 % |
c |    443167 |  348145  1242654 |  711133  443073 23272270    52.5 | 18.573 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.93 0.90 2/54 26319
Raw data (stat): 26319 (runsolver) R 26318 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489598373 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+10.0005 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 7327 0 0 0 978 21 0 0 25 0 1 0 489598373 36245504 7102 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8849 7102 603 41 0 8808 0
vsize: 35396
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 7464 0 0 0 1977 21 0 0 25 0 1 0 489598373 36921344 7239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9014 7239 603 41 0 8973 0
vsize: 36056
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 7563 0 0 0 2976 22 0 0 25 0 1 0 489598373 37191680 7338 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9080 7338 603 41 0 9039 0
vsize: 36320
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 7667 0 0 0 3976 23 0 0 25 0 1 0 489598373 37732352 7442 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9212 7442 603 41 0 9171 0
vsize: 36848
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 7753 0 0 0 4975 24 0 0 25 0 1 0 489598373 38002688 7528 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9278 7528 603 41 0 9237 0
vsize: 37112
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 7842 0 0 0 5974 25 0 0 25 0 1 0 489598373 38408192 7617 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9377 7617 603 41 0 9336 0
vsize: 37508
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 8186 0 0 0 6973 26 0 0 25 0 1 0 489598373 39882752 7961 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9737 7961 603 41 0 9696 0
vsize: 38948
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 9026 0 0 0 7970 29 0 0 25 0 1 0 489598373 43245568 8801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10558 8801 603 41 0 10517 0
vsize: 42232
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 9652 0 0 0 8967 32 0 0 25 0 1 0 489598373 45817856 9427 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11186 9427 603 41 0 11145 0
vsize: 44744
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 9840 0 0 0 9967 33 0 0 25 0 1 0 489598373 46886912 9615 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11447 9615 603 41 0 11406 0
vsize: 45788
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 10040 0 0 0 10966 34 0 0 25 0 1 0 489598373 47558656 9815 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11611 9815 603 41 0 11570 0
vsize: 46444
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26319
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 10290 0 0 0 11965 35 0 0 25 0 1 0 489598373 48640000 10065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11875 10065 603 41 0 11834 0
vsize: 47500
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 10997 0 0 0 12962 37 0 0 25 0 1 0 489598373 51478528 10772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12568 10772 603 41 0 12527 0
vsize: 50272
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 11288 0 0 0 13961 38 0 0 25 0 1 0 489598373 52690944 11063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12864 11063 603 41 0 12823 0
vsize: 51456
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 11862 0 0 0 14959 40 0 0 25 0 1 0 489598373 54964224 11637 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13419 11637 603 41 0 13378 0
vsize: 53676
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 12384 0 0 0 15957 42 0 0 25 0 1 0 489598373 57126912 12159 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13947 12159 603 41 0 13906 0
vsize: 55788
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 12796 0 0 0 16956 44 0 0 25 0 1 0 489598373 58732544 12571 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14339 12571 603 41 0 14298 0
vsize: 57356
[startup+180.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 13205 0 0 0 17955 45 0 0 25 0 1 0 489598373 60350464 12980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 12980 603 41 0 14693 0
vsize: 58936
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 13566 0 0 0 18954 46 0 0 25 0 1 0 489598373 61825024 13341 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 13341 603 41 0 15053 0
vsize: 60376
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 13918 0 0 0 19953 47 0 0 25 0 1 0 489598373 63307776 13693 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15456 13693 603 41 0 15415 0
vsize: 61824
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 14229 0 0 0 20952 48 0 0 25 0 1 0 489598373 64520192 14004 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15752 14004 603 41 0 15711 0
vsize: 63008
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 14537 0 0 0 21951 49 0 0 25 0 1 0 489598373 65859584 14312 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16079 14312 603 41 0 16038 0
vsize: 64316
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 14815 0 0 0 22950 50 0 0 25 0 1 0 489598373 67473408 14590 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16473 14590 603 41 0 16432 0
vsize: 65892
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 15040 0 0 0 23949 51 0 0 25 0 1 0 489598373 68415488 14815 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16703 14815 603 41 0 16662 0
vsize: 66812
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 15206 0 0 0 24949 52 0 0 25 0 1 0 489598373 69091328 14981 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16868 14981 603 41 0 16827 0
vsize: 67472
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 15322 0 0 0 25949 52 0 0 25 0 1 0 489598373 69496832 15097 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16967 15097 603 41 0 16926 0
vsize: 67868
[startup+270.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 15471 0 0 0 26948 53 0 0 25 0 1 0 489598373 70168576 15246 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17131 15246 603 41 0 17090 0
vsize: 68524
[startup+280.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 15906 0 0 0 27948 53 0 0 25 0 1 0 489598373 71905280 15681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17555 15681 603 41 0 17514 0
vsize: 70220
[startup+290.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 16105 0 0 0 28947 54 0 0 25 0 1 0 489598373 72712192 15880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17752 15880 603 41 0 17711 0
vsize: 71008
[startup+300.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 16407 0 0 0 29946 55 0 0 25 0 1 0 489598373 73924608 16182 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 16182 603 41 0 18007 0
vsize: 72192
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 16526 0 0 0 30946 56 0 0 25 0 1 0 489598373 74330112 16301 4294967295 134512640 134672761 3221224544 3221223760 134557630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18147 16301 603 41 0 18106 0
vsize: 72588
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 16629 0 0 0 31946 56 0 0 25 0 1 0 489598373 74735616 16404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18246 16404 603 41 0 18205 0
vsize: 72984
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 16726 0 0 0 32946 56 0 0 25 0 1 0 489598373 75137024 16501 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18344 16501 603 41 0 18303 0
vsize: 73376
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 16820 0 0 0 33946 56 0 0 25 0 1 0 489598373 75542528 16595 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18443 16595 603 41 0 18402 0
vsize: 73772
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 17056 0 0 0 34945 57 0 0 25 0 1 0 489598373 76484608 16831 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18673 16831 603 41 0 18632 0
vsize: 74692
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 17172 0 0 0 35945 57 0 0 25 0 1 0 489598373 76886016 16947 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18771 16947 603 41 0 18730 0
vsize: 75084
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 17578 0 0 0 36944 59 0 0 25 0 1 0 489598373 78508032 17353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 17353 603 41 0 19126 0
vsize: 76668
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 18052 0 0 0 37942 61 0 0 25 0 1 0 489598373 80523264 17827 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19659 17827 603 41 0 19618 0
vsize: 78636
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 18443 0 0 0 38942 61 0 0 25 0 1 0 489598373 82001920 18218 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20020 18218 603 41 0 19979 0
vsize: 80080
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 18828 0 0 0 39941 63 0 0 25 0 1 0 489598373 83615744 18603 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20414 18603 603 41 0 20373 0
vsize: 81656
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 19224 0 0 0 40940 64 0 0 25 0 1 0 489598373 85233664 18999 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20809 18999 603 41 0 20768 0
vsize: 83236
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 19579 0 0 0 41939 65 0 0 25 0 1 0 489598373 86712320 19354 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21170 19354 603 41 0 21129 0
vsize: 84680
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 19928 0 0 0 42939 66 0 0 25 0 1 0 489598373 88055808 19703 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21498 19703 603 41 0 21457 0
vsize: 85992
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 20296 0 0 0 43939 66 0 0 25 0 1 0 489598373 89542656 20071 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21861 20071 603 41 0 21820 0
vsize: 87444
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 20668 0 0 0 44937 68 0 0 25 0 1 0 489598373 91168768 20443 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22258 20443 603 41 0 22217 0
vsize: 89032
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 21027 0 0 0 45937 69 0 0 25 0 1 0 489598373 92528640 20802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22590 20802 603 41 0 22549 0
vsize: 90360
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 21358 0 0 0 46936 69 0 0 25 0 1 0 489598373 93872128 21133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22918 21133 603 41 0 22877 0
vsize: 91672
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 21754 0 0 0 47935 70 0 0 25 0 1 0 489598373 95547392 21529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23327 21529 603 41 0 23286 0
vsize: 93308
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 22044 0 0 0 48935 71 0 0 25 0 1 0 489598373 96763904 21819 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23624 21820 603 41 0 23583 0
vsize: 94496
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 22356 0 0 0 49934 72 0 0 25 0 1 0 489598373 97980416 22131 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23921 22131 603 41 0 23880 0
vsize: 95684
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 22844 0 0 0 50932 73 0 0 25 0 1 0 489598373 100003840 22619 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24415 22619 603 41 0 24374 0
vsize: 97660
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 23667 0 0 0 51930 76 0 0 25 0 1 0 489598373 104435712 23442 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 23442 603 41 0 25456 0
vsize: 101988
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 24331 0 0 0 52928 78 0 0 25 0 1 0 489598373 107126784 24106 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26154 24106 603 41 0 26113 0
vsize: 104616
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 25158 0 0 0 53925 81 0 0 25 0 1 0 489598373 110493696 24933 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26976 24933 603 41 0 26935 0
vsize: 107904
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 25903 0 0 0 54923 83 0 0 25 0 1 0 489598373 113438720 25678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27695 25678 603 41 0 27654 0
vsize: 110780
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 26346 0 0 0 55922 84 0 0 25 0 1 0 489598373 115322880 26121 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28155 26121 603 41 0 28114 0
vsize: 112620
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 26538 0 0 0 56921 85 0 0 25 0 1 0 489598373 115998720 26313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28320 26313 603 41 0 28279 0
vsize: 113280
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 26716 0 0 0 57920 86 0 0 25 0 1 0 489598373 116801536 26491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28516 26491 603 41 0 28475 0
vsize: 114064
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 26897 0 0 0 58920 87 0 0 25 0 1 0 489598373 117481472 26672 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28682 26672 603 41 0 28641 0
vsize: 114728
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 27096 0 0 0 59919 87 0 0 25 0 1 0 489598373 118292480 26871 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28880 26871 603 41 0 28839 0
vsize: 115520
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 27299 0 0 0 60919 88 0 0 25 0 1 0 489598373 119103488 27074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29078 27074 603 41 0 29037 0
vsize: 116312
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 27506 0 0 0 61918 89 0 0 25 0 1 0 489598373 120041472 27281 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29307 27281 603 41 0 29266 0
vsize: 117228
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 27710 0 0 0 62918 89 0 0 25 0 1 0 489598373 120852480 27485 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29505 27485 603 41 0 29464 0
vsize: 118020
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 27931 0 0 0 63917 90 0 0 25 0 1 0 489598373 121659392 27706 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29702 27706 603 41 0 29661 0
vsize: 118808
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 28170 0 0 0 64916 91 0 0 25 0 1 0 489598373 122732544 27945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29964 27945 603 41 0 29923 0
vsize: 119856
[startup+660.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 28391 0 0 0 65917 92 0 0 25 0 1 0 489598373 123543552 28166 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30162 28166 603 41 0 30121 0
vsize: 120648
[startup+670.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 28583 0 0 0 66917 92 0 0 25 0 1 0 489598373 124358656 28358 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30361 28358 603 41 0 30320 0
vsize: 121444
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 28775 0 0 0 67916 94 0 0 25 0 1 0 489598373 125214720 28550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30570 28550 603 41 0 30529 0
vsize: 122280
[startup+690.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 28878 0 0 0 68916 94 0 0 25 0 1 0 489598373 125620224 28653 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30669 28653 603 41 0 30628 0
vsize: 122676
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29045 0 0 0 69916 95 0 0 25 0 1 0 489598373 126296064 28820 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30834 28820 603 41 0 30793 0
vsize: 123336
[startup+710.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29213 0 0 0 70915 95 0 0 25 0 1 0 489598373 126971904 28988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30999 28988 603 41 0 30958 0
vsize: 123996
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29295 0 0 0 71915 95 0 0 25 0 1 0 489598373 127242240 29070 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31065 29070 603 41 0 31024 0
vsize: 124260
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29430 0 0 0 72915 96 0 0 25 0 1 0 489598373 127787008 29205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31198 29205 603 41 0 31157 0
vsize: 124792
[startup+740.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29540 0 0 0 73915 96 0 0 25 0 1 0 489598373 128192512 29315 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31297 29315 603 41 0 31256 0
vsize: 125188
[startup+750.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29640 0 0 0 74915 97 0 0 25 0 1 0 489598373 128606208 29415 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31398 29415 603 41 0 31357 0
vsize: 125592
[startup+760.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 29867 0 0 0 75914 98 0 0 25 0 1 0 489598373 129548288 29642 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31628 29642 603 41 0 31587 0
vsize: 126512
[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 30022 0 0 0 76914 98 0 0 25 0 1 0 489598373 130220032 29797 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31792 29797 603 41 0 31751 0
vsize: 127168
[startup+780.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 30147 0 0 0 77914 99 0 0 25 0 1 0 489598373 130625536 29922 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31891 29922 603 41 0 31850 0
vsize: 127564
[startup+790.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 30289 0 0 0 78913 99 0 0 25 0 1 0 489598373 131301376 30064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32056 30064 603 41 0 32015 0
vsize: 128224
[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 30879 0 0 0 79913 101 0 0 25 0 1 0 489598373 133595136 30654 4294967295 134512640 134672761 3221224544 3221223776 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32616 30654 603 41 0 32575 0
vsize: 130464
[startup+810.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 31581 0 0 0 80911 103 0 0 25 0 1 0 489598373 136450048 31356 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 31356 603 41 0 33272 0
vsize: 133252
[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 32110 0 0 0 81909 105 0 0 25 0 1 0 489598373 138739712 31885 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33872 31885 603 41 0 33831 0
vsize: 135488
[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 32513 0 0 0 82908 106 0 0 25 0 1 0 489598373 140345344 32288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34264 32288 603 41 0 34223 0
vsize: 137056
[startup+840.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 32851 0 0 0 83908 107 0 0 25 0 1 0 489598373 141758464 32626 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34609 32626 603 41 0 34568 0
vsize: 138436
[startup+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 33172 0 0 0 84907 108 0 0 25 0 1 0 489598373 143110144 32947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34939 32947 603 41 0 34898 0
vsize: 139756
[startup+860.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 33486 0 0 0 85906 109 0 0 25 0 1 0 489598373 144314368 33261 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35233 33261 603 41 0 35192 0
vsize: 140932
[startup+870.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 33755 0 0 0 86905 110 0 0 25 0 1 0 489598373 145432576 33530 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35506 33530 603 41 0 35465 0
vsize: 142024
[startup+880.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 34072 0 0 0 87904 111 0 0 25 0 1 0 489598373 146780160 33847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35835 33847 603 41 0 35794 0
vsize: 143340
[startup+890.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 34308 0 0 0 88904 111 0 0 25 0 1 0 489598373 147722240 34083 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36065 34083 603 41 0 36024 0
vsize: 144260
[startup+900.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 34532 0 0 0 89904 112 0 0 25 0 1 0 489598373 148525056 34307 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36261 34307 603 41 0 36220 0
vsize: 145044
[startup+910.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 34756 0 0 0 90904 112 0 0 25 0 1 0 489598373 149479424 34531 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36494 34531 603 41 0 36453 0
vsize: 145976
[startup+920.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 34925 0 0 0 91903 113 0 0 25 0 1 0 489598373 150163456 34700 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36661 34700 603 41 0 36620 0
vsize: 146644
[startup+930.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 35105 0 0 0 92903 114 0 0 25 0 1 0 489598373 150999040 34880 4294967295 134512640 134672761 3221224544 3221223664 134542670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36865 34880 603 41 0 36824 0
vsize: 147460
[startup+940.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 35303 0 0 0 93902 114 0 0 25 0 1 0 489598373 151826432 35078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37067 35078 603 41 0 37026 0
vsize: 148268
[startup+950.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 35768 0 0 0 94901 116 0 0 25 0 1 0 489598373 153583616 35543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37496 35543 603 41 0 37455 0
vsize: 149984
[startup+960.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 35912 0 0 0 95900 116 0 0 25 0 1 0 489598373 154275840 35687 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37665 35687 603 41 0 37624 0
vsize: 150660
[startup+970.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 36050 0 0 0 96900 116 0 0 25 0 1 0 489598373 154824704 35825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37799 35825 603 41 0 37758 0
vsize: 151196
[startup+980.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 36206 0 0 0 97900 117 0 0 25 0 1 0 489598373 155361280 35981 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37930 35981 603 41 0 37889 0
vsize: 151720
[startup+990.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 36444 0 0 0 98900 118 0 0 25 0 1 0 489598373 156438528 36219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38193 36219 603 41 0 38152 0
vsize: 152772
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 36697 0 0 0 99899 119 0 0 25 0 1 0 489598373 157380608 36472 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38423 36472 603 41 0 38382 0
vsize: 153692
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 36872 0 0 0 100899 119 0 0 25 0 1 0 489598373 158187520 36647 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38620 36647 603 41 0 38579 0
vsize: 154480
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 37054 0 0 0 101898 120 0 0 25 0 1 0 489598373 158863360 36829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38785 36829 603 41 0 38744 0
vsize: 155140
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 37247 0 0 0 102898 120 0 0 25 0 1 0 489598373 159670272 37022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38982 37022 603 41 0 38941 0
vsize: 155928
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 37437 0 0 0 103898 121 0 0 25 0 1 0 489598373 160481280 37212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39180 37212 603 41 0 39139 0
vsize: 156720
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 37610 0 0 0 104899 121 0 0 25 0 1 0 489598373 161153024 37385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39344 37385 603 41 0 39303 0
vsize: 157376
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 37781 0 0 0 105899 122 0 0 25 0 1 0 489598373 161837056 37556 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39511 37556 603 41 0 39470 0
vsize: 158044
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 37963 0 0 0 106898 122 0 0 25 0 1 0 489598373 162504704 37738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39674 37738 603 41 0 39633 0
vsize: 158696
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 38146 0 0 0 107899 123 0 0 25 0 1 0 489598373 163311616 37921 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39871 37921 603 41 0 39830 0
vsize: 159484
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 38338 0 0 0 108898 123 0 0 25 0 1 0 489598373 164118528 38113 4294967295 134512640 134672761 3221224544 3221223712 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40068 38113 603 41 0 40027 0
vsize: 160272
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 38542 0 0 0 109898 124 0 0 25 0 1 0 489598373 164921344 38317 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40264 38317 603 41 0 40223 0
vsize: 161056
[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 38740 0 0 0 110897 125 0 0 25 0 1 0 489598373 165732352 38515 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40462 38515 603 41 0 40421 0
vsize: 161848
[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 38919 0 0 0 111897 125 0 0 25 0 1 0 489598373 166404096 38694 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40626 38694 603 41 0 40585 0
vsize: 162504
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 39121 0 0 0 112897 126 0 0 25 0 1 0 489598373 167202816 38896 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40821 38896 603 41 0 40780 0
vsize: 163284
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 39325 0 0 0 113896 126 0 0 25 0 1 0 489598373 168140800 39100 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41050 39100 603 41 0 41009 0
vsize: 164200
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 39515 0 0 0 114897 127 0 0 25 0 1 0 489598373 168816640 39290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41215 39290 603 41 0 41174 0
vsize: 164860
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 39712 0 0 0 115897 127 0 0 25 0 1 0 489598373 169631744 39487 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41414 39487 603 41 0 41373 0
vsize: 165656
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 39920 0 0 0 116897 128 0 0 25 0 1 0 489598373 170442752 39695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41612 39695 603 41 0 41571 0
vsize: 166448
[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 40109 0 0 0 117897 128 0 0 25 0 1 0 489598373 171270144 39884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41814 39884 603 41 0 41773 0
vsize: 167256
[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 40285 0 0 0 118897 129 0 0 25 0 1 0 489598373 171945984 40060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41979 40060 603 41 0 41938 0
vsize: 167916
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26321
Raw data (stat): 26319 (minisat+) R 26318 30701 30700 0 -1 0 40487 0 0 0 119896 129 0 0 25 0 1 0 489598373 172888064 40262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42209 40262 603 41 0 42168 0
vsize: 168836
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 26321
Raw data (stat): 26319 (minisat+) Z 26318 30701 30700 0 -1 12 40489 0 0 0 119896 137 0 0 22 0 1 0 489598373 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.23
CPU time (s): 1200.34
CPU user time (s): 1198.97
CPU system time (s): 1.37379
CPU usage (%): 100.009
Max. virtual memory (Kb): 168836
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####