PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-air05.opb
MD5SUM	02b9fdfc96e8b88ab6df67318e21abbc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	29720
Optimality of the best value was proved	NO
Number of terms in the objective function	7195
Biggest coefficient in the objective function	2679
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	3908448
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	2679
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	3908448
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.15
Number of variables	7195
Total number of constraints	7621
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	7621
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	404
Trace number 18344

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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:        591556 kB
Buffers:         34300 kB
Cached:         380708 kB
SwapCached:        540 kB
Active:         139024 kB
Inactive:       278000 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        591276 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20588 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:49:02 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 18184 7 1200.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 852 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 850]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[ 848]---> Adder-cost: 162   maxlim: 86   bits: 7/7
c ---[ 846]---> Adder-cost: 172   maxlim: 90   bits: 7/7
c ---[ 844]---> Adder-cost: 204   maxlim: 106   bits: 7/7
c ---[ 842]---> Adder-cost: 156   maxlim: 80   bits: 7/7
c ---[ 840]---> Adder-cost: 226   maxlim: 118   bits: 7/7
c ---[ 838]---> Adder-cost: 472   maxlim: 245   bits: 8/8
c ---[ 836]---> Adder-cost: 362   maxlim: 228   bits: 8/8
c ---[ 834]---> Adder-cost: 416   maxlim: 214   bits: 8/8
c ---[ 832]---> Adder-cost: 430   maxlim: 230   bits: 8/8
c ---[ 830]---> Adder-cost: 646   maxlim: 332   bits: 9/9
c ---[ 828]---> Adder-cost: 616   maxlim: 357   bits: 9/9
c ---[ 826]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[ 824]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[ 822]---> Adder-cost: 126   maxlim: 67   bits: 7/7
c ---[ 820]---> Adder-cost: 84   maxlim: 52   bits: 6/6
c ---[ 818]---> Adder-cost: 320   maxlim: 166   bits: 8/8
c ---[ 816]---> Adder-cost: 154   maxlim: 82   bits: 7/7
c ---[ 814]---> Adder-cost: 340   maxlim: 176   bits: 8/8
c ---[ 812]---> Adder-cost: 312   maxlim: 186   bits: 8/8
c ---[ 810]---> Adder-cost: 172   maxlim: 91   bits: 7/7
c ---[ 806]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 804]---> Adder-cost: 64   maxlim: 44   bits: 6/6
c ---[ 802]---> Adder-cost: 56   maxlim: 38   bits: 6/6
c ---[ 800]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 798]---> Adder-cost: 208   maxlim: 107   bits: 7/7
c ---[ 796]---> Adder-cost: 148   maxlim: 106   bits: 7/7
c ---[ 794]---> Adder-cost: 196   maxlim: 119   bits: 7/7
c ---[ 792]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[ 788]---> Adder-cost: 84   maxlim: 47   bits: 6/6
c ---[ 786]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 784]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[ 780]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[ 778]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 776]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 774]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[ 772]---> Adder-cost: 170   maxlim: 88   bits: 7/7
c ---[ 770]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[ 768]---> Adder-cost: 202   maxlim: 104   bits: 7/7
c ---[ 766]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[ 764]---> Adder-cost: 186   maxlim: 126   bits: 7/7
c ---[ 762]---> Adder-cost: 442   maxlim: 226   bits: 8/8
c ---[ 760]---> Adder-cost: 270   maxlim: 143   bits: 8/8
c ---[ 758]---> Adder-cost: 236   maxlim: 170   bits: 8/8
c ---[ 756]---> Adder-cost: 408   maxlim: 217   bits: 8/8
c ---[ 754]---> Adder-cost: 184   maxlim: 110   bits: 7/7
c ---[ 752]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 750]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 746]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 744]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 740]---> Adder-cost: 126   maxlim: 67   bits: 7/7
c ---[ 738]---> Adder-cost: 74   maxlim: 39   bits: 6/6
c ---[ 736]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[ 734]---> Adder-cost: 276   maxlim: 141   bits: 8/8
c ---[ 732]---> Adder-cost: 268   maxlim: 143   bits: 8/8
c ---[ 730]---> Adder-cost: 354   maxlim: 194   bits: 8/8
c ---[ 728]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 724]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[ 722]---> Adder-cost: 200   maxlim: 109   bits: 7/7
c ---[ 720]---> Adder-cost: 266   maxlim: 136   bits: 8/8
c ---[ 718]---> Adder-cost: 278   maxlim: 151   bits: 8/8
c ---[ 716]---> Adder-cost: 288   maxlim: 155   bits: 8/8
c ---[ 714]---> Adder-cost: 222   maxlim: 127   bits: 8/7
c ---[ 712]---> Adder-cost: 190   maxlim: 122   bits: 7/7
c ---[ 710]---> Adder-cost: 234   maxlim: 158   bits: 8/8
c ---[ 708]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 706]---> Adder-cost: 146   maxlim: 81   bits: 7/7
c ---[ 704]---> Adder-cost: 312   maxlim: 159   bits: 8/8
c ---[ 702]---> Adder-cost: 280   maxlim: 163   bits: 8/8
c ---[ 700]---> Adder-cost: 282   maxlim: 149   bits: 8/8
c ---[ 698]---> Adder-cost: 220   maxlim: 140   bits: 8/8
c ---[ 696]---> Adder-cost: 380   maxlim: 191   bits: 8/8
c ---[ 694]---> Adder-cost: 462   maxlim: 238   bits: 8/8
c ---[ 692]---> Adder-cost: 282   maxlim: 145   bits: 8/8
c ---[ 690]---> Adder-cost: 264   maxlim: 144   bits: 8/8
c ---[ 688]---> Adder-cost: 212   maxlim: 112   bits: 7/7
c ---[ 686]---> Adder-cost: 146   maxlim: 117   bits: 7/7
c ---[ 684]---> Adder-cost: 524   maxlim: 282   bits: 9/9
c ---[ 682]---> Adder-cost: 466   maxlim: 259   bits: 9/9
c ---[ 680]---> Adder-cost: 486   maxlim: 267   bits: 9/9
c ---[ 678]---> Adder-cost: 668   maxlim: 344   bits: 9/9
c ---[ 676]---> Adder-cost: 468   maxlim: 357   bits: 9/9
c ---[ 674]---> Adder-cost: 534   maxlim: 301   bits: 9/9
c ---[ 672]---> Adder-cost: 324   maxlim: 188   bits: 8/8
c ---[ 670]---> Adder-cost: 708   maxlim: 366   bits: 9/9
c ---[ 668]---> Adder-cost: 594   maxlim: 370   bits: 9/9
c ---[ 666]---> Adder-cost: 718   maxlim: 378   bits: 9/9
c ---[ 664]---> Adder-cost: 456   maxlim: 262   bits: 9/9
c ---[ 662]---> Adder-cost: 488   maxlim: 296   bits: 9/9
c ---[ 660]---> Adder-cost: 596   maxlim: 347   bits: 9/9
c ---[ 658]---> Adder-cost: 156   maxlim: 80   bits: 7/7
c ---[ 656]---> Adder-cost: 192   maxlim: 99   bits: 7/7
c ---[ 654]---> Adder-cost: 218   maxlim: 122   bits: 7/7
c ---[ 652]---> Adder-cost: 248   maxlim: 127   bits: 8/7
c ---[ 650]---> Adder-cost: 198   maxlim: 115   bits: 7/7
c ---[ 648]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[ 646]---> Adder-cost: 272   maxlim: 139   bits: 8/8
c ---[ 644]---> Adder-cost: 220   maxlim: 152   bits: 8/8
c ---[ 642]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 640]---> Adder-cost: 98   maxlim: 59   bits: 6/6
c ---[ 638]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[ 636]---> Adder-cost: 184   maxlim: 106   bits: 7/7
c ---[ 634]---> Adder-cost: 188   maxlim: 96   bits: 7/7
c ---[ 630]---> Adder-cost: 156   maxlim: 95   bits: 7/7
c ---[ 628]---> Adder-cost: 396   maxlim: 203   bits: 8/8
c ---[ 626]---> Adder-cost: 408   maxlim: 230   bits: 8/8
c ---[ 624]---> Adder-cost: 444   maxlim: 233   bits: 8/8
c ---[ 622]---> Adder-cost: 384   maxlim: 219   bits: 8/8
c ---[ 620]---> Adder-cost: 254   maxlim: 127   bits: 8/7
c ---[ 618]---> Adder-cost: 162   maxlim: 92   bits: 7/7
c ---[ 616]---> Adder-cost: 400   maxlim: 208   bits: 8/8
c ---[ 614]---> Adder-cost: 380   maxlim: 211   bits: 8/8
c ---[ 612]---> Adder-cost: 94   maxlim: 52   bits: 6/6
c ---[ 610]---> Adder-cost: 124   maxlim: 65   bits: 7/7
c ---[ 608]---> Adder-cost: 300   maxlim: 155   bits: 8/8
c ---[ 606]---> Adder-cost: 180   maxlim: 155   bits: 8/8
c ---[ 604]---> Adder-cost: 122   maxlim: 78   bits: 7/7
c ---[ 596]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 594]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 592]---> Adder-cost: 250   maxlim: 127   bits: 8/7
c ---[ 590]---> Adder-cost: 214   maxlim: 144   bits: 8/8
c ---[ 588]---> Adder-cost: 434   maxlim: 223   bits: 8/8
c ---[ 586]---> Adder-cost: 364   maxlim: 216   bits: 8/8
c ---[ 584]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 582]---> Adder-cost: 98   maxlim: 54   bits: 6/6
c ---[ 580]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 578]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[ 576]---> Adder-cost: 122   maxlim: 68   bits: 7/7
c ---[ 574]---> Adder-cost: 154   maxlim: 88   bits: 7/7
c ---[ 572]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 570]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 568]---> Adder-cost: 6   maxlim: 6   bits: 3/3
c ---[ 566]---> Adder-cost: 20   maxlim: 14   bits: 4/4
c ---[ 564]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 562]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[ 560]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 558]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 556]---> Adder-cost: 94   maxlim: 59   bits: 6/6
c ---[ 554]---> Adder-cost: 506   maxlim: 263   bits: 9/9
c ---[ 552]---> Adder-cost: 428   maxlim: 255   bits: 9/8
c ---[ 548]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 546]---> Adder-cost: 176   maxlim: 98   bits: 7/7
c ---[ 544]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[ 542]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 540]---> Adder-cost: 298   maxlim: 163   bits: 8/8
c ---[ 538]---> Adder-cost: 450   maxlim: 243   bits: 8/8
c ---[ 536]---> Adder-cost: 260   maxlim: 137   bits: 8/8
c ---[ 534]---> Adder-cost: 256   maxlim: 153   bits: 8/8
c ---[ 532]---> Adder-cost: 316   maxlim: 182   bits: 8/8
c ---[ 530]---> Adder-cost: 230   maxlim: 162   bits: 8/8
c ---[ 528]---> Adder-cost: 172   maxlim: 93   bits: 7/7
c ---[ 526]---> Adder-cost: 292   maxlim: 158   bits: 8/8
c ---[ 524]---> Adder-cost: 272   maxlim: 146   bits: 8/8
c ---[ 522]---> Adder-cost: 376   maxlim: 192   bits: 8/8
c ---[ 520]---> Adder-cost: 288   maxlim: 181   bits: 8/8
c ---[ 518]---> Adder-cost: 190   maxlim: 105   bits: 7/7
c ---[ 516]---> Adder-cost: 156   maxlim: 106   bits: 7/7
c ---[ 514]---> Adder-cost: 254   maxlim: 133   bits: 8/8
c ---[ 512]---> Adder-cost: 160   maxlim: 99   bits: 7/7
c ---[ 510]---> Adder-cost: 152   maxlim: 96   bits: 7/7
c ---[ 508]---> Adder-cost: 164   maxlim: 100   bits: 7/7
c ---[ 506]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[ 504]---> Adder-cost: 64   maxlim: 35   bits: 6/6
c ---[ 502]---> Adder-cost: 522   maxlim: 274   bits: 9/9
c ---[ 500]---> Adder-cost: 488   maxlim: 286   bits: 9/9
c ---[ 498]---> Adder-cost: 162   maxlim: 86   bits: 7/7
c ---[ 496]---> Adder-cost: 128   maxlim: 90   bits: 7/7
c ---[ 494]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[ 492]---> Adder-cost: 110   maxlim: 70   bits: 7/7
c ---[ 490]---> Adder-cost: 548   maxlim: 283   bits: 9/9
c ---[ 488]---> Adder-cost: 404   maxlim: 291   bits: 9/9
c ---[ 486]---> Adder-cost: 254   maxlim: 128   bits: 8/8
c ---[ 484]---> Adder-cost: 178   maxlim: 113   bits: 7/7
c ---[ 482]---> Adder-cost: 176   maxlim: 96   bits: 7/7
c ---[ 480]---> Adder-cost: 216   maxlim: 119   bits: 7/7
c ---[ 478]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 476]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 474]---> Adder-cost: 62   maxlim: 39   bits: 6/6
c ---[ 472]---> Adder-cost: 500   maxlim: 261   bits: 9/9
c ---[ 470]---> Adder-cost: 458   maxlim: 268   bits: 9/9
c ---[ 468]---> Adder-cost: 326   maxlim: 171   bits: 8/8
c ---[ 466]---> Adder-cost: 232   maxlim: 127   bits: 8/7
c ---[ 464]---> Adder-cost: 286   maxlim: 147   bits: 8/8
c ---[ 462]---> Adder-cost: 290   maxlim: 165   bits: 8/8
c ---[ 460]---> Adder-cost: 416   maxlim: 216   bits: 8/8
c ---[ 458]---> Adder-cost: 334   maxlim: 211   bits: 8/8
c ---[ 456]---> Adder-cost: 390   maxlim: 210   bits: 8/8
c ---[ 454]---> Adder-cost: 334   maxlim: 206   bits: 8/8
c ---[ 452]---> Adder-cost: 448   maxlim: 247   bits: 8/8
c ---[ 450]---> Adder-cost: 252   maxlim: 154   bits: 8/8
c ---[ 448]---> Adder-cost: 210   maxlim: 116   bits: 7/7
c ---[ 446]---> Adder-cost: 78   maxlim: 45   bits: 6/6
c ---[ 444]---> Adder-cost: 74   maxlim: 45   bits: 6/6
c ---[ 442]---> Adder-cost: 674   maxlim: 373   bits: 9/9
c ---[ 440]---> Adder-cost: 502   maxlim: 283   bits: 9/9
c ---[ 438]---> Adder-cost: 688   maxlim: 403   bits: 9/9
c ---[ 436]---> Adder-cost: 640   maxlim: 337   bits: 9/9
c ---[ 434]---> Adder-cost: 516   maxlim: 293   bits: 9/9
c ---[ 432]---> Adder-cost: 428   maxlim: 276   bits: 9/9
c ---[ 428]---> Adder-cost: 314   maxlim: 161   bits: 8/8
c ---[ 426]---> Adder-cost: 360   maxlim: 189   bits: 8/8
c ---[ 424]---> Adder-cost: 356   maxlim: 202   bits: 8/8
c ---[ 422]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[ 420]---> Adder-cost: 78   maxlim: 51   bits: 6/6
c ---[ 416]---> Adder-cost: 624   maxlim: 322   bits: 9/9
c ---[ 414]---> Adder-cost: 158   maxlim: 89   bits: 7/7
c ---[ 412]---> Adder-cost: 154   maxlim: 85   bits: 7/7
c ---[ 410]---> Adder-cost: 120   maxlim: 100   bits: 7/7
c ---[ 406]---> Adder-cost: 266   maxlim: 135   bits: 8/8
c ---[ 404]---> Adder-cost: 218   maxlim: 116   bits: 7/7
c ---[ 402]---> Adder-cost: 158   maxlim: 95   bits: 7/7
c ---[ 400]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 398]---> Adder-cost: 72   maxlim: 52   bits: 6/6
c ---[ 396]---> Adder-cost: 116   maxlim: 66   bits: 7/7
c ---[ 394]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 392]---> Adder-cost: 80   maxlim: 58   bits: 6/6
c ---[ 390]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 388]---> Adder-cost: 110   maxlim: 61   bits: 6/6
c ---[ 386]---> Adder-cost: 384   maxlim: 203   bits: 8/8
c ---[ 384]---> Adder-cost: 156   maxlim: 107   bits: 7/7
c ---[ 382]---> Adder-cost: 110   maxlim: 75   bits: 7/7
c ---[ 380]---> Adder-cost: 160   maxlim: 108   bits: 7/7
c ---[ 378]---> Adder-cost: 518   maxlim: 267   bits: 9/9
c ---[ 376]---> Adder-cost: 476   maxlim: 275   bits: 9/9
c ---[ 374]---> Adder-cost: 308   maxlim: 162   bits: 8/8
c ---[ 372]---> Adder-cost: 244   maxlim: 151   bits: 8/8
c ---[ 370]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 368]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 366]---> Adder-cost: 20   maxlim: 14   bits: 4/4
c ---[ 364]---> Adder-cost: 26   maxlim: 17   bits: 5/5
c ---[ 362]---> Adder-cost: 216   maxlim: 113   bits: 7/7
c ---[ 360]---> Adder-cost: 128   maxlim: 111   bits: 7/7
c ---[ 358]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 356]---> Adder-cost: 76   maxlim: 70   bits: 7/7
c ---[ 354]---> Adder-cost: 108   maxlim: 69   bits: 7/7
c ---[ 352]---> Adder-cost: 158   maxlim: 89   bits: 7/7
c ---[ 350]---> Adder-cost: 146   maxlim: 78   bits: 7/7
c ---[ 348]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[ 346]---> Adder-cost: 344   maxlim: 182   bits: 8/8
c ---[ 344]---> Adder-cost: 250   maxlim: 154   bits: 8/8
c ---[ 342]---> Adder-cost: 234   maxlim: 123   bits: 7/7
c ---[ 340]---> Adder-cost: 180   maxlim: 114   bits: 7/7
c ---[ 334]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 332]---> Adder-cost: 122   maxlim: 75   bits: 7/7
c ---[ 330]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 328]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 326]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 324]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 322]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 320]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 318]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 316]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[ 314]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 312]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 310]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 308]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[ 306]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 304]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 302]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 300]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 298]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 296]---> Adder-cost: 72   maxlim: 41   bits: 6/6
c ---[ 294]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[ 292]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[ 290]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[ 288]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[ 286]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 284]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[ 282]---> Adder-cost: 48   maxlim: 27   bits: 5/5
c ---[ 280]---> Adder-cost: 128   maxlim: 70   bits: 7/7
c ---[ 278]---> Adder-cost: 334   maxlim: 171   bits: 8/8
c ---[ 276]---> Adder-cost: 202   maxlim: 108   bits: 7/7
c ---[ 274]---> Adder-cost: 156   maxlim: 83   bits: 7/7
c ---[ 272]---> Adder-cost: 116   maxlim: 89   bits: 7/7
c ---[ 270]---> Adder-cost: 326   maxlim: 183   bits: 8/8
c ---[ 266]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 264]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 262]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 260]---> Adder-cost: 34   maxlim: 26   bits: 5/5
c ---[ 258]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 256]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 254]---> Adder-cost: 184   maxlim: 95   bits: 7/7
c ---[ 252]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[ 250]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 248]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 246]---> Adder-cost: 330   maxlim: 171   bits: 8/8
c ---[ 244]---> Adder-cost: 182   maxlim: 97   bits: 7/7
c ---[ 242]---> Adder-cost: 146   maxlim: 103   bits: 7/7
c ---[ 240]---> Adder-cost: 514   maxlim: 271   bits: 9/9
c ---[ 238]---> Adder-cost: 508   maxlim: 272   bits: 9/9
c ---[ 236]---> Adder-cost: 422   maxlim: 219   bits: 8/8
c ---[ 234]---> Adder-cost: 318   maxlim: 188   bits: 8/8
c ---[ 232]---> Adder-cost: 226   maxlim: 122   bits: 7/7
c ---[ 230]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[ 228]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[ 226]---> Adder-cost: 256   maxlim: 138   bits: 8/8
c ---[ 224]---> Adder-cost: 164   maxlim: 87   bits: 7/7
c ---[ 222]---> Adder-cost: 142   maxlim: 79   bits: 7/7
c ---[ 220]---> Adder-cost: 138   maxlim: 72   bits: 7/7
c ---[ 218]---> Adder-cost: 108   maxlim: 73   bits: 7/7
c ---[ 216]---> Adder-cost: 154   maxlim: 84   bits: 7/7
c ---[ 214]---> Adder-cost: 122   maxlim: 77   bits: 7/7
c ---[ 212]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[ 210]---> Adder-cost: 108   maxlim: 73   bits: 7/7
c ---[ 208]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 206]---> Adder-cost: 54   maxlim: 75   bits: 7/7
c ---[ 204]---> Adder-cost: 140   maxlim: 76   bits: 7/7
c ---[ 202]---> Adder-cost: 90   maxlim: 79   bits: 7/7
c ---[ 200]---> Adder-cost: 204   maxlim: 113   bits: 7/7
c ---[ 198]---> Adder-cost: 208   maxlim: 120   bits: 7/7
c ---[ 196]---> Adder-cost: 430   maxlim: 228   bits: 8/8
c ---[ 194]---> Adder-cost: 406   maxlim: 234   bits: 8/8
c ---[ 192]---> Adder-cost: 180   maxlim: 104   bits: 7/7
c ---[ 190]---> Adder-cost: 196   maxlim: 113   bits: 7/7
c ---[ 188]---> Adder-cost: 140   maxlim: 114   bits: 7/7
c ---[ 186]---> Adder-cost: 146   maxlim: 79   bits: 7/7
c ---[ 184]---> Adder-cost: 288   maxlim: 157   bits: 8/8
c ---[ 182]---> Adder-cost: 178   maxlim: 113   bits: 7/7
c ---[ 180]---> Adder-cost: 154   maxlim: 100   bits: 7/7
c ---[ 178]---> Adder-cost: 340   maxlim: 176   bits: 8/8
c ---[ 176]---> Adder-cost: 322   maxlim: 181   bits: 8/8
c ---[ 174]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[ 172]---> Adder-cost: 94   maxlim: 56   bits: 6/6
c ---[ 170]---> Adder-cost: 630   maxlim: 329   bits: 9/9
c ---[ 168]---> Adder-cost: 472   maxlim: 322   bits: 9/9
c ---[ 166]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 164]---> Adder-cost: 182   maxlim: 113   bits: 7/7
c ---[ 162]---> Adder-cost: 328   maxlim: 172   bits: 8/8
c ---[ 160]---> Adder-cost: 462   maxlim: 262   bits: 9/9
c ---[ 158]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 156]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 154]---> Adder-cost: 88   maxlim: 47   bits: 6/6
c ---[ 152]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[ 150]---> Adder-cost: 192   maxlim: 106   bits: 7/7
c ---[ 146]---> Adder-cost: 274   maxlim: 142   bits: 8/8
c ---[ 144]---> Adder-cost: 474   maxlim: 252   bits: 8/8
c ---[ 142]---> Adder-cost: 312   maxlim: 166   bits: 8/8
c ---[ 140]---> Adder-cost: 210   maxlim: 127   bits: 8/7
c ---[ 138]---> Adder-cost: 266   maxlim: 159   bits: 8/8
c ---[ 136]---> Adder-cost: 268   maxlim: 157   bits: 8/8
c ---[ 134]---> Adder-cost: 348   maxlim: 185   bits: 8/8
c ---[ 132]---> Adder-cost: 536   maxlim: 301   bits: 9/9
c ---[ 130]---> Adder-cost: 274   maxlim: 140   bits: 8/8
c ---[ 128]---> Adder-cost: 204   maxlim: 129   bits: 8/8
c ---[ 126]---> Adder-cost: 190   maxlim: 101   bits: 7/7
c ---[ 124]---> Adder-cost: 316   maxlim: 171   bits: 8/8
c ---[ 122]---> Adder-cost: 290   maxlim: 155   bits: 8/8
c ---[ 120]---> Adder-cost: 224   maxlim: 173   bits: 8/8
c ---[ 118]---> Adder-cost: 446   maxlim: 229   bits: 8/8
c ---[ 116]---> Adder-cost: 400   maxlim: 220   bits: 8/8
c ---[ 114]---> Adder-cost: 288   maxlim: 150   bits: 8/8
c ---[ 112]---> Adder-cost: 244   maxlim: 136   bits: 8/8
c ---[ 110]---> Adder-cost: 358   maxlim: 188   bits: 8/8
c ---[ 108]---> Adder-cost: 340   maxlim: 181   bits: 8/8
c ---[ 106]---> Adder-cost: 334   maxlim: 186   bits: 8/8
c ---[ 104]---> Adder-cost: 382   maxlim: 221   bits: 8/8
c ---[ 102]---> Adder-cost: 276   maxlim: 147   bits: 8/8
c ---[ 100]---> Adder-cost: 398   maxlim: 209   bits: 8/8
c ---[  98]---> Adder-cost: 276   maxlim: 147   bits: 8/8
c ---[  96]---> Adder-cost: 164   maxlim: 90   bits: 7/7
c ---[  94]---> Adder-cost: 116   maxlim: 75   bits: 7/7
c ---[  92]---> Adder-cost: 134   maxlim: 72   bits: 7/7
c ---[  90]---> Adder-cost: 118   maxlim: 71   bits: 7/7
c ---[  88]---> Adder-cost: 316   maxlim: 169   bits: 8/8
c ---[  86]---> Adder-cost: 206   maxlim: 169   bits: 8/8
c ---[  84]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[  82]---> Adder-cost: 74   maxlim: 53   bits: 6/6
c ---[  80]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[  78]---> Adder-cost: 12   maxlim: 8   bits: 4/4
c ---[  76]---> Adder-cost: 206   maxlim: 107   bits: 7/7
c ---[  74]---> Adder-cost: 184   maxlim: 128   bits: 8/8
c ---[  72]---> Adder-cost: 308   maxlim: 165   bits: 8/8
c ---[  70]---> Adder-cost: 288   maxlim: 171   bits: 8/8
c ---[  68]---> Adder-cost: 288   maxlim: 149   bits: 8/8
c ---[  66]---> Adder-cost: 236   maxlim: 127   bits: 8/7
c ---[  64]---> Adder-cost: 436   maxlim: 232   bits: 8/8
c ---[  62]---> Adder-cost: 358   maxlim: 191   bits: 8/8
c ---[  60]---> Adder-cost: 260   maxlim: 162   bits: 8/8
c ---[  58]---> Adder-cost: 204   maxlim: 148   bits: 8/8
c ---[  56]---> Adder-cost: 166   maxlim: 113   bits: 7/7
c ---[  54]---> Adder-cost: 242   maxlim: 133   bits: 8/8
c ---[  52]---> Adder-cost: 556   maxlim: 293   bits: 9/9
c ---[  50]---> Adder-cost: 490   maxlim: 274   bits: 9/9
c ---[  48]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  46]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[  44]---> Adder-cost: 174   maxlim: 93   bits: 7/7
c ---[  42]---> Adder-cost: 208   maxlim: 117   bits: 7/7
c ---[  40]---> Adder-cost: 166   maxlim: 88   bits: 7/7
c ---[  38]---> Adder-cost: 92   maxlim: 57   bits: 6/6
c ---[  36]---> Adder-cost: 100   maxlim: 59   bits: 6/6
c ---[  34]---> Adder-cost: 112   maxlim: 73   bits: 7/7
c ---[  32]---> Adder-cost: 156   maxlim: 84   bits: 7/7
c ---[  30]---> Adder-cost: 194   maxlim: 117   bits: 7/7
c ---[  28]---> Adder-cost: 386   maxlim: 225   bits: 8/8
c ---[  26]---> Adder-cost: 346   maxlim: 175   bits: 8/8
c ---[  24]---> Adder-cost: 260   maxlim: 159   bits: 8/8
c ---[  22]---> Adder-cost: 466   maxlim: 251   bits: 8/8
c ---[  20]---> Adder-cost: 250   maxlim: 138   bits: 8/8
c ---[  18]---> Adder-cost: 264   maxlim: 141   bits: 8/8
c ---[  16]---> Adder-cost: 246   maxlim: 128   bits: 8/8
c ---[  14]---> Adder-cost: 144   maxlim: 107   bits: 7/7
c ---[  12]---> Adder-cost: 158   maxlim: 120   bits: 7/7
c ---[  10]---> Adder-cost: 194   maxlim: 102   bits: 7/7
c ---[   8]---> Adder-cost: 224   maxlim: 119   bits: 7/7
c ---[   6]---> Adder-cost: 166   maxlim: 92   bits: 7/7
c ---[   4]---> Adder-cost: 148   maxlim: 94   bits: 7/7
c ---[   2]---> Adder-cost: 204   maxlim: 107   bits: 7/7
c ---[   0]---> Adder-cost: 180   maxlim: 105   bits: 7/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  604037  2151407 |  201345       0        0     nan |  0.000 % |
c |       100 |  603363  2149087 |  221479      23       66     2.9 |  6.371 % |
c |       250 |  602236  2145126 |  243627      49      235     4.8 |  6.566 % |
c |       475 |  600790  2140064 |  267990     102      405     4.0 |  6.815 % |
c |       812 |  598667  2132685 |  294789     199      780     3.9 |  7.195 % |
c |      1319 |  595634  2122094 |  324268     352     1430     4.1 |  7.702 % |
c |      2078 |  591771  2108607 |  356694     664     2905     4.4 |  8.369 % |
c |      3219 |  588158  2096046 |  392364    1411     6415     4.5 |  8.989 % |
c |      4927 |  582376  2075852 |  431600    2425    12014     5.0 |  9.974 % |
c |      7489 |  575971  2053251 |  474760    4211    21145     5.0 | 11.054 % |
c |     11333 |  568657  2027287 |  522237    7136    37856     5.3 | 12.309 % |
c |     17099 |  554615  1977803 |  574460   11010    60931     5.5 | 14.655 % |
c |     25749 |  529806  1890228 |  631906   16184    94936     5.9 | 18.878 % |
#### 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.66 0.89 0.93 2/54 27466
Raw data (stat): 27466 (runsolver) R 27465 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545790425 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.71 0.89 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11174 0 0 0 971 28 0 0 25 0 1 0 545790425 50323456 10781 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12286 10781 603 41 0 12245 0
vsize: 49144
[startup+20.0019 s]
Raw data (loadavg): 0.75 0.90 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11183 0 0 0 1970 28 0 0 25 0 1 0 545790425 50323456 10790 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12286 10790 603 41 0 12245 0
vsize: 49144
[startup+30.1038 s]
Raw data (loadavg): 0.79 0.90 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11198 0 0 0 2980 28 0 0 25 0 1 0 545790425 50458624 10805 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12319 10805 603 41 0 12278 0
vsize: 49276
[startup+40.104 s]
Raw data (loadavg): 0.82 0.90 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11228 0 0 0 3980 29 0 0 25 0 1 0 545790425 50614272 10835 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 10835 603 41 0 12316 0
vsize: 49428
[startup+50.1046 s]
Raw data (loadavg): 0.85 0.91 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11263 0 0 0 4980 29 0 0 25 0 1 0 545790425 50749440 10870 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12390 10870 603 41 0 12349 0
vsize: 49560
[startup+60.1046 s]
Raw data (loadavg): 0.87 0.91 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11292 0 0 0 5980 29 0 0 25 0 1 0 545790425 50749440 10899 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12390 10899 603 41 0 12349 0
vsize: 49560
[startup+70.1048 s]
Raw data (loadavg): 0.89 0.91 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11320 0 0 0 6980 29 0 0 25 0 1 0 545790425 50884608 10927 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12423 10927 603 41 0 12382 0
vsize: 49692
[startup+80.1044 s]
Raw data (loadavg): 0.91 0.91 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11341 0 0 0 7980 29 0 0 25 0 1 0 545790425 51019776 10948 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12456 10948 603 41 0 12415 0
vsize: 49824
[startup+90.1044 s]
Raw data (loadavg): 0.92 0.92 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11361 0 0 0 8980 29 0 0 25 0 1 0 545790425 51154944 10968 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12489 10968 603 41 0 12448 0
vsize: 49956
[startup+100.105 s]
Raw data (loadavg): 0.93 0.92 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11393 0 0 0 9981 29 0 0 25 0 1 0 545790425 51314688 11000 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 11000 603 41 0 12487 0
vsize: 50112
[startup+110.105 s]
Raw data (loadavg): 0.94 0.92 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11416 0 0 0 10981 29 0 0 25 0 1 0 545790425 51314688 11023 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 11023 603 41 0 12487 0
vsize: 50112
[startup+120.105 s]
Raw data (loadavg): 0.95 0.92 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11446 0 0 0 11980 30 0 0 25 0 1 0 545790425 51449856 11053 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12561 11053 603 41 0 12520 0
vsize: 50244
[startup+130.105 s]
Raw data (loadavg): 0.96 0.92 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11461 0 0 0 12980 30 0 0 25 0 1 0 545790425 51449856 11068 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12561 11068 603 41 0 12520 0
vsize: 50244
[startup+140.105 s]
Raw data (loadavg): 0.96 0.93 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11478 0 0 0 13980 30 0 0 25 0 1 0 545790425 51585024 11085 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12594 11085 603 41 0 12553 0
vsize: 50376
[startup+150.106 s]
Raw data (loadavg): 0.97 0.93 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11488 0 0 0 14979 30 0 0 25 0 1 0 545790425 51585024 11095 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11095 603 41 0 12553 0
vsize: 50376
[startup+160.106 s]
Raw data (loadavg): 0.97 0.93 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11499 0 0 0 15979 31 0 0 25 0 1 0 545790425 51720192 11106 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11106 603 41 0 12586 0
vsize: 50508
[startup+170.106 s]
Raw data (loadavg): 0.98 0.93 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11519 0 0 0 16979 31 0 0 25 0 1 0 545790425 51720192 11126 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11126 603 41 0 12586 0
vsize: 50508
[startup+180.106 s]
Raw data (loadavg): 0.98 0.93 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11536 0 0 0 17978 32 0 0 25 0 1 0 545790425 51855360 11143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 11143 603 41 0 12619 0
vsize: 50640
[startup+190.107 s]
Raw data (loadavg): 0.98 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11548 0 0 0 18978 32 0 0 25 0 1 0 545790425 51855360 11155 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 11155 603 41 0 12619 0
vsize: 50640
[startup+200.107 s]
Raw data (loadavg): 0.98 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11561 0 0 0 19978 32 0 0 25 0 1 0 545790425 51855360 11168 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 11168 603 41 0 12619 0
vsize: 50640
[startup+210.108 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11576 0 0 0 20978 33 0 0 25 0 1 0 545790425 51990528 11183 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11183 603 41 0 12652 0
vsize: 50772
[startup+220.109 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11586 0 0 0 21977 33 0 0 25 0 1 0 545790425 51990528 11193 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11193 603 41 0 12652 0
vsize: 50772
[startup+230.109 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11596 0 0 0 22977 33 0 0 25 0 1 0 545790425 51990528 11203 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11203 603 41 0 12652 0
vsize: 50772
[startup+240.109 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11603 0 0 0 23977 34 0 0 25 0 1 0 545790425 51990528 11210 4294967295 134512640 134672761 3221224544 3221223792 134562140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11210 603 41 0 12652 0
vsize: 50772
[startup+250.108 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11606 0 0 0 24977 34 0 0 25 0 1 0 545790425 52125696 11213 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11213 603 41 0 12685 0
vsize: 50904
[startup+260.11 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11608 0 0 0 25977 34 0 0 25 0 1 0 545790425 52125696 11215 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11215 603 41 0 12685 0
vsize: 50904
[startup+270.111 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11610 0 0 0 26976 35 0 0 25 0 1 0 545790425 52125696 11217 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11217 603 41 0 12685 0
vsize: 50904
[startup+280.11 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11615 0 0 0 27977 35 0 0 25 0 1 0 545790425 52125696 11222 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11222 603 41 0 12685 0
vsize: 50904
[startup+290.111 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11619 0 0 0 28977 35 0 0 25 0 1 0 545790425 52125696 11226 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11226 603 41 0 12685 0
vsize: 50904
[startup+300.111 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11626 0 0 0 29977 35 0 0 25 0 1 0 545790425 52125696 11233 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11233 603 41 0 12685 0
vsize: 50904
[startup+310.112 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11627 0 0 0 30976 35 0 0 25 0 1 0 545790425 52125696 11234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11234 603 41 0 12685 0
vsize: 50904
[startup+320.112 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11628 0 0 0 31977 35 0 0 25 0 1 0 545790425 52125696 11235 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11235 603 41 0 12685 0
vsize: 50904
[startup+330.112 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11630 0 0 0 32977 35 0 0 25 0 1 0 545790425 52125696 11237 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11237 603 41 0 12685 0
vsize: 50904
[startup+340.113 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11633 0 0 0 33977 35 0 0 25 0 1 0 545790425 52125696 11240 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11240 603 41 0 12685 0
vsize: 50904
[startup+350.113 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11635 0 0 0 34977 35 0 0 25 0 1 0 545790425 52125696 11242 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11242 603 41 0 12685 0
vsize: 50904
[startup+360.114 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11638 0 0 0 35977 35 0 0 25 0 1 0 545790425 52125696 11245 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11245 603 41 0 12685 0
vsize: 50904
[startup+370.113 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11639 0 0 0 36977 35 0 0 25 0 1 0 545790425 52125696 11246 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11246 603 41 0 12685 0
vsize: 50904
[startup+380.114 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11640 0 0 0 37977 35 0 0 25 0 1 0 545790425 52125696 11247 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11247 603 41 0 12685 0
vsize: 50904
[startup+390.115 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11642 0 0 0 38977 35 0 0 25 0 1 0 545790425 52125696 11249 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11249 603 41 0 12685 0
vsize: 50904
[startup+400.114 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11643 0 0 0 39978 35 0 0 25 0 1 0 545790425 52125696 11250 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11250 603 41 0 12685 0
vsize: 50904
[startup+410.115 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11644 0 0 0 40978 35 0 0 25 0 1 0 545790425 52125696 11251 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11251 603 41 0 12685 0
vsize: 50904
[startup+420.115 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11644 0 0 0 41978 36 0 0 25 0 1 0 545790425 52125696 11251 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11251 603 41 0 12685 0
vsize: 50904
[startup+430.115 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11650 0 0 0 42978 36 0 0 25 0 1 0 545790425 52269056 11257 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11257 603 41 0 12720 0
vsize: 51044
[startup+440.115 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11650 0 0 0 43978 36 0 0 25 0 1 0 545790425 52269056 11257 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11257 603 41 0 12720 0
vsize: 51044
[startup+450.115 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11652 0 0 0 44978 36 0 0 25 0 1 0 545790425 52269056 11259 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11259 603 41 0 12720 0
vsize: 51044
[startup+460.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11652 0 0 0 45978 36 0 0 25 0 1 0 545790425 52269056 11259 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11259 603 41 0 12720 0
vsize: 51044
[startup+470.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11653 0 0 0 46978 36 0 0 25 0 1 0 545790425 52269056 11260 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+480.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11653 0 0 0 47979 36 0 0 25 0 1 0 545790425 52269056 11260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+490.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11653 0 0 0 48979 36 0 0 25 0 1 0 545790425 52269056 11260 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+500.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11654 0 0 0 49979 36 0 0 25 0 1 0 545790425 52269056 11261 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+510.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11654 0 0 0 50979 36 0 0 25 0 1 0 545790425 52269056 11261 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+520.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11654 0 0 0 51979 36 0 0 25 0 1 0 545790425 52269056 11261 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+530.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11654 0 0 0 52979 36 0 0 25 0 1 0 545790425 52269056 11261 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+540.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11654 0 0 0 53979 36 0 0 25 0 1 0 545790425 52269056 11261 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+550.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11654 0 0 0 54979 36 0 0 25 0 1 0 545790425 52269056 11261 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+560.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11655 0 0 0 55980 36 0 0 25 0 1 0 545790425 52269056 11262 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11262 603 41 0 12720 0
vsize: 51044
[startup+570.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11656 0 0 0 56980 36 0 0 25 0 1 0 545790425 52269056 11263 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11263 603 41 0 12720 0
vsize: 51044
[startup+580.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11656 0 0 0 57979 36 0 0 25 0 1 0 545790425 52269056 11263 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11263 603 41 0 12720 0
vsize: 51044
[startup+590.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11656 0 0 0 58980 36 0 0 25 0 1 0 545790425 52269056 11263 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11263 603 41 0 12720 0
vsize: 51044
[startup+600.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11657 0 0 0 59979 37 0 0 25 0 1 0 545790425 52269056 11264 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11264 603 41 0 12720 0
vsize: 51044
[startup+610.119 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11658 0 0 0 60980 37 0 0 25 0 1 0 545790425 52269056 11265 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11265 603 41 0 12720 0
vsize: 51044
[startup+620.119 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11659 0 0 0 61980 37 0 0 25 0 1 0 545790425 52269056 11266 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11266 603 41 0 12720 0
vsize: 51044
[startup+630.119 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11668 0 0 0 62980 37 0 0 25 0 1 0 545790425 52269056 11275 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+640.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11668 0 0 0 63980 37 0 0 25 0 1 0 545790425 52269056 11275 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+650.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11668 0 0 0 64980 37 0 0 25 0 1 0 545790425 52269056 11275 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+660.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11668 0 0 0 65980 37 0 0 25 0 1 0 545790425 52269056 11275 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+670.121 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11670 0 0 0 66980 37 0 0 25 0 1 0 545790425 52269056 11277 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+680.121 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11670 0 0 0 67980 37 0 0 25 0 1 0 545790425 52269056 11277 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+690.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11670 0 0 0 68981 37 0 0 25 0 1 0 545790425 52269056 11277 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+700.121 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11670 0 0 0 69981 37 0 0 25 0 1 0 545790425 52269056 11277 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+710.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11673 0 0 0 70981 37 0 0 25 0 1 0 545790425 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+720.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11673 0 0 0 71981 37 0 0 25 0 1 0 545790425 52269056 11280 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+730.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11673 0 0 0 72981 37 0 0 25 0 1 0 545790425 52269056 11280 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+740.123 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11673 0 0 0 73981 37 0 0 25 0 1 0 545790425 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+750.124 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11673 0 0 0 74981 37 0 0 25 0 1 0 545790425 52269056 11280 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+760.124 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11674 0 0 0 75981 38 0 0 25 0 1 0 545790425 52269056 11281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11281 603 41 0 12720 0
vsize: 51044
[startup+770.124 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11674 0 0 0 76981 38 0 0 25 0 1 0 545790425 52269056 11281 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11281 603 41 0 12720 0
vsize: 51044
[startup+780.124 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11676 0 0 0 77981 38 0 0 25 0 1 0 545790425 52269056 11283 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+790.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11676 0 0 0 78981 38 0 0 25 0 1 0 545790425 52269056 11283 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+800.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11676 0 0 0 79980 38 0 0 25 0 1 0 545790425 52269056 11283 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+810.126 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11679 0 0 0 80980 38 0 0 25 0 1 0 545790425 52269056 11286 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11286 603 41 0 12720 0
vsize: 51044
[startup+820.126 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11681 0 0 0 81980 38 0 0 25 0 1 0 545790425 52269056 11288 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11288 603 41 0 12720 0
vsize: 51044
[startup+830.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11682 0 0 0 82980 38 0 0 25 0 1 0 545790425 52269056 11289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11289 603 41 0 12720 0
vsize: 51044
[startup+840.126 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11682 0 0 0 83980 38 0 0 25 0 1 0 545790425 52269056 11289 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11289 603 41 0 12720 0
vsize: 51044
[startup+850.126 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11684 0 0 0 84981 38 0 0 25 0 1 0 545790425 52269056 11291 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11291 603 41 0 12720 0
vsize: 51044
[startup+860.127 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11687 0 0 0 85981 38 0 0 25 0 1 0 545790425 52269056 11294 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11294 603 41 0 12720 0
vsize: 51044
[startup+870.126 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11687 0 0 0 86981 38 0 0 25 0 1 0 545790425 52269056 11294 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11294 603 41 0 12720 0
vsize: 51044
[startup+880.137 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11688 0 0 0 87982 39 0 0 25 0 1 0 545790425 52269056 11295 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11295 603 41 0 12720 0
vsize: 51044
[startup+890.137 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11688 0 0 0 88982 39 0 0 25 0 1 0 545790425 52269056 11295 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11295 603 41 0 12720 0
vsize: 51044
[startup+900.147 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11689 0 0 0 89983 39 0 0 25 0 1 0 545790425 52269056 11296 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11296 603 41 0 12720 0
vsize: 51044
[startup+910.151 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11689 0 0 0 90984 39 0 0 25 0 1 0 545790425 52269056 11296 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11296 603 41 0 12720 0
vsize: 51044
[startup+920.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11690 0 0 0 91986 39 0 0 25 0 1 0 545790425 52269056 11297 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11297 603 41 0 12720 0
vsize: 51044
[startup+930.174 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11691 0 0 0 92986 39 0 0 25 0 1 0 545790425 52269056 11298 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+940.179 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11691 0 0 0 93987 39 0 0 25 0 1 0 545790425 52269056 11298 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+950.185 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11691 0 0 0 94988 39 0 0 25 0 1 0 545790425 52269056 11298 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+960.186 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11691 0 0 0 95988 39 0 0 25 0 1 0 545790425 52269056 11298 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+970.186 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11691 0 0 0 96988 39 0 0 25 0 1 0 545790425 52269056 11298 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+980.186 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11691 0 0 0 97988 39 0 0 25 0 1 0 545790425 52269056 11298 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+990.186 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11692 0 0 0 98988 39 0 0 25 0 1 0 545790425 52269056 11299 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11299 603 41 0 12720 0
vsize: 51044
[startup+1000.19 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11692 0 0 0 99988 39 0 0 25 0 1 0 545790425 52269056 11299 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11299 603 41 0 12720 0
vsize: 51044
[startup+1010.19 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11693 0 0 0 100988 39 0 0 25 0 1 0 545790425 52269056 11300 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+1020.19 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11693 0 0 0 101989 39 0 0 25 0 1 0 545790425 52269056 11300 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+1030.19 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11693 0 0 0 102989 39 0 0 25 0 1 0 545790425 52269056 11300 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+1040.19 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11694 0 0 0 103989 39 0 0 25 0 1 0 545790425 52269056 11301 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1050.19 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11694 0 0 0 104989 39 0 0 25 0 1 0 545790425 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1060.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11694 0 0 0 105990 39 0 0 25 0 1 0 545790425 52269056 11301 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1070.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11694 0 0 0 106990 39 0 0 25 0 1 0 545790425 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1080.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 107990 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1090.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 108990 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1100.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 109991 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1110.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 110991 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1120.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 111991 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1130.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 112991 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1140.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11695 0 0 0 113991 39 0 0 25 0 1 0 545790425 52269056 11302 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1150.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11697 0 0 0 114991 39 0 0 25 0 1 0 545790425 52269056 11304 4294967295 134512640 134672761 3221224544 3221223716 134556604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11304 603 41 0 12720 0
vsize: 51044
[startup+1160.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11697 0 0 0 115991 40 0 0 25 0 1 0 545790425 52269056 11304 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11304 603 41 0 12720 0
vsize: 51044
[startup+1170.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11714 0 0 0 116991 40 0 0 25 0 1 0 545790425 52510720 11321 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11321 603 41 0 12779 0
vsize: 51280
[startup+1180.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11715 0 0 0 117991 40 0 0 25 0 1 0 545790425 52510720 11322 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1190.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11715 0 0 0 118991 40 0 0 25 0 1 0 545790425 52510720 11322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 27466
Raw data (stat): 27466 (minisat+) R 27465 23176 23175 0 -1 0 11715 0 0 0 119991 40 0 0 25 0 1 0 545790425 52510720 11322 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 27466
Raw data (stat): 27466 (minisat+) Z 27465 23176 23175 0 -1 12 11717 0 0 0 119991 42 0 0 25 0 1 0 545790425 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.22
CPU time (s): 1200.35
CPU user time (s): 1199.92
CPU system time (s): 0.426935
CPU usage (%): 100.01
Max. virtual memory (Kb): 51280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####