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/miplib/normalized-mps-v2-13-7-air05.opb
MD5SUM	a48e4d8c244906df694603c81ee602a6
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.13
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 15796

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 05:47:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16663 boxname=wulflinc20 idbench=1282 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a48e4d8c244906df694603c81ee602a6  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air05.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air05.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air05.opb
IDLAUNCH: 16663
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        864996 kB
Buffers:          8768 kB
Cached:         137052 kB
SwapCached:        516 kB
Active:          32000 kB
Inactive:       115792 kB
HighTotal:      131008 kB
HighFree:        32648 kB
LowTotal:       903652 kB
LowFree:        832348 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            16136 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:07:59 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 16663 7 1200.27 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.81 0.91 0.90 2/54 29317
Raw data (stat): 29317 (runsolver) R 29316 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542677135 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.0008 s]
Raw data (loadavg): 0.84 0.91 0.90 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11174 0 0 0 966 32 0 0 25 0 1 0 542677135 50323456 10781 4294967295 134512640 134672761 3221224544 3221223716 134556685 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.001 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11183 0 0 0 1966 32 0 0 25 0 1 0 542677135 50323456 10790 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.002 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11199 0 0 0 2966 32 0 0 25 0 1 0 542677135 50458624 10806 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12319 10806 603 41 0 12278 0
vsize: 49276
[startup+40.0017 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11228 0 0 0 3966 32 0 0 25 0 1 0 542677135 50614272 10835 4294967295 134512640 134672761 3221224544 3221223740 134556584 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.0012 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11266 0 0 0 4966 32 0 0 25 0 1 0 542677135 50749440 10873 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12390 10873 603 41 0 12349 0
vsize: 49560
[startup+60.0013 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11293 0 0 0 5966 32 0 0 25 0 1 0 542677135 50884608 10900 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12423 10900 603 41 0 12382 0
vsize: 49692
[startup+70.0019 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11320 0 0 0 6966 33 0 0 25 0 1 0 542677135 50884608 10927 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.0023 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11347 0 0 0 7966 33 0 0 25 0 1 0 542677135 51019776 10954 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12456 10954 603 41 0 12415 0
vsize: 49824
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11366 0 0 0 8966 33 0 0 25 0 1 0 542677135 51154944 10973 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12489 10973 603 41 0 12448 0
vsize: 49956
[startup+100.002 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11393 0 0 0 9966 33 0 0 25 0 1 0 542677135 51314688 11000 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.003 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11423 0 0 0 10966 33 0 0 25 0 1 0 542677135 51314688 11030 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 11030 603 41 0 12487 0
vsize: 50112
[startup+120.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11449 0 0 0 11966 33 0 0 25 0 1 0 542677135 51449856 11056 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12561 11056 603 41 0 12520 0
vsize: 50244
[startup+130.003 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11461 0 0 0 12966 33 0 0 25 0 1 0 542677135 51449856 11068 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11481 0 0 0 13965 34 0 0 25 0 1 0 542677135 51585024 11088 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12594 11088 603 41 0 12553 0
vsize: 50376
[startup+150.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11490 0 0 0 14965 34 0 0 25 0 1 0 542677135 51585024 11097 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12594 11097 603 41 0 12553 0
vsize: 50376
[startup+160.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11507 0 0 0 15966 34 0 0 25 0 1 0 542677135 51720192 11114 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12627 11114 603 41 0 12586 0
vsize: 50508
[startup+170.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11522 0 0 0 16966 34 0 0 25 0 1 0 542677135 51720192 11129 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12627 11129 603 41 0 12586 0
vsize: 50508
[startup+180.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11543 0 0 0 17965 35 0 0 25 0 1 0 542677135 51855360 11150 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12660 11150 603 41 0 12619 0
vsize: 50640
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11553 0 0 0 18965 35 0 0 25 0 1 0 542677135 51855360 11160 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12660 11160 603 41 0 12619 0
vsize: 50640
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11567 0 0 0 19965 35 0 0 25 0 1 0 542677135 51855360 11174 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12660 11174 603 41 0 12619 0
vsize: 50640
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11580 0 0 0 20965 35 0 0 25 0 1 0 542677135 51990528 11187 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11187 603 41 0 12652 0
vsize: 50772
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11590 0 0 0 21965 35 0 0 25 0 1 0 542677135 51990528 11197 4294967295 134512640 134672761 3221224544 3221223752 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11197 603 41 0 12652 0
vsize: 50772
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11599 0 0 0 22966 35 0 0 25 0 1 0 542677135 51990528 11206 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11206 603 41 0 12652 0
vsize: 50772
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11605 0 0 0 23966 35 0 0 25 0 1 0 542677135 51990528 11212 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11212 603 41 0 12652 0
vsize: 50772
[startup+250.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11607 0 0 0 24966 35 0 0 25 0 1 0 542677135 52125696 11214 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11214 603 41 0 12685 0
vsize: 50904
[startup+260.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11609 0 0 0 25966 35 0 0 25 0 1 0 542677135 52125696 11216 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11216 603 41 0 12685 0
vsize: 50904
[startup+270.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11613 0 0 0 26966 35 0 0 25 0 1 0 542677135 52125696 11220 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11220 603 41 0 12685 0
vsize: 50904
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11617 0 0 0 27966 35 0 0 25 0 1 0 542677135 52125696 11224 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11224 603 41 0 12685 0
vsize: 50904
[startup+290.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11622 0 0 0 28967 35 0 0 25 0 1 0 542677135 52125696 11229 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11229 603 41 0 12685 0
vsize: 50904
[startup+300.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11627 0 0 0 29967 35 0 0 25 0 1 0 542677135 52125696 11234 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11234 603 41 0 12685 0
vsize: 50904
[startup+310.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11628 0 0 0 30967 35 0 0 25 0 1 0 542677135 52125696 11235 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11235 603 41 0 12685 0
vsize: 50904
[startup+320.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11630 0 0 0 31967 35 0 0 25 0 1 0 542677135 52125696 11237 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11237 603 41 0 12685 0
vsize: 50904
[startup+330.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11632 0 0 0 32967 35 0 0 25 0 1 0 542677135 52125696 11239 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11239 603 41 0 12685 0
vsize: 50904
[startup+340.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11634 0 0 0 33967 35 0 0 25 0 1 0 542677135 52125696 11241 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11241 603 41 0 12685 0
vsize: 50904
[startup+350.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11638 0 0 0 34968 35 0 0 25 0 1 0 542677135 52125696 11245 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11245 603 41 0 12685 0
vsize: 50904
[startup+360.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11638 0 0 0 35968 35 0 0 25 0 1 0 542677135 52125696 11245 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11640 0 0 0 36968 35 0 0 25 0 1 0 542677135 52125696 11247 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11247 603 41 0 12685 0
vsize: 50904
[startup+380.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11641 0 0 0 37968 35 0 0 25 0 1 0 542677135 52125696 11248 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11248 603 41 0 12685 0
vsize: 50904
[startup+390.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11643 0 0 0 38968 35 0 0 25 0 1 0 542677135 52125696 11250 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11250 603 41 0 12685 0
vsize: 50904
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11644 0 0 0 39969 35 0 0 25 0 1 0 542677135 52125696 11251 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11251 603 41 0 12685 0
vsize: 50904
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11644 0 0 0 40969 35 0 0 25 0 1 0 542677135 52125696 11251 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11645 0 0 0 41969 35 0 0 25 0 1 0 542677135 52125696 11252 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12726 11252 603 41 0 12685 0
vsize: 50904
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11650 0 0 0 42969 35 0 0 25 0 1 0 542677135 52269056 11257 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11652 0 0 0 43969 35 0 0 25 0 1 0 542677135 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+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11652 0 0 0 44969 35 0 0 25 0 1 0 542677135 52269056 11259 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11653 0 0 0 45969 35 0 0 25 0 1 0 542677135 52269056 11260 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11653 0 0 0 46970 35 0 0 25 0 1 0 542677135 52269056 11260 4294967295 134512640 134672761 3221224544 3221223668 134566118 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11653 0 0 0 47970 35 0 0 25 0 1 0 542677135 52269056 11260 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11654 0 0 0 48970 35 0 0 25 0 1 0 542677135 52269056 11261 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11654 0 0 0 49970 35 0 0 25 0 1 0 542677135 52269056 11261 4294967295 134512640 134672761 3221224544 3221223716 134556596 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11654 0 0 0 50970 35 0 0 25 0 1 0 542677135 52269056 11261 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11654 0 0 0 51970 35 0 0 25 0 1 0 542677135 52269056 11261 4294967295 134512640 134672761 3221224544 3221223696 134565092 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11654 0 0 0 52970 35 0 0 25 0 1 0 542677135 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+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11654 0 0 0 53971 35 0 0 25 0 1 0 542677135 52269056 11261 4294967295 134512640 134672761 3221224544 3221223696 134565098 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11655 0 0 0 54971 35 0 0 25 0 1 0 542677135 52269056 11262 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11262 603 41 0 12720 0
vsize: 51044
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11656 0 0 0 55971 35 0 0 25 0 1 0 542677135 52269056 11263 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11263 603 41 0 12720 0
vsize: 51044
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11656 0 0 0 56970 36 0 0 25 0 1 0 542677135 52269056 11263 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11656 0 0 0 57970 36 0 0 25 0 1 0 542677135 52269056 11263 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11658 0 0 0 58970 36 0 0 25 0 1 0 542677135 52269056 11265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11265 603 41 0 12720 0
vsize: 51044
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11658 0 0 0 59970 36 0 0 25 0 1 0 542677135 52269056 11265 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11265 603 41 0 12720 0
vsize: 51044
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11659 0 0 0 60970 36 0 0 25 0 1 0 542677135 52269056 11266 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11266 603 41 0 12720 0
vsize: 51044
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11668 0 0 0 61970 36 0 0 25 0 1 0 542677135 52269056 11275 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+630.003 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11668 0 0 0 62971 36 0 0 25 0 1 0 542677135 52269056 11275 4294967295 134512640 134672761 3221224544 3221223792 134562140 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.004 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11668 0 0 0 63971 36 0 0 25 0 1 0 542677135 52269056 11275 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.004 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11670 0 0 0 64971 36 0 0 25 0 1 0 542677135 52269056 11277 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+660.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11670 0 0 0 65971 36 0 0 25 0 1 0 542677135 52269056 11277 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+670.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11670 0 0 0 66971 36 0 0 25 0 1 0 542677135 52269056 11277 4294967295 134512640 134672761 3221224544 3221223760 134561985 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.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11670 0 0 0 67971 36 0 0 25 0 1 0 542677135 52269056 11277 4294967295 134512640 134672761 3221224544 3221223668 134566043 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.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11670 0 0 0 68971 36 0 0 25 0 1 0 542677135 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+700.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11673 0 0 0 69972 36 0 0 25 0 1 0 542677135 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+710.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11673 0 0 0 70972 36 0 0 25 0 1 0 542677135 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29317
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11673 0 0 0 71972 36 0 0 25 0 1 0 542677135 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.003 s]
Raw data (loadavg): 1.01 0.99 0.91 3/57 29353
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11673 0 0 0 72971 37 0 0 25 0 1 0 542677135 52269056 11280 4294967295 134512640 134672761 3221224544 3221223792 134562132 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.088 s]
Raw data (loadavg): 1.09 1.00 0.92 2/58 29362
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11674 0 0 0 73980 37 0 0 25 0 1 0 542677135 52269056 11281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11281 603 41 0 12720 0
vsize: 51044
[startup+750.089 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 29370
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11674 0 0 0 74979 37 0 0 25 0 1 0 542677135 52269056 11281 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11281 603 41 0 12720 0
vsize: 51044
[startup+760.09 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 29370
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11676 0 0 0 75980 37 0 0 25 0 1 0 542677135 52269056 11283 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+770.089 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 29370
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11676 0 0 0 76979 37 0 0 25 0 1 0 542677135 52269056 11283 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+780.095 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 29370
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11676 0 0 0 77978 37 0 0 25 0 1 0 542677135 52269056 11283 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+790.096 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 29370
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11679 0 0 0 78978 38 0 0 25 0 1 0 542677135 52269056 11286 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11286 603 41 0 12720 0
vsize: 51044
[startup+800.095 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29370
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11681 0 0 0 79978 38 0 0 25 0 1 0 542677135 52269056 11288 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11288 603 41 0 12720 0
vsize: 51044
[startup+810.096 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11682 0 0 0 80978 38 0 0 25 0 1 0 542677135 52269056 11289 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11289 603 41 0 12720 0
vsize: 51044
[startup+820.096 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11682 0 0 0 81979 38 0 0 25 0 1 0 542677135 52269056 11289 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11289 603 41 0 12720 0
vsize: 51044
[startup+830.095 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11684 0 0 0 82978 38 0 0 25 0 1 0 542677135 52269056 11291 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11291 603 41 0 12720 0
vsize: 51044
[startup+840.095 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11687 0 0 0 83978 38 0 0 25 0 1 0 542677135 52269056 11294 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11294 603 41 0 12720 0
vsize: 51044
[startup+850.096 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11687 0 0 0 84978 38 0 0 25 0 1 0 542677135 52269056 11294 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11294 603 41 0 12720 0
vsize: 51044
[startup+860.096 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11688 0 0 0 85979 38 0 0 25 0 1 0 542677135 52269056 11295 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11295 603 41 0 12720 0
vsize: 51044
[startup+870.096 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11688 0 0 0 86979 38 0 0 25 0 1 0 542677135 52269056 11295 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11295 603 41 0 12720 0
vsize: 51044
[startup+880.095 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11689 0 0 0 87979 38 0 0 25 0 1 0 542677135 52269056 11296 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11296 603 41 0 12720 0
vsize: 51044
[startup+890.096 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11689 0 0 0 88979 38 0 0 25 0 1 0 542677135 52269056 11296 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11296 603 41 0 12720 0
vsize: 51044
[startup+900.096 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11690 0 0 0 89979 38 0 0 25 0 1 0 542677135 52269056 11297 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11297 603 41 0 12720 0
vsize: 51044
[startup+910.096 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11691 0 0 0 90979 38 0 0 25 0 1 0 542677135 52269056 11298 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+920.097 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11691 0 0 0 91980 38 0 0 25 0 1 0 542677135 52269056 11298 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+930.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11691 0 0 0 92980 38 0 0 25 0 1 0 542677135 52269056 11298 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11691 0 0 0 93980 38 0 0 25 0 1 0 542677135 52269056 11298 4294967295 134512640 134672761 3221224544 3221223668 134566082 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11691 0 0 0 94981 38 0 0 25 0 1 0 542677135 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+960.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11691 0 0 0 95981 38 0 0 25 0 1 0 542677135 52269056 11298 4294967295 134512640 134672761 3221224544 3221223680 134560654 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11692 0 0 0 96981 38 0 0 25 0 1 0 542677135 52269056 11299 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11299 603 41 0 12720 0
vsize: 51044
[startup+980.099 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11692 0 0 0 97981 38 0 0 25 0 1 0 542677135 52269056 11299 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11299 603 41 0 12720 0
vsize: 51044
[startup+990.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11693 0 0 0 98981 38 0 0 25 0 1 0 542677135 52269056 11300 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11693 0 0 0 99981 38 0 0 25 0 1 0 542677135 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+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11693 0 0 0 100982 38 0 0 25 0 1 0 542677135 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+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11694 0 0 0 101982 38 0 0 25 0 1 0 542677135 52269056 11301 4294967295 134512640 134672761 3221224544 3221223708 134564518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11694 0 0 0 102982 38 0 0 25 0 1 0 542677135 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11694 0 0 0 103982 38 0 0 25 0 1 0 542677135 52269056 11301 4294967295 134512640 134672761 3221224544 3221223696 134565045 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29372
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 104982 38 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 105982 39 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 106982 39 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 107982 39 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 108983 39 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 109983 39 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11695 0 0 0 110983 39 0 0 25 0 1 0 542677135 52269056 11302 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11697 0 0 0 111983 39 0 0 25 0 1 0 542677135 52269056 11304 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11304 603 41 0 12720 0
vsize: 51044
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11697 0 0 0 112983 39 0 0 25 0 1 0 542677135 52269056 11304 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12761 11304 603 41 0 12720 0
vsize: 51044
[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11714 0 0 0 113983 39 0 0 25 0 1 0 542677135 52510720 11321 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11321 603 41 0 12779 0
vsize: 51280
[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11715 0 0 0 114983 39 0 0 25 0 1 0 542677135 52510720 11322 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11715 0 0 0 115983 39 0 0 25 0 1 0 542677135 52510720 11322 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11715 0 0 0 116984 39 0 0 25 0 1 0 542677135 52510720 11322 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11715 0 0 0 117984 39 0 0 25 0 1 0 542677135 52510720 11322 4294967295 134512640 134672761 3221224544 3221223716 134556671 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11715 0 0 0 118984 39 0 0 25 0 1 0 542677135 52510720 11322 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29374
Raw data (stat): 29317 (minisat+) R 29316 27565 27564 0 -1 0 11715 0 0 0 119985 39 0 0 25 0 1 0 542677135 52510720 11322 4294967295 134512640 134672761 3221224544 3221223712 134561018 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.13 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 29374
Raw data (stat): 29317 (minisat+) Z 29316 27565 27564 0 -1 12 11717 0 0 0 119985 41 0 0 25 0 1 0 542677135 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.13
CPU time (s): 1200.27
CPU user time (s): 1199.85
CPU system time (s): 0.415936
CPU usage (%): 100.012
Max. virtual memory (Kb): 51280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####