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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.14
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 21524

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-22 00:10:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13192 boxname=wulflinc25 idbench=1015 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  02b9fdfc96e8b88ab6df67318e21abbc  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-air05.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-air05.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-air05.opb
IDLAUNCH: 13192
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        717036 kB
Buffers:         15656 kB
Cached:         282080 kB
SwapCached:        716 kB
Active:          41088 kB
Inactive:       258604 kB
HighTotal:      131008 kB
HighFree:          448 kB
LowTotal:       903652 kB
LowFree:        716588 kB
SwapTotal:     2097892 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12284 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:30:33 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 13192 7 1200.36 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.86 0.97 0.91 2/54 17449
Raw data (stat): 17449 (runsolver) R 17448 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549304554 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99975 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11174 0 0 0 969 29 0 0 25 0 1 0 549304554 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.0004 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11183 0 0 0 1968 29 0 0 25 0 1 0 549304554 50323456 10790 4294967295 134512640 134672761 3221224544 3221223716 134556627 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 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11199 0 0 0 2968 30 0 0 25 0 1 0 549304554 50458624 10806 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12319 10806 603 41 0 12278 0
vsize: 49276
[startup+40.0005 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11231 0 0 0 3968 30 0 0 25 0 1 0 549304554 50614272 10838 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12357 10838 603 41 0 12316 0
vsize: 49428
[startup+50.0041 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11266 0 0 0 4967 30 0 0 25 0 1 0 549304554 50749440 10873 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12390 10873 603 41 0 12349 0
vsize: 49560
[startup+60.0037 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11294 0 0 0 5967 30 0 0 25 0 1 0 549304554 50884608 10901 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 10901 603 41 0 12382 0
vsize: 49692
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11322 0 0 0 6968 30 0 0 25 0 1 0 549304554 50884608 10929 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 10929 603 41 0 12382 0
vsize: 49692
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11349 0 0 0 7968 30 0 0 25 0 1 0 549304554 51019776 10956 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12456 10956 603 41 0 12415 0
vsize: 49824
[startup+90.0035 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11367 0 0 0 8968 31 0 0 25 0 1 0 549304554 51154944 10974 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12489 10974 603 41 0 12448 0
vsize: 49956
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11394 0 0 0 9967 31 0 0 25 0 1 0 549304554 51314688 11001 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12528 11001 603 41 0 12487 0
vsize: 50112
[startup+110.009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11423 0 0 0 10968 31 0 0 25 0 1 0 549304554 51314688 11030 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12528 11030 603 41 0 12487 0
vsize: 50112
[startup+120.018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11450 0 0 0 11969 31 0 0 25 0 1 0 549304554 51449856 11057 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12561 11057 603 41 0 12520 0
vsize: 50244
[startup+130.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11461 0 0 0 12969 31 0 0 25 0 1 0 549304554 51449856 11068 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12561 11068 603 41 0 12520 0
vsize: 50244
[startup+140.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11481 0 0 0 13969 31 0 0 25 0 1 0 549304554 51585024 11088 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11088 603 41 0 12553 0
vsize: 50376
[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11490 0 0 0 14970 31 0 0 25 0 1 0 549304554 51585024 11097 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11097 603 41 0 12553 0
vsize: 50376
[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11510 0 0 0 15970 31 0 0 25 0 1 0 549304554 51720192 11117 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11117 603 41 0 12586 0
vsize: 50508
[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11526 0 0 0 16970 31 0 0 25 0 1 0 549304554 51720192 11133 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12627 11133 603 41 0 12586 0
vsize: 50508
[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11544 0 0 0 17969 31 0 0 25 0 1 0 549304554 51855360 11151 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 11151 603 41 0 12619 0
vsize: 50640
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11554 0 0 0 18970 31 0 0 25 0 1 0 549304554 51855360 11161 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 11161 603 41 0 12619 0
vsize: 50640
[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11568 0 0 0 19970 32 0 0 25 0 1 0 549304554 51990528 11175 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11175 603 41 0 12652 0
vsize: 50772
[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11581 0 0 0 20970 32 0 0 25 0 1 0 549304554 51990528 11188 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11188 603 41 0 12652 0
vsize: 50772
[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11591 0 0 0 21971 32 0 0 25 0 1 0 549304554 51990528 11198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11198 603 41 0 12652 0
vsize: 50772
[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11600 0 0 0 22971 32 0 0 25 0 1 0 549304554 51990528 11207 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11207 603 41 0 12652 0
vsize: 50772
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11606 0 0 0 23971 32 0 0 25 0 1 0 549304554 52125696 11213 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11213 603 41 0 12685 0
vsize: 50904
[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11607 0 0 0 24971 32 0 0 25 0 1 0 549304554 52125696 11214 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11214 603 41 0 12685 0
vsize: 50904
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11609 0 0 0 25971 32 0 0 25 0 1 0 549304554 52125696 11216 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11216 603 41 0 12685 0
vsize: 50904
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11614 0 0 0 26971 32 0 0 25 0 1 0 549304554 52125696 11221 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11221 603 41 0 12685 0
vsize: 50904
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11618 0 0 0 27972 32 0 0 25 0 1 0 549304554 52125696 11225 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11225 603 41 0 12685 0
vsize: 50904
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11622 0 0 0 28972 32 0 0 25 0 1 0 549304554 52125696 11229 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11229 603 41 0 12685 0
vsize: 50904
[startup+300.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11627 0 0 0 29972 32 0 0 25 0 1 0 549304554 52125696 11234 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11234 603 41 0 12685 0
vsize: 50904
[startup+310.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11628 0 0 0 30974 32 0 0 25 0 1 0 549304554 52125696 11235 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11235 603 41 0 12685 0
vsize: 50904
[startup+320.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11630 0 0 0 31974 32 0 0 25 0 1 0 549304554 52125696 11237 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11237 603 41 0 12685 0
vsize: 50904
[startup+330.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11632 0 0 0 32974 32 0 0 25 0 1 0 549304554 52125696 11239 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11635 0 0 0 33974 32 0 0 25 0 1 0 549304554 52125696 11242 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11242 603 41 0 12685 0
vsize: 50904
[startup+350.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11638 0 0 0 34973 32 0 0 25 0 1 0 549304554 52125696 11245 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11245 603 41 0 12685 0
vsize: 50904
[startup+360.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11639 0 0 0 35974 32 0 0 25 0 1 0 549304554 52125696 11246 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11246 603 41 0 12685 0
vsize: 50904
[startup+370.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11640 0 0 0 36974 32 0 0 25 0 1 0 549304554 52125696 11247 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11247 603 41 0 12685 0
vsize: 50904
[startup+380.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11642 0 0 0 37975 32 0 0 25 0 1 0 549304554 52125696 11249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11249 603 41 0 12685 0
vsize: 50904
[startup+390.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11643 0 0 0 38975 32 0 0 25 0 1 0 549304554 52125696 11250 4294967295 134512640 134672761 3221224544 3221223708 134564508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11250 603 41 0 12685 0
vsize: 50904
[startup+400.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11644 0 0 0 39975 32 0 0 25 0 1 0 549304554 52125696 11251 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11251 603 41 0 12685 0
vsize: 50904
[startup+410.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11644 0 0 0 40975 32 0 0 25 0 1 0 549304554 52125696 11251 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11251 603 41 0 12685 0
vsize: 50904
[startup+420.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11650 0 0 0 41975 32 0 0 25 0 1 0 549304554 52269056 11257 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11257 603 41 0 12720 0
vsize: 51044
[startup+430.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11652 0 0 0 42975 32 0 0 25 0 1 0 549304554 52269056 11259 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11259 603 41 0 12720 0
vsize: 51044
[startup+440.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11652 0 0 0 43976 32 0 0 25 0 1 0 549304554 52269056 11259 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11259 603 41 0 12720 0
vsize: 51044
[startup+450.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11653 0 0 0 44976 32 0 0 25 0 1 0 549304554 52269056 11260 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+460.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11653 0 0 0 45976 32 0 0 25 0 1 0 549304554 52269056 11260 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11653 0 0 0 46976 32 0 0 25 0 1 0 549304554 52269056 11260 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+480.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11653 0 0 0 47976 32 0 0 25 0 1 0 549304554 52269056 11260 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11260 603 41 0 12720 0
vsize: 51044
[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11654 0 0 0 48976 32 0 0 25 0 1 0 549304554 52269056 11261 4294967295 134512640 134672761 3221224544 3221223696 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11654 0 0 0 49977 32 0 0 25 0 1 0 549304554 52269056 11261 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+510.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11654 0 0 0 50977 32 0 0 25 0 1 0 549304554 52269056 11261 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11654 0 0 0 51977 32 0 0 25 0 1 0 549304554 52269056 11261 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11654 0 0 0 52977 32 0 0 25 0 1 0 549304554 52269056 11261 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11654 0 0 0 53977 32 0 0 25 0 1 0 549304554 52269056 11261 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11261 603 41 0 12720 0
vsize: 51044
[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11655 0 0 0 54978 32 0 0 25 0 1 0 549304554 52269056 11262 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11262 603 41 0 12720 0
vsize: 51044
[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11656 0 0 0 55978 33 0 0 25 0 1 0 549304554 52269056 11263 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11656 0 0 0 56977 33 0 0 25 0 1 0 549304554 52269056 11263 4294967295 134512640 134672761 3221224544 3221223736 134556585 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11656 0 0 0 57977 33 0 0 25 0 1 0 549304554 52269056 11263 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11263 603 41 0 12720 0
vsize: 51044
[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11658 0 0 0 58977 33 0 0 25 0 1 0 549304554 52269056 11265 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11265 603 41 0 12720 0
vsize: 51044
[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11659 0 0 0 59977 33 0 0 25 0 1 0 549304554 52269056 11266 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11266 603 41 0 12720 0
vsize: 51044
[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11668 0 0 0 60977 33 0 0 25 0 1 0 549304554 52269056 11275 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11668 0 0 0 61977 33 0 0 25 0 1 0 549304554 52269056 11275 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11668 0 0 0 62977 34 0 0 25 0 1 0 549304554 52269056 11275 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11668 0 0 0 63977 34 0 0 25 0 1 0 549304554 52269056 11275 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11275 603 41 0 12720 0
vsize: 51044
[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11670 0 0 0 64978 34 0 0 25 0 1 0 549304554 52269056 11277 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11670 0 0 0 65978 34 0 0 25 0 1 0 549304554 52269056 11277 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11670 0 0 0 66978 34 0 0 25 0 1 0 549304554 52269056 11277 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11670 0 0 0 67978 34 0 0 25 0 1 0 549304554 52269056 11277 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11277 603 41 0 12720 0
vsize: 51044
[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11673 0 0 0 68978 34 0 0 25 0 1 0 549304554 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+700.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11673 0 0 0 69978 34 0 0 25 0 1 0 549304554 52269056 11280 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11673 0 0 0 70978 34 0 0 25 0 1 0 549304554 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11673 0 0 0 71979 34 0 0 25 0 1 0 549304554 52269056 11280 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+730.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11673 0 0 0 72979 34 0 0 25 0 1 0 549304554 52269056 11280 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11280 603 41 0 12720 0
vsize: 51044
[startup+740.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11674 0 0 0 73979 34 0 0 25 0 1 0 549304554 52269056 11281 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11281 603 41 0 12720 0
vsize: 51044
[startup+750.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11674 0 0 0 74979 34 0 0 25 0 1 0 549304554 52269056 11281 4294967295 134512640 134672761 3221224544 3221223716 134556609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11281 603 41 0 12720 0
vsize: 51044
[startup+760.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11676 0 0 0 75979 34 0 0 25 0 1 0 549304554 52269056 11283 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11283 603 41 0 12720 0
vsize: 51044
[startup+770.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11676 0 0 0 76979 34 0 0 25 0 1 0 549304554 52269056 11283 4294967295 134512640 134672761 3221224544 3221223712 134565029 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11678 0 0 0 77979 34 0 0 25 0 1 0 549304554 52269056 11285 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11285 603 41 0 12720 0
vsize: 51044
[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11679 0 0 0 78979 34 0 0 25 0 1 0 549304554 52269056 11286 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11286 603 41 0 12720 0
vsize: 51044
[startup+800.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11681 0 0 0 79979 34 0 0 25 0 1 0 549304554 52269056 11288 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11288 603 41 0 12720 0
vsize: 51044
[startup+810.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11682 0 0 0 80979 34 0 0 25 0 1 0 549304554 52269056 11289 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11289 603 41 0 12720 0
vsize: 51044
[startup+820.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11684 0 0 0 81980 34 0 0 25 0 1 0 549304554 52269056 11291 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11291 603 41 0 12720 0
vsize: 51044
[startup+830.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11685 0 0 0 82980 34 0 0 25 0 1 0 549304554 52269056 11292 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11292 603 41 0 12720 0
vsize: 51044
[startup+840.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11687 0 0 0 83980 35 0 0 25 0 1 0 549304554 52269056 11294 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11294 603 41 0 12720 0
vsize: 51044
[startup+850.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11687 0 0 0 84980 35 0 0 25 0 1 0 549304554 52269056 11294 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11294 603 41 0 12720 0
vsize: 51044
[startup+860.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11688 0 0 0 85980 35 0 0 25 0 1 0 549304554 52269056 11295 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11295 603 41 0 12720 0
vsize: 51044
[startup+870.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11689 0 0 0 86980 35 0 0 25 0 1 0 549304554 52269056 11296 4294967295 134512640 134672761 3221224544 3221223716 134556658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11296 603 41 0 12720 0
vsize: 51044
[startup+880.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11689 0 0 0 87981 35 0 0 25 0 1 0 549304554 52269056 11296 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11296 603 41 0 12720 0
vsize: 51044
[startup+890.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11690 0 0 0 88981 35 0 0 25 0 1 0 549304554 52269056 11297 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11297 603 41 0 12720 0
vsize: 51044
[startup+900.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11691 0 0 0 89981 35 0 0 25 0 1 0 549304554 52269056 11298 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+910.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11691 0 0 0 90981 35 0 0 25 0 1 0 549304554 52269056 11298 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+920.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11691 0 0 0 91981 35 0 0 25 0 1 0 549304554 52269056 11298 4294967295 134512640 134672761 3221224544 3221223692 134565968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+930.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11691 0 0 0 92981 35 0 0 25 0 1 0 549304554 52269056 11298 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+940.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11691 0 0 0 93982 35 0 0 25 0 1 0 549304554 52269056 11298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+950.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11691 0 0 0 94982 35 0 0 25 0 1 0 549304554 52269056 11298 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11298 603 41 0 12720 0
vsize: 51044
[startup+960.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11692 0 0 0 95982 35 0 0 25 0 1 0 549304554 52269056 11299 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11299 603 41 0 12720 0
vsize: 51044
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11692 0 0 0 96982 35 0 0 25 0 1 0 549304554 52269056 11299 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11299 603 41 0 12720 0
vsize: 51044
[startup+980.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11693 0 0 0 97982 35 0 0 25 0 1 0 549304554 52269056 11300 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+990.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11693 0 0 0 98982 35 0 0 25 0 1 0 549304554 52269056 11300 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11693 0 0 0 99983 35 0 0 25 0 1 0 549304554 52269056 11300 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11300 603 41 0 12720 0
vsize: 51044
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11694 0 0 0 100983 35 0 0 25 0 1 0 549304554 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11694 0 0 0 101983 35 0 0 25 0 1 0 549304554 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1030.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11694 0 0 0 102994 35 0 0 25 0 1 0 549304554 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1040.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11694 0 0 0 103994 35 0 0 25 0 1 0 549304554 52269056 11301 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11301 603 41 0 12720 0
vsize: 51044
[startup+1050.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11695 0 0 0 104994 35 0 0 25 0 1 0 549304554 52269056 11302 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1060.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11695 0 0 0 105994 35 0 0 25 0 1 0 549304554 52269056 11302 4294967295 134512640 134672761 3221224544 3221223716 134556609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1070.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11695 0 0 0 106994 35 0 0 25 0 1 0 549304554 52269056 11302 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1080.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11695 0 0 0 107995 35 0 0 25 0 1 0 549304554 52269056 11302 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1090.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11695 0 0 0 108995 35 0 0 25 0 1 0 549304554 52269056 11302 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1100.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11695 0 0 0 109995 35 0 0 25 0 1 0 549304554 52269056 11302 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11302 603 41 0 12720 0
vsize: 51044
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11697 0 0 0 110995 35 0 0 25 0 1 0 549304554 52269056 11304 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11304 603 41 0 12720 0
vsize: 51044
[startup+1120.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11697 0 0 0 111994 35 0 0 25 0 1 0 549304554 52269056 11304 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11697 0 0 0 112993 35 0 0 25 0 1 0 549304554 52269056 11304 4294967295 134512640 134672761 3221224544 3221223696 134565143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 11304 603 41 0 12720 0
vsize: 51044
[startup+1140.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 113993 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1150.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 114994 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1160.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 115994 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1170.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 116994 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 117995 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 118996 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17449
Raw data (stat): 17449 (minisat+) R 17448 28099 28098 0 -1 0 11715 0 0 0 119998 35 0 0 25 0 1 0 549304554 52510720 11322 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12820 11322 603 41 0 12779 0
vsize: 51280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.56 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 17449
Raw data (stat): 17449 (minisat+) Z 17448 28099 28098 0 -1 12 11717 0 0 0 119998 37 0 0 22 0 1 0 549304554 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.56
CPU time (s): 1200.36
CPU user time (s): 1199.99
CPU system time (s): 0.378942
CPU usage (%): 99.9837
Max. virtual memory (Kb): 51280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####