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/miplib2003/normalized-mps-v2-20-10-air05.opb
MD5SUM	a0fff131fa124ee4d61d9b3bf266a4ba
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	29628
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 22006

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-22 01:50:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12451 boxname=wulflinc18 idbench=958 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a0fff131fa124ee4d61d9b3bf266a4ba  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-air05.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-air05.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-air05.opb
IDLAUNCH: 12451
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        245660 kB
Buffers:         22044 kB
Cached:         743160 kB
SwapCached:        748 kB
Active:          82444 kB
Inactive:       684664 kB
HighTotal:      131008 kB
HighFree:          924 kB
LowTotal:       903652 kB
LowFree:        244736 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            16108 kB
Committed_AS:    63812 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:10:38 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 12451 7 1200.21 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: 448   maxlim: 230   bits: 8/8
c ---[ 846]---> Adder-cost: 254   maxlim: 127   bits: 8/7
c ---[ 844]---> Adder-cost: 202   maxlim: 115   bits: 7/7
c ---[ 842]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 840]---> Adder-cost: 274   maxlim: 139   bits: 8/8
c ---[ 838]---> Adder-cost: 220   maxlim: 152   bits: 8/8
c ---[ 836]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 834]---> Adder-cost: 98   maxlim: 59   bits: 6/6
c ---[ 832]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[ 830]---> Adder-cost: 184   maxlim: 106   bits: 7/7
c ---[ 828]---> Adder-cost: 188   maxlim: 96   bits: 7/7
c ---[ 826]---> Adder-cost: 648   maxlim: 332   bits: 9/9
c ---[ 822]---> Adder-cost: 156   maxlim: 95   bits: 7/7
c ---[ 820]---> Adder-cost: 400   maxlim: 203   bits: 8/8
c ---[ 818]---> Adder-cost: 414   maxlim: 230   bits: 8/8
c ---[ 816]---> Adder-cost: 450   maxlim: 233   bits: 8/8
c ---[ 814]---> Adder-cost: 392   maxlim: 219   bits: 8/8
c ---[ 812]---> Adder-cost: 254   maxlim: 127   bits: 8/7
c ---[ 810]---> Adder-cost: 162   maxlim: 92   bits: 7/7
c ---[ 808]---> Adder-cost: 406   maxlim: 208   bits: 8/8
c ---[ 806]---> Adder-cost: 392   maxlim: 211   bits: 8/8
c ---[ 804]---> Adder-cost: 618   maxlim: 357   bits: 9/9
c ---[ 802]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 800]---> Adder-cost: 124   maxlim: 65   bits: 7/7
c ---[ 798]---> Adder-cost: 304   maxlim: 155   bits: 8/8
c ---[ 796]---> Adder-cost: 182   maxlim: 155   bits: 8/8
c ---[ 794]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 786]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 784]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 782]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[ 780]---> Adder-cost: 254   maxlim: 127   bits: 8/7
c ---[ 778]---> Adder-cost: 216   maxlim: 144   bits: 8/8
c ---[ 776]---> Adder-cost: 442   maxlim: 223   bits: 8/8
c ---[ 774]---> Adder-cost: 370   maxlim: 216   bits: 8/8
c ---[ 772]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 770]---> Adder-cost: 98   maxlim: 54   bits: 6/6
c ---[ 768]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 766]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[ 764]---> Adder-cost: 122   maxlim: 68   bits: 7/7
c ---[ 762]---> Adder-cost: 158   maxlim: 88   bits: 7/7
c ---[ 760]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[ 758]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 756]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 754]---> Adder-cost: 6   maxlim: 6   bits: 3/3
c ---[ 752]---> Adder-cost: 20   maxlim: 14   bits: 4/4
c ---[ 750]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 748]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[ 746]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 744]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 742]---> Adder-cost: 94   maxlim: 59   bits: 6/6
c ---[ 740]---> Adder-cost: 512   maxlim: 263   bits: 9/9
c ---[ 738]---> Adder-cost: 126   maxlim: 67   bits: 7/7
c ---[ 736]---> Adder-cost: 434   maxlim: 255   bits: 9/8
c ---[ 732]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 730]---> Adder-cost: 182   maxlim: 98   bits: 7/7
c ---[ 728]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[ 726]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 724]---> Adder-cost: 312   maxlim: 163   bits: 8/8
c ---[ 722]---> Adder-cost: 456   maxlim: 243   bits: 8/8
c ---[ 720]---> Adder-cost: 266   maxlim: 137   bits: 8/8
c ---[ 718]---> Adder-cost: 270   maxlim: 153   bits: 8/8
c ---[ 716]---> Adder-cost: 84   maxlim: 52   bits: 6/6
c ---[ 714]---> Adder-cost: 318   maxlim: 182   bits: 8/8
c ---[ 712]---> Adder-cost: 232   maxlim: 162   bits: 8/8
c ---[ 710]---> Adder-cost: 172   maxlim: 93   bits: 7/7
c ---[ 708]---> Adder-cost: 300   maxlim: 158   bits: 8/8
c ---[ 706]---> Adder-cost: 274   maxlim: 146   bits: 8/8
c ---[ 704]---> Adder-cost: 380   maxlim: 192   bits: 8/8
c ---[ 702]---> Adder-cost: 288   maxlim: 181   bits: 8/8
c ---[ 700]---> Adder-cost: 190   maxlim: 105   bits: 7/7
c ---[ 698]---> Adder-cost: 158   maxlim: 106   bits: 7/7
c ---[ 696]---> Adder-cost: 254   maxlim: 133   bits: 8/8
c ---[ 694]---> Adder-cost: 316   maxlim: 166   bits: 8/8
c ---[ 692]---> Adder-cost: 160   maxlim: 99   bits: 7/7
c ---[ 690]---> Adder-cost: 154   maxlim: 96   bits: 7/7
c ---[ 688]---> Adder-cost: 166   maxlim: 100   bits: 7/7
c ---[ 686]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[ 684]---> Adder-cost: 64   maxlim: 35   bits: 6/6
c ---[ 682]---> Adder-cost: 528   maxlim: 274   bits: 9/9
c ---[ 680]---> Adder-cost: 492   maxlim: 286   bits: 9/9
c ---[ 678]---> Adder-cost: 162   maxlim: 86   bits: 7/7
c ---[ 676]---> Adder-cost: 128   maxlim: 90   bits: 7/7
c ---[ 674]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[ 672]---> Adder-cost: 152   maxlim: 82   bits: 7/7
c ---[ 670]---> Adder-cost: 114   maxlim: 70   bits: 7/7
c ---[ 668]---> Adder-cost: 558   maxlim: 283   bits: 9/9
c ---[ 666]---> Adder-cost: 408   maxlim: 291   bits: 9/9
c ---[ 664]---> Adder-cost: 254   maxlim: 128   bits: 8/8
c ---[ 662]---> Adder-cost: 178   maxlim: 113   bits: 7/7
c ---[ 660]---> Adder-cost: 186   maxlim: 96   bits: 7/7
c ---[ 658]---> Adder-cost: 222   maxlim: 119   bits: 7/7
c ---[ 656]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 654]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 652]---> Adder-cost: 62   maxlim: 39   bits: 6/6
c ---[ 650]---> Adder-cost: 330   maxlim: 176   bits: 8/8
c ---[ 648]---> Adder-cost: 508   maxlim: 261   bits: 9/9
c ---[ 646]---> Adder-cost: 462   maxlim: 268   bits: 9/9
c ---[ 644]---> Adder-cost: 332   maxlim: 171   bits: 8/8
c ---[ 642]---> Adder-cost: 232   maxlim: 127   bits: 8/7
c ---[ 640]---> Adder-cost: 286   maxlim: 147   bits: 8/8
c ---[ 638]---> Adder-cost: 290   maxlim: 165   bits: 8/8
c ---[ 636]---> Adder-cost: 418   maxlim: 216   bits: 8/8
c ---[ 634]---> Adder-cost: 336   maxlim: 211   bits: 8/8
c ---[ 632]---> Adder-cost: 392   maxlim: 210   bits: 8/8
c ---[ 630]---> Adder-cost: 338   maxlim: 206   bits: 8/8
c ---[ 628]---> Adder-cost: 156   maxlim: 86   bits: 7/7
c ---[ 626]---> Adder-cost: 308   maxlim: 186   bits: 8/8
c ---[ 624]---> Adder-cost: 462   maxlim: 247   bits: 8/8
c ---[ 622]---> Adder-cost: 254   maxlim: 154   bits: 8/8
c ---[ 620]---> Adder-cost: 218   maxlim: 116   bits: 7/7
c ---[ 618]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 616]---> Adder-cost: 78   maxlim: 45   bits: 6/6
c ---[ 614]---> Adder-cost: 700   maxlim: 373   bits: 9/9
c ---[ 612]---> Adder-cost: 516   maxlim: 283   bits: 9/9
c ---[ 610]---> Adder-cost: 696   maxlim: 403   bits: 9/9
c ---[ 608]---> Adder-cost: 644   maxlim: 337   bits: 9/9
c ---[ 606]---> Adder-cost: 516   maxlim: 293   bits: 9/9
c ---[ 604]---> Adder-cost: 172   maxlim: 91   bits: 7/7
c ---[ 602]---> Adder-cost: 428   maxlim: 276   bits: 9/9
c ---[ 598]---> Adder-cost: 314   maxlim: 161   bits: 8/8
c ---[ 596]---> Adder-cost: 360   maxlim: 189   bits: 8/8
c ---[ 594]---> Adder-cost: 358   maxlim: 202   bits: 8/8
c ---[ 592]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[ 590]---> Adder-cost: 78   maxlim: 51   bits: 6/6
c ---[ 586]---> Adder-cost: 630   maxlim: 322   bits: 9/9
c ---[ 584]---> Adder-cost: 160   maxlim: 89   bits: 7/7
c ---[ 582]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 580]---> Adder-cost: 154   maxlim: 85   bits: 7/7
c ---[ 578]---> Adder-cost: 120   maxlim: 100   bits: 7/7
c ---[ 574]---> Adder-cost: 266   maxlim: 135   bits: 8/8
c ---[ 572]---> Adder-cost: 218   maxlim: 116   bits: 7/7
c ---[ 570]---> Adder-cost: 158   maxlim: 95   bits: 7/7
c ---[ 568]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 566]---> Adder-cost: 72   maxlim: 52   bits: 6/6
c ---[ 564]---> Adder-cost: 116   maxlim: 66   bits: 7/7
c ---[ 562]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 560]---> Adder-cost: 0   maxlim: 42   bits: 6/6
c ---[ 558]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[ 556]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 554]---> Adder-cost: 110   maxlim: 61   bits: 6/6
c ---[ 552]---> Adder-cost: 388   maxlim: 203   bits: 8/8
c ---[ 550]---> Adder-cost: 156   maxlim: 107   bits: 7/7
c ---[ 548]---> Adder-cost: 110   maxlim: 75   bits: 7/7
c ---[ 546]---> Adder-cost: 160   maxlim: 108   bits: 7/7
c ---[ 544]---> Adder-cost: 520   maxlim: 267   bits: 9/9
c ---[ 542]---> Adder-cost: 480   maxlim: 275   bits: 9/9
c ---[ 540]---> Adder-cost: 310   maxlim: 162   bits: 8/8
c ---[ 538]---> Adder-cost: 62   maxlim: 44   bits: 6/6
c ---[ 536]---> Adder-cost: 246   maxlim: 151   bits: 8/8
c ---[ 534]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 532]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 530]---> Adder-cost: 20   maxlim: 14   bits: 4/4
c ---[ 528]---> Adder-cost: 26   maxlim: 17   bits: 5/5
c ---[ 526]---> Adder-cost: 216   maxlim: 113   bits: 7/7
c ---[ 524]---> Adder-cost: 128   maxlim: 111   bits: 7/7
c ---[ 522]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 520]---> Adder-cost: 76   maxlim: 70   bits: 7/7
c ---[ 518]---> Adder-cost: 108   maxlim: 69   bits: 7/7
c ---[ 516]---> Adder-cost: 56   maxlim: 38   bits: 6/6
c ---[ 514]---> Adder-cost: 158   maxlim: 89   bits: 7/7
c ---[ 512]---> Adder-cost: 146   maxlim: 78   bits: 7/7
c ---[ 510]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[ 508]---> Adder-cost: 344   maxlim: 182   bits: 8/8
c ---[ 506]---> Adder-cost: 250   maxlim: 154   bits: 8/8
c ---[ 504]---> Adder-cost: 236   maxlim: 123   bits: 7/7
c ---[ 502]---> Adder-cost: 180   maxlim: 114   bits: 7/7
c ---[ 496]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 494]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 492]---> Adder-cost: 122   maxlim: 75   bits: 7/7
c ---[ 490]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 488]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 486]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 484]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 482]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 480]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 478]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 476]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[ 474]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 472]---> Adder-cost: 206   maxlim: 107   bits: 7/7
c ---[ 470]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 468]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 466]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[ 464]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 462]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 460]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 458]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 456]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 454]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[ 452]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[ 450]---> Adder-cost: 148   maxlim: 106   bits: 7/7
c ---[ 448]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[ 446]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[ 444]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[ 442]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 440]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[ 438]---> Adder-cost: 48   maxlim: 27   bits: 5/5
c ---[ 436]---> Adder-cost: 128   maxlim: 70   bits: 7/7
c ---[ 434]---> Adder-cost: 334   maxlim: 171   bits: 8/8
c ---[ 432]---> Adder-cost: 202   maxlim: 108   bits: 7/7
c ---[ 430]---> Adder-cost: 156   maxlim: 83   bits: 7/7
c ---[ 428]---> Adder-cost: 192   maxlim: 119   bits: 7/7
c ---[ 426]---> Adder-cost: 116   maxlim: 89   bits: 7/7
c ---[ 424]---> Adder-cost: 326   maxlim: 183   bits: 8/8
c ---[ 420]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 418]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 416]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 414]---> Adder-cost: 34   maxlim: 26   bits: 5/5
c ---[ 412]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 410]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 408]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[ 406]---> Adder-cost: 170   maxlim: 90   bits: 7/7
c ---[ 404]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[ 402]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[ 400]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 398]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 396]---> Adder-cost: 334   maxlim: 171   bits: 8/8
c ---[ 394]---> Adder-cost: 182   maxlim: 97   bits: 7/7
c ---[ 392]---> Adder-cost: 146   maxlim: 103   bits: 7/7
c ---[ 390]---> Adder-cost: 514   maxlim: 271   bits: 9/9
c ---[ 388]---> Adder-cost: 508   maxlim: 272   bits: 9/9
c ---[ 386]---> Adder-cost: 426   maxlim: 219   bits: 8/8
c ---[ 384]---> Adder-cost: 320   maxlim: 188   bits: 8/8
c ---[ 382]---> Adder-cost: 82   maxlim: 47   bits: 6/6
c ---[ 380]---> Adder-cost: 228   maxlim: 122   bits: 7/7
c ---[ 378]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[ 376]---> Adder-cost: 134   maxlim: 70   bits: 7/7
c ---[ 374]---> Adder-cost: 262   maxlim: 138   bits: 8/8
c ---[ 372]---> Adder-cost: 166   maxlim: 87   bits: 7/7
c ---[ 370]---> Adder-cost: 142   maxlim: 79   bits: 7/7
c ---[ 368]---> Adder-cost: 138   maxlim: 72   bits: 7/7
c ---[ 366]---> Adder-cost: 108   maxlim: 73   bits: 7/7
c ---[ 364]---> Adder-cost: 154   maxlim: 84   bits: 7/7
c ---[ 362]---> Adder-cost: 122   maxlim: 77   bits: 7/7
c ---[ 360]---> Adder-cost: 0   maxlim: 47   bits: 6/6
c ---[ 358]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[ 356]---> Adder-cost: 108   maxlim: 73   bits: 7/7
c ---[ 354]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 352]---> Adder-cost: 54   maxlim: 75   bits: 7/7
c ---[ 350]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[ 348]---> Adder-cost: 90   maxlim: 79   bits: 7/7
c ---[ 346]---> Adder-cost: 210   maxlim: 113   bits: 7/7
c ---[ 344]---> Adder-cost: 212   maxlim: 120   bits: 7/7
c ---[ 342]---> Adder-cost: 444   maxlim: 228   bits: 8/8
c ---[ 340]---> Adder-cost: 410   maxlim: 234   bits: 8/8
c ---[ 338]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 336]---> Adder-cost: 202   maxlim: 104   bits: 7/7
c ---[ 334]---> Adder-cost: 198   maxlim: 113   bits: 7/7
c ---[ 332]---> Adder-cost: 144   maxlim: 114   bits: 7/7
c ---[ 330]---> Adder-cost: 146   maxlim: 79   bits: 7/7
c ---[ 328]---> Adder-cost: 298   maxlim: 157   bits: 8/8
c ---[ 326]---> Adder-cost: 178   maxlim: 113   bits: 7/7
c ---[ 324]---> Adder-cost: 154   maxlim: 100   bits: 7/7
c ---[ 322]---> Adder-cost: 344   maxlim: 176   bits: 8/8
c ---[ 320]---> Adder-cost: 324   maxlim: 181   bits: 8/8
c ---[ 318]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 316]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[ 314]---> Adder-cost: 104   maxlim: 56   bits: 6/6
c ---[ 312]---> Adder-cost: 640   maxlim: 329   bits: 9/9
c ---[ 310]---> Adder-cost: 476   maxlim: 322   bits: 9/9
c ---[ 308]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 306]---> Adder-cost: 184   maxlim: 113   bits: 7/7
c ---[ 304]---> Adder-cost: 334   maxlim: 172   bits: 8/8
c ---[ 302]---> Adder-cost: 500   maxlim: 262   bits: 9/9
c ---[ 300]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 298]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 296]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 294]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[ 292]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[ 290]---> Adder-cost: 192   maxlim: 106   bits: 7/7
c ---[ 286]---> Adder-cost: 276   maxlim: 142   bits: 8/8
c ---[ 284]---> Adder-cost: 478   maxlim: 252   bits: 8/8
c ---[ 282]---> Adder-cost: 316   maxlim: 166   bits: 8/8
c ---[ 280]---> Adder-cost: 214   maxlim: 127   bits: 8/7
c ---[ 278]---> Adder-cost: 270   maxlim: 159   bits: 8/8
c ---[ 276]---> Adder-cost: 268   maxlim: 157   bits: 8/8
c ---[ 274]---> Adder-cost: 348   maxlim: 185   bits: 8/8
c ---[ 272]---> Adder-cost: 0   maxlim: 26   bits: 5/5
c ---[ 270]---> Adder-cost: 542   maxlim: 301   bits: 9/9
c ---[ 268]---> Adder-cost: 274   maxlim: 140   bits: 8/8
c ---[ 266]---> Adder-cost: 204   maxlim: 129   bits: 8/8
c ---[ 264]---> Adder-cost: 190   maxlim: 101   bits: 7/7
c ---[ 262]---> Adder-cost: 324   maxlim: 171   bits: 8/8
c ---[ 260]---> Adder-cost: 294   maxlim: 155   bits: 8/8
c ---[ 258]---> Adder-cost: 224   maxlim: 173   bits: 8/8
c ---[ 256]---> Adder-cost: 448   maxlim: 229   bits: 8/8
c ---[ 254]---> Adder-cost: 400   maxlim: 220   bits: 8/8
c ---[ 252]---> Adder-cost: 288   maxlim: 150   bits: 8/8
c ---[ 250]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 248]---> Adder-cost: 244   maxlim: 136   bits: 8/8
c ---[ 246]---> Adder-cost: 360   maxlim: 188   bits: 8/8
c ---[ 244]---> Adder-cost: 340   maxlim: 181   bits: 8/8
c ---[ 242]---> Adder-cost: 338   maxlim: 186   bits: 8/8
c ---[ 240]---> Adder-cost: 392   maxlim: 221   bits: 8/8
c ---[ 238]---> Adder-cost: 276   maxlim: 147   bits: 8/8
c ---[ 236]---> Adder-cost: 400   maxlim: 209   bits: 8/8
c ---[ 234]---> Adder-cost: 278   maxlim: 147   bits: 8/8
c ---[ 232]---> Adder-cost: 164   maxlim: 90   bits: 7/7
c ---[ 230]---> Adder-cost: 116   maxlim: 75   bits: 7/7
c ---[ 228]---> Adder-cost: 48   maxlim: 30   bits: 5/5
c ---[ 226]---> Adder-cost: 134   maxlim: 72   bits: 7/7
c ---[ 224]---> Adder-cost: 118   maxlim: 71   bits: 7/7
c ---[ 222]---> Adder-cost: 316   maxlim: 169   bits: 8/8
c ---[ 220]---> Adder-cost: 206   maxlim: 169   bits: 8/8
c ---[ 218]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[ 216]---> Adder-cost: 74   maxlim: 53   bits: 6/6
c ---[ 214]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 212]---> Adder-cost: 12   maxlim: 8   bits: 4/4
c ---[ 210]---> Adder-cost: 206   maxlim: 107   bits: 7/7
c ---[ 208]---> Adder-cost: 184   maxlim: 128   bits: 8/8
c ---[ 206]---> Adder-cost: 104   maxlim: 56   bits: 6/6
c ---[ 204]---> Adder-cost: 308   maxlim: 165   bits: 8/8
c ---[ 202]---> Adder-cost: 288   maxlim: 171   bits: 8/8
c ---[ 200]---> Adder-cost: 288   maxlim: 149   bits: 8/8
c ---[ 198]---> Adder-cost: 236   maxlim: 127   bits: 8/7
c ---[ 196]---> Adder-cost: 440   maxlim: 232   bits: 8/8
c ---[ 194]---> Adder-cost: 360   maxlim: 191   bits: 8/8
c ---[ 192]---> Adder-cost: 260   maxlim: 162   bits: 8/8
c ---[ 190]---> Adder-cost: 204   maxlim: 148   bits: 8/8
c ---[ 188]---> Adder-cost: 166   maxlim: 113   bits: 7/7
c ---[ 186]---> Adder-cost: 242   maxlim: 133   bits: 8/8
c ---[ 184]---> Adder-cost: 204   maxlim: 106   bits: 7/7
c ---[ 182]---> Adder-cost: 164   maxlim: 88   bits: 7/7
c ---[ 180]---> Adder-cost: 558   maxlim: 293   bits: 9/9
c ---[ 178]---> Adder-cost: 492   maxlim: 274   bits: 9/9
c ---[ 176]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 174]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 172]---> Adder-cost: 174   maxlim: 93   bits: 7/7
c ---[ 170]---> Adder-cost: 208   maxlim: 117   bits: 7/7
c ---[ 168]---> Adder-cost: 168   maxlim: 88   bits: 7/7
c ---[ 166]---> Adder-cost: 92   maxlim: 57   bits: 6/6
c ---[ 164]---> Adder-cost: 100   maxlim: 59   bits: 6/6
c ---[ 162]---> Adder-cost: 112   maxlim: 73   bits: 7/7
c ---[ 160]---> Adder-cost: 72   maxlim: 42   bits: 6/6
c ---[ 158]---> Adder-cost: 156   maxlim: 84   bits: 7/7
c ---[ 156]---> Adder-cost: 194   maxlim: 117   bits: 7/7
c ---[ 154]---> Adder-cost: 394   maxlim: 225   bits: 8/8
c ---[ 152]---> Adder-cost: 346   maxlim: 175   bits: 8/8
c ---[ 150]---> Adder-cost: 260   maxlim: 159   bits: 8/8
c ---[ 148]---> Adder-cost: 472   maxlim: 251   bits: 8/8
c ---[ 146]---> Adder-cost: 250   maxlim: 138   bits: 8/8
c ---[ 144]---> Adder-cost: 264   maxlim: 141   bits: 8/8
c ---[ 142]---> Adder-cost: 250   maxlim: 128   bits: 8/8
c ---[ 140]---> Adder-cost: 144   maxlim: 107   bits: 7/7
c ---[ 138]---> Adder-cost: 202   maxlim: 104   bits: 7/7
c ---[ 136]---> Adder-cost: 158   maxlim: 120   bits: 7/7
c ---[ 134]---> Adder-cost: 194   maxlim: 102   bits: 7/7
c ---[ 132]---> Adder-cost: 224   maxlim: 119   bits: 7/7
c ---[ 130]---> Adder-cost: 166   maxlim: 92   bits: 7/7
c ---[ 128]---> Adder-cost: 150   maxlim: 94   bits: 7/7
c ---[ 126]---> Adder-cost: 204   maxlim: 107   bits: 7/7
c ---[ 124]---> Adder-cost: 184   maxlim: 105   bits: 7/7
c ---[ 122]---> Adder-cost: 178   maxlim: 95   bits: 7/7
c ---[ 120]---> Adder-cost: 184   maxlim: 126   bits: 7/7
c ---[ 118]---> Adder-cost: 402   maxlim: 226   bits: 8/8
c ---[ 116]---> Adder-cost: 264   maxlim: 143   bits: 8/8
c ---[ 114]---> Adder-cost: 230   maxlim: 170   bits: 8/8
c ---[ 112]---> Adder-cost: 394   maxlim: 217   bits: 8/8
c ---[ 110]---> Adder-cost: 172   maxlim: 110   bits: 7/7
c ---[ 108]---> Adder-cost: 144   maxlim: 80   bits: 7/7
c ---[ 106]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 104]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[ 100]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[  98]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  94]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[  92]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[  90]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[  88]---> Adder-cost: 274   maxlim: 141   bits: 8/8
c ---[  86]---> Adder-cost: 202   maxlim: 118   bits: 7/7
c ---[  84]---> Adder-cost: 266   maxlim: 143   bits: 8/8
c ---[  82]---> Adder-cost: 344   maxlim: 194   bits: 8/8
c ---[  80]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[  76]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[  74]---> Adder-cost: 176   maxlim: 109   bits: 7/7
c ---[  72]---> Adder-cost: 260   maxlim: 136   bits: 8/8
c ---[  70]---> Adder-cost: 266   maxlim: 151   bits: 8/8
c ---[  68]---> Adder-cost: 278   maxlim: 155   bits: 8/8
c ---[  66]---> Adder-cost: 220   maxlim: 127   bits: 8/7
c ---[  64]---> Adder-cost: 448   maxlim: 245   bits: 8/8
c ---[  62]---> Adder-cost: 182   maxlim: 122   bits: 7/7
c ---[  60]---> Adder-cost: 234   maxlim: 158   bits: 8/8
c ---[  58]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[  56]---> Adder-cost: 140   maxlim: 81   bits: 7/7
c ---[  54]---> Adder-cost: 308   maxlim: 159   bits: 8/8
c ---[  52]---> Adder-cost: 272   maxlim: 163   bits: 8/8
c ---[  50]---> Adder-cost: 276   maxlim: 149   bits: 8/8
c ---[  48]---> Adder-cost: 220   maxlim: 140   bits: 8/8
c ---[  46]---> Adder-cost: 354   maxlim: 191   bits: 8/8
c ---[  44]---> Adder-cost: 442   maxlim: 238   bits: 8/8
c ---[  42]---> Adder-cost: 346   maxlim: 228   bits: 8/8
c ---[  40]---> Adder-cost: 272   maxlim: 145   bits: 8/8
c ---[  38]---> Adder-cost: 262   maxlim: 144   bits: 8/8
c ---[  36]---> Adder-cost: 212   maxlim: 112   bits: 7/7
c ---[  34]---> Adder-cost: 146   maxlim: 117   bits: 7/7
c ---[  32]---> Adder-cost: 490   maxlim: 282   bits: 9/9
c ---[  30]---> Adder-cost: 444   maxlim: 259   bits: 9/9
c ---[  28]---> Adder-cost: 470   maxlim: 267   bits: 9/9
c ---[  26]---> Adder-cost: 636   maxlim: 344   bits: 9/9
c ---[  24]---> Adder-cost: 460   maxlim: 357   bits: 9/9
c ---[  22]---> Adder-cost: 508   maxlim: 301   bits: 9/9
c ---[  20]---> Adder-cost: 384   maxlim: 214   bits: 8/8
c ---[  18]---> Adder-cost: 312   maxlim: 188   bits: 8/8
c ---[  16]---> Adder-cost: 682   maxlim: 366   bits: 9/9
c ---[  14]---> Adder-cost: 584   maxlim: 370   bits: 9/9
c ---[  12]---> Adder-cost: 696   maxlim: 378   bits: 9/9
c ---[  10]---> Adder-cost: 450   maxlim: 262   bits: 9/9
c ---[   8]---> Adder-cost: 484   maxlim: 296   bits: 9/9
c ---[   6]---> Adder-cost: 586   maxlim: 347   bits: 9/9
c ---[   4]---> Adder-cost: 134   maxlim: 80   bits: 7/7
c ---[   2]---> Adder-cost: 192   maxlim: 99   bits: 7/7
c ---[   0]---> Adder-cost: 212   maxlim: 122   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 |       101 |  603358  2149022 |  221479      17       56     3.3 |  6.368 % |
c |       251 |  602874  2147316 |  243627     108      396     3.7 |  6.452 % |
c |       476 |  601716  2143298 |  267990     203      835     4.1 |  6.650 % |
c |       814 |  599505  2135589 |  294789     302     1233     4.1 |  7.033 % |
c |      1321 |  596299  2124459 |  324268     478     1984     4.2 |  7.597 % |
c |      2080 |  591642  2108208 |  356694     714     2968     4.2 |  8.395 % |
c |      3219 |  587540  2093912 |  392364    1368     6023     4.4 |  9.096 % |
c |      4927 |  581884  2074070 |  431600    2381    10896     4.6 | 10.051 % |
c |      7489 |  575365  2051207 |  474760    4126    21175     5.1 | 11.155 % |
c |     11333 |  566442  2019868 |  522237    6879    36653     5.3 | 12.654 % |
c |     17099 |  556367  1984291 |  574460   11355    61375     5.4 | 14.382 % |
c |     25748 |  532652  1900460 |  631906   16758    98470     5.9 | 18.368 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.88 0.87 2/55 14423
Raw data (stat): 14423 (runsolver) R 14422 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549885872 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.0004 s]
Raw data (loadavg): 0.88 0.89 0.87 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11173 0 0 0 971 28 0 0 25 0 1 0 549885872 50348032 10776 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12292 10776 603 41 0 12251 0
vsize: 49168
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.89 0.87 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11178 0 0 0 1971 28 0 0 25 0 1 0 549885872 50348032 10781 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12292 10781 603 41 0 12251 0
vsize: 49168
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.89 0.87 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11219 0 0 0 2971 28 0 0 25 0 1 0 549885872 50483200 10822 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12325 10822 603 41 0 12284 0
vsize: 49300
[startup+40.0032 s]
Raw data (loadavg): 0.92 0.89 0.87 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11242 0 0 0 3971 28 0 0 25 0 1 0 549885872 50618368 10845 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12358 10845 603 41 0 12317 0
vsize: 49432
[startup+50.0044 s]
Raw data (loadavg): 0.93 0.90 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11276 0 0 0 4971 28 0 0 25 0 1 0 549885872 50753536 10879 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12391 10879 603 41 0 12350 0
vsize: 49564
[startup+60.0043 s]
Raw data (loadavg): 0.94 0.90 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11314 0 0 0 5971 29 0 0 25 0 1 0 549885872 50888704 10917 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12424 10917 603 41 0 12383 0
vsize: 49696
[startup+70.0052 s]
Raw data (loadavg): 0.95 0.90 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11344 0 0 0 6970 29 0 0 25 0 1 0 549885872 51023872 10947 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 10947 603 41 0 12416 0
vsize: 49828
[startup+80.0063 s]
Raw data (loadavg): 0.96 0.91 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11373 0 0 0 7970 29 0 0 25 0 1 0 549885872 51159040 10976 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12490 10976 603 41 0 12449 0
vsize: 49960
[startup+90.0061 s]
Raw data (loadavg): 0.96 0.91 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11400 0 0 0 8969 30 0 0 25 0 1 0 549885872 51294208 11003 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12523 11003 603 41 0 12482 0
vsize: 50092
[startup+100.007 s]
Raw data (loadavg): 0.97 0.91 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11420 0 0 0 9969 30 0 0 25 0 1 0 549885872 51294208 11023 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12523 11023 603 41 0 12482 0
vsize: 50092
[startup+110.007 s]
Raw data (loadavg): 0.97 0.91 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11439 0 0 0 10969 30 0 0 25 0 1 0 549885872 51429376 11042 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11042 603 41 0 12515 0
vsize: 50224
[startup+120.008 s]
Raw data (loadavg): 0.98 0.92 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11454 0 0 0 11969 30 0 0 25 0 1 0 549885872 51429376 11057 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12556 11057 603 41 0 12515 0
vsize: 50224
[startup+130.008 s]
Raw data (loadavg): 0.98 0.92 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11476 0 0 0 12969 30 0 0 25 0 1 0 549885872 51564544 11079 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12589 11079 603 41 0 12548 0
vsize: 50356
[startup+140.008 s]
Raw data (loadavg): 0.98 0.92 0.88 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11492 0 0 0 13969 30 0 0 25 0 1 0 549885872 51564544 11095 4294967295 134512640 134672761 3221224544 3221223760 134557630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12589 11095 603 41 0 12548 0
vsize: 50356
[startup+150.009 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11506 0 0 0 14969 31 0 0 25 0 1 0 549885872 51699712 11109 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12622 11109 603 41 0 12581 0
vsize: 50488
[startup+160.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11520 0 0 0 15969 31 0 0 25 0 1 0 549885872 51699712 11123 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12622 11123 603 41 0 12581 0
vsize: 50488
[startup+170.008 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11527 0 0 0 16969 31 0 0 25 0 1 0 549885872 51834880 11130 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12655 11130 603 41 0 12614 0
vsize: 50620
[startup+180.008 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11539 0 0 0 17969 31 0 0 25 0 1 0 549885872 51834880 11142 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12655 11142 603 41 0 12614 0
vsize: 50620
[startup+190.008 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11554 0 0 0 18969 31 0 0 25 0 1 0 549885872 51834880 11157 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12655 11157 603 41 0 12614 0
vsize: 50620
[startup+200.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11564 0 0 0 19969 32 0 0 25 0 1 0 549885872 51834880 11167 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12655 11167 603 41 0 12614 0
vsize: 50620
[startup+210.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11570 0 0 0 20969 32 0 0 25 0 1 0 549885872 51970048 11173 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 11173 603 41 0 12647 0
vsize: 50752
[startup+220.01 s]
Raw data (loadavg): 0.99 0.94 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11582 0 0 0 21969 32 0 0 25 0 1 0 549885872 51970048 11185 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 11185 603 41 0 12647 0
vsize: 50752
[startup+230.01 s]
Raw data (loadavg): 0.99 0.94 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11591 0 0 0 22969 32 0 0 25 0 1 0 549885872 51970048 11194 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 11194 603 41 0 12647 0
vsize: 50752
[startup+240.01 s]
Raw data (loadavg): 0.99 0.94 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11597 0 0 0 23969 32 0 0 25 0 1 0 549885872 51970048 11200 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 11200 603 41 0 12647 0
vsize: 50752
[startup+250.011 s]
Raw data (loadavg): 0.99 0.94 0.89 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11604 0 0 0 24969 32 0 0 25 0 1 0 549885872 51970048 11207 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 11207 603 41 0 12647 0
vsize: 50752
[startup+260.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11607 0 0 0 25969 32 0 0 25 0 1 0 549885872 52105216 11210 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11210 603 41 0 12680 0
vsize: 50884
[startup+270.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11610 0 0 0 26970 32 0 0 25 0 1 0 549885872 52105216 11213 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11213 603 41 0 12680 0
vsize: 50884
[startup+280.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11611 0 0 0 27970 32 0 0 25 0 1 0 549885872 52105216 11214 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11214 603 41 0 12680 0
vsize: 50884
[startup+290.011 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14423
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11615 0 0 0 28970 32 0 0 25 0 1 0 549885872 52105216 11218 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11218 603 41 0 12680 0
vsize: 50884
[startup+300.011 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11615 0 0 0 29970 32 0 0 25 0 1 0 549885872 52105216 11218 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11218 603 41 0 12680 0
vsize: 50884
[startup+310.011 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11620 0 0 0 30970 32 0 0 25 0 1 0 549885872 52105216 11223 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11223 603 41 0 12680 0
vsize: 50884
[startup+320.012 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11621 0 0 0 31970 32 0 0 25 0 1 0 549885872 52105216 11224 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11224 603 41 0 12680 0
vsize: 50884
[startup+330.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11624 0 0 0 32970 32 0 0 25 0 1 0 549885872 52105216 11227 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11227 603 41 0 12680 0
vsize: 50884
[startup+340.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11625 0 0 0 33970 33 0 0 25 0 1 0 549885872 52105216 11228 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11228 603 41 0 12680 0
vsize: 50884
[startup+350.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11627 0 0 0 34970 33 0 0 25 0 1 0 549885872 52105216 11230 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11230 603 41 0 12680 0
vsize: 50884
[startup+360.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11631 0 0 0 35971 33 0 0 25 0 1 0 549885872 52105216 11234 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11234 603 41 0 12680 0
vsize: 50884
[startup+370.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11635 0 0 0 36971 33 0 0 25 0 1 0 549885872 52105216 11238 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11238 603 41 0 12680 0
vsize: 50884
[startup+380.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11636 0 0 0 37971 33 0 0 25 0 1 0 549885872 52105216 11239 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11239 603 41 0 12680 0
vsize: 50884
[startup+390.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11636 0 0 0 38971 33 0 0 25 0 1 0 549885872 52105216 11239 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11239 603 41 0 12680 0
vsize: 50884
[startup+400.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11637 0 0 0 39971 33 0 0 25 0 1 0 549885872 52105216 11240 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11240 603 41 0 12680 0
vsize: 50884
[startup+410.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11639 0 0 0 40971 33 0 0 25 0 1 0 549885872 52105216 11242 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11242 603 41 0 12680 0
vsize: 50884
[startup+420.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11641 0 0 0 41972 33 0 0 25 0 1 0 549885872 52105216 11244 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11244 603 41 0 12680 0
vsize: 50884
[startup+430.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11642 0 0 0 42972 33 0 0 25 0 1 0 549885872 52105216 11245 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11245 603 41 0 12680 0
vsize: 50884
[startup+440.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11642 0 0 0 43972 33 0 0 25 0 1 0 549885872 52105216 11245 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11245 603 41 0 12680 0
vsize: 50884
[startup+450.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11648 0 0 0 44972 33 0 0 25 0 1 0 549885872 52105216 11251 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+460.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11648 0 0 0 45972 33 0 0 25 0 1 0 549885872 52105216 11251 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+470.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11648 0 0 0 46972 33 0 0 25 0 1 0 549885872 52105216 11251 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+480.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11648 0 0 0 47972 33 0 0 25 0 1 0 549885872 52105216 11251 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+490.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11649 0 0 0 48972 33 0 0 25 0 1 0 549885872 52105216 11252 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11252 603 41 0 12680 0
vsize: 50884
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11649 0 0 0 49973 33 0 0 25 0 1 0 549885872 52105216 11252 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11252 603 41 0 12680 0
vsize: 50884
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11651 0 0 0 50973 33 0 0 25 0 1 0 549885872 52105216 11254 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11254 603 41 0 12680 0
vsize: 50884
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11653 0 0 0 51973 33 0 0 25 0 1 0 549885872 52105216 11256 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11256 603 41 0 12680 0
vsize: 50884
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11653 0 0 0 52973 33 0 0 25 0 1 0 549885872 52105216 11256 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11256 603 41 0 12680 0
vsize: 50884
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11655 0 0 0 53973 33 0 0 25 0 1 0 549885872 52105216 11258 4294967295 134512640 134672761 3221224544 3221223712 134564767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11258 603 41 0 12680 0
vsize: 50884
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11657 0 0 0 54973 33 0 0 25 0 1 0 549885872 52105216 11260 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11260 603 41 0 12680 0
vsize: 50884
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14425
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11658 0 0 0 55973 33 0 0 25 0 1 0 549885872 52105216 11261 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11261 603 41 0 12680 0
vsize: 50884
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14464
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11659 0 0 0 56974 33 0 0 25 0 1 0 549885872 52105216 11262 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11262 603 41 0 12680 0
vsize: 50884
[startup+580.023 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 14478
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11660 0 0 0 57974 34 0 0 25 0 1 0 549885872 52105216 11263 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11263 603 41 0 12680 0
vsize: 50884
[startup+590.023 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 14478
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11660 0 0 0 58973 34 0 0 25 0 1 0 549885872 52105216 11263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11263 603 41 0 12680 0
vsize: 50884
[startup+600.024 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 14480
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11664 0 0 0 59973 35 0 0 25 0 1 0 549885872 52105216 11267 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11267 603 41 0 12680 0
vsize: 50884
[startup+610.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 14480
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11664 0 0 0 60973 35 0 0 25 0 1 0 549885872 52105216 11267 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11267 603 41 0 12680 0
vsize: 50884
[startup+620.025 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 14480
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11664 0 0 0 61973 35 0 0 25 0 1 0 549885872 52105216 11267 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12721 11267 603 41 0 12680 0
vsize: 50884
[startup+630.026 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 14480
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11665 0 0 0 62973 36 0 0 25 0 1 0 549885872 52240384 11268 4294967295 134512640 134672761 3221224544 3221223712 134564726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11268 603 41 0 12713 0
vsize: 51016
[startup+640.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11666 0 0 0 63972 36 0 0 25 0 1 0 549885872 52240384 11269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11269 603 41 0 12713 0
vsize: 51016
[startup+650.026 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11676 0 0 0 64972 37 0 0 25 0 1 0 549885872 52240384 11279 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+660.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11676 0 0 0 65972 37 0 0 25 0 1 0 549885872 52240384 11279 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+670.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11676 0 0 0 66971 37 0 0 25 0 1 0 549885872 52240384 11279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+680.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11676 0 0 0 67971 38 0 0 25 0 1 0 549885872 52240384 11279 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+690.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11681 0 0 0 68971 38 0 0 25 0 1 0 549885872 52240384 11284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11284 603 41 0 12713 0
vsize: 51016
[startup+700.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11681 0 0 0 69970 39 0 0 25 0 1 0 549885872 52240384 11284 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11284 603 41 0 12713 0
vsize: 51016
[startup+710.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11683 0 0 0 70971 39 0 0 25 0 1 0 549885872 52240384 11286 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11286 603 41 0 12713 0
vsize: 51016
[startup+720.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11683 0 0 0 71971 39 0 0 25 0 1 0 549885872 52240384 11286 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11286 603 41 0 12713 0
vsize: 51016
[startup+730.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11683 0 0 0 72971 39 0 0 25 0 1 0 549885872 52240384 11286 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11286 603 41 0 12713 0
vsize: 51016
[startup+740.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11683 0 0 0 73971 39 0 0 25 0 1 0 549885872 52240384 11286 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11286 603 41 0 12713 0
vsize: 51016
[startup+750.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11684 0 0 0 74971 39 0 0 25 0 1 0 549885872 52240384 11287 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11287 603 41 0 12713 0
vsize: 51016
[startup+760.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11684 0 0 0 75972 39 0 0 25 0 1 0 549885872 52240384 11287 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11287 603 41 0 12713 0
vsize: 51016
[startup+770.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11684 0 0 0 76972 39 0 0 25 0 1 0 549885872 52240384 11287 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11287 603 41 0 12713 0
vsize: 51016
[startup+780.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11684 0 0 0 77972 39 0 0 25 0 1 0 549885872 52240384 11287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11287 603 41 0 12713 0
vsize: 51016
[startup+790.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11685 0 0 0 78972 39 0 0 25 0 1 0 549885872 52240384 11288 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11288 603 41 0 12713 0
vsize: 51016
[startup+800.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11685 0 0 0 79972 39 0 0 25 0 1 0 549885872 52240384 11288 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12754 11288 603 41 0 12713 0
vsize: 51016
[startup+810.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11685 0 0 0 80971 40 0 0 25 0 1 0 549885872 52240384 11288 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11288 603 41 0 12713 0
vsize: 51016
[startup+820.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11685 0 0 0 81972 40 0 0 25 0 1 0 549885872 52240384 11288 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11288 603 41 0 12713 0
vsize: 51016
[startup+830.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11685 0 0 0 82972 40 0 0 25 0 1 0 549885872 52240384 11288 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11288 603 41 0 12713 0
vsize: 51016
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11685 0 0 0 83972 40 0 0 25 0 1 0 549885872 52240384 11288 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11288 603 41 0 12713 0
vsize: 51016
[startup+850.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11686 0 0 0 84972 40 0 0 25 0 1 0 549885872 52240384 11289 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11289 603 41 0 12713 0
vsize: 51016
[startup+860.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11686 0 0 0 85972 40 0 0 25 0 1 0 549885872 52240384 11289 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11289 603 41 0 12713 0
vsize: 51016
[startup+870.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11686 0 0 0 86972 40 0 0 25 0 1 0 549885872 52240384 11289 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11289 603 41 0 12713 0
vsize: 51016
[startup+880.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11686 0 0 0 87972 40 0 0 25 0 1 0 549885872 52240384 11289 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11289 603 41 0 12713 0
vsize: 51016
[startup+890.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14482
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11687 0 0 0 88972 40 0 0 25 0 1 0 549885872 52240384 11290 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11290 603 41 0 12713 0
vsize: 51016
[startup+900.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14484
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11687 0 0 0 89972 40 0 0 25 0 1 0 549885872 52240384 11290 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11290 603 41 0 12713 0
vsize: 51016
[startup+910.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14484
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 90973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+920.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 91973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+930.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 92973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+940.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 93973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+950.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 94973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+960.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 95973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223708 134564531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+970.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11688 0 0 0 96973 40 0 0 25 0 1 0 549885872 52240384 11291 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11291 603 41 0 12713 0
vsize: 51016
[startup+980.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 97974 40 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+990.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 98974 40 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 99974 40 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 100974 40 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 101974 40 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 102974 41 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 103974 41 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11689 0 0 0 104975 41 0 0 25 0 1 0 549885872 52240384 11292 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11292 603 41 0 12713 0
vsize: 51016
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11691 0 0 0 105975 41 0 0 25 0 1 0 549885872 52240384 11294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11294 603 41 0 12713 0
vsize: 51016
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11691 0 0 0 106975 41 0 0 25 0 1 0 549885872 52240384 11294 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11294 603 41 0 12713 0
vsize: 51016
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11691 0 0 0 107975 41 0 0 25 0 1 0 549885872 52240384 11294 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11294 603 41 0 12713 0
vsize: 51016
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11691 0 0 0 108975 41 0 0 25 0 1 0 549885872 52240384 11294 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11294 603 41 0 12713 0
vsize: 51016
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11691 0 0 0 109976 41 0 0 25 0 1 0 549885872 52240384 11294 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11294 603 41 0 12713 0
vsize: 51016
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11691 0 0 0 110976 41 0 0 25 0 1 0 549885872 52240384 11294 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11294 603 41 0 12713 0
vsize: 51016
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11708 0 0 0 111976 41 0 0 25 0 1 0 549885872 52441088 11311 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11311 603 41 0 12762 0
vsize: 51212
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11708 0 0 0 112976 41 0 0 25 0 1 0 549885872 52441088 11311 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11311 603 41 0 12762 0
vsize: 51212
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11708 0 0 0 113976 41 0 0 25 0 1 0 549885872 52441088 11311 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11311 603 41 0 12762 0
vsize: 51212
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11709 0 0 0 114976 41 0 0 25 0 1 0 549885872 52441088 11312 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11312 603 41 0 12762 0
vsize: 51212
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11709 0 0 0 115976 41 0 0 25 0 1 0 549885872 52441088 11312 4294967295 134512640 134672761 3221224544 3221223668 134566103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12803 11312 603 41 0 12762 0
vsize: 51212
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11709 0 0 0 116975 41 0 0 25 0 1 0 549885872 52441088 11312 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11312 603 41 0 12762 0
vsize: 51212
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11709 0 0 0 117975 41 0 0 25 0 1 0 549885872 52441088 11312 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11312 603 41 0 12762 0
vsize: 51212
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14486
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11709 0 0 0 118976 41 0 0 25 0 1 0 549885872 52441088 11312 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11312 603 41 0 12762 0
vsize: 51212
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14488
Raw data (stat): 14423 (minisat+) R 14422 20024 20023 0 -1 0 11709 0 0 0 119976 41 0 0 25 0 1 0 549885872 52441088 11312 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11312 603 41 0 12762 0
vsize: 51212
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 14488
Raw data (stat): 14423 (minisat+) Z 14422 20024 20023 0 -1 12 11711 0 0 0 119976 44 0 0 25 0 1 0 549885872 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.07
CPU time (s): 1200.21
CPU user time (s): 1199.76
CPU system time (s): 0.441932
CPU usage (%): 100.012
Max. virtual memory (Kb): 51212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####