PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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.15
Number of variables	7195
Total number of constraints	7621
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	7621
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	404
Trace number 18804

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 16:40:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17443 boxname=wulflinc22 idbench=1342 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a0fff131fa124ee4d61d9b3bf266a4ba  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air05.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air05.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air05.opb
IDLAUNCH: 17443
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        357836 kB
Buffers:         29828 kB
Cached:         617784 kB
SwapCached:         20 kB
Active:         118660 kB
Inactive:       531624 kB
HighTotal:      131008 kB
HighFree:        14672 kB
LowTotal:       903652 kB
LowFree:        343164 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            20804 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:00:24 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 17443 7 1200.2 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): 1.06 0.98 0.92 2/54 5012
Raw data (stat): 5012 (runsolver) R 5011 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546591165 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.9999 s]
Raw data (loadavg): 1.05 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11173 0 0 0 972 27 0 0 25 0 1 0 546591165 50348032 10776 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.001 s]
Raw data (loadavg): 1.04 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11178 0 0 0 1972 27 0 0 25 0 1 0 546591165 50348032 10781 4294967295 134512640 134672761 3221224544 3221223716 134556671 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.0013 s]
Raw data (loadavg): 1.04 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11219 0 0 0 2971 28 0 0 25 0 1 0 546591165 50483200 10822 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.002 s]
Raw data (loadavg): 1.03 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11242 0 0 0 3971 28 0 0 25 0 1 0 546591165 50618368 10845 4294967295 134512640 134672761 3221224544 3221223668 134566109 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.0028 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11276 0 0 0 4970 29 0 0 25 0 1 0 546591165 50753536 10879 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12391 10879 603 41 0 12350 0
vsize: 49564
[startup+60.0026 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11320 0 0 0 5970 29 0 0 25 0 1 0 546591165 50888704 10923 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12424 10923 603 41 0 12383 0
vsize: 49696
[startup+70.0033 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11344 0 0 0 6970 29 0 0 25 0 1 0 546591165 51023872 10947 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12457 10947 603 41 0 12416 0
vsize: 49828
[startup+80.0037 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11373 0 0 0 7970 29 0 0 25 0 1 0 546591165 51159040 10976 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.0045 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11400 0 0 0 8970 29 0 0 25 0 1 0 546591165 51294208 11003 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12523 11003 603 41 0 12482 0
vsize: 50092
[startup+100.004 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11420 0 0 0 9970 29 0 0 25 0 1 0 546591165 51294208 11023 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12523 11023 603 41 0 12482 0
vsize: 50092
[startup+110.004 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11439 0 0 0 10970 30 0 0 25 0 1 0 546591165 51429376 11042 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12556 11042 603 41 0 12515 0
vsize: 50224
[startup+120.005 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11454 0 0 0 11970 30 0 0 25 0 1 0 546591165 51429376 11057 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12556 11057 603 41 0 12515 0
vsize: 50224
[startup+130.005 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11476 0 0 0 12971 30 0 0 25 0 1 0 546591165 51564544 11079 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12589 11079 603 41 0 12548 0
vsize: 50356
[startup+140.005 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11492 0 0 0 13971 30 0 0 25 0 1 0 546591165 51564544 11095 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12589 11095 603 41 0 12548 0
vsize: 50356
[startup+150.006 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11506 0 0 0 14971 30 0 0 25 0 1 0 546591165 51699712 11109 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12622 11109 603 41 0 12581 0
vsize: 50488
[startup+160.005 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11520 0 0 0 15971 30 0 0 25 0 1 0 546591165 51699712 11123 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12622 11123 603 41 0 12581 0
vsize: 50488
[startup+170.005 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11527 0 0 0 16971 30 0 0 25 0 1 0 546591165 51834880 11130 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12655 11130 603 41 0 12614 0
vsize: 50620
[startup+180.005 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11539 0 0 0 17971 30 0 0 25 0 1 0 546591165 51834880 11142 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12655 11142 603 41 0 12614 0
vsize: 50620
[startup+190.006 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11554 0 0 0 18972 30 0 0 25 0 1 0 546591165 51834880 11157 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12655 11157 603 41 0 12614 0
vsize: 50620
[startup+200.005 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11564 0 0 0 19972 30 0 0 25 0 1 0 546591165 51834880 11167 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12655 11167 603 41 0 12614 0
vsize: 50620
[startup+210.008 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11570 0 0 0 20972 30 0 0 25 0 1 0 546591165 51970048 11173 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12688 11173 603 41 0 12647 0
vsize: 50752
[startup+220.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11582 0 0 0 21972 30 0 0 25 0 1 0 546591165 51970048 11185 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12688 11185 603 41 0 12647 0
vsize: 50752
[startup+230.008 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11591 0 0 0 22972 30 0 0 25 0 1 0 546591165 51970048 11194 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12688 11194 603 41 0 12647 0
vsize: 50752
[startup+240.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11597 0 0 0 23973 30 0 0 25 0 1 0 546591165 51970048 11200 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12688 11200 603 41 0 12647 0
vsize: 50752
[startup+250.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11604 0 0 0 24973 30 0 0 25 0 1 0 546591165 51970048 11207 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12688 11207 603 41 0 12647 0
vsize: 50752
[startup+260.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11607 0 0 0 25973 30 0 0 25 0 1 0 546591165 52105216 11210 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11210 603 41 0 12680 0
vsize: 50884
[startup+270.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11610 0 0 0 26973 30 0 0 25 0 1 0 546591165 52105216 11213 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11213 603 41 0 12680 0
vsize: 50884
[startup+280.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11611 0 0 0 27973 30 0 0 25 0 1 0 546591165 52105216 11214 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11214 603 41 0 12680 0
vsize: 50884
[startup+290.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11615 0 0 0 28973 30 0 0 25 0 1 0 546591165 52105216 11218 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11218 603 41 0 12680 0
vsize: 50884
[startup+300.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11615 0 0 0 29974 30 0 0 25 0 1 0 546591165 52105216 11218 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11218 603 41 0 12680 0
vsize: 50884
[startup+310.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11620 0 0 0 30974 30 0 0 25 0 1 0 546591165 52105216 11223 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11223 603 41 0 12680 0
vsize: 50884
[startup+320.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11621 0 0 0 31974 30 0 0 25 0 1 0 546591165 52105216 11224 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11224 603 41 0 12680 0
vsize: 50884
[startup+330.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11624 0 0 0 32974 30 0 0 25 0 1 0 546591165 52105216 11227 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11227 603 41 0 12680 0
vsize: 50884
[startup+340.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11625 0 0 0 33974 30 0 0 25 0 1 0 546591165 52105216 11228 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11627 0 0 0 34973 31 0 0 25 0 1 0 546591165 52105216 11230 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11230 603 41 0 12680 0
vsize: 50884
[startup+360.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11631 0 0 0 35974 31 0 0 25 0 1 0 546591165 52105216 11234 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11234 603 41 0 12680 0
vsize: 50884
[startup+370.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11635 0 0 0 36974 31 0 0 25 0 1 0 546591165 52105216 11238 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11238 603 41 0 12680 0
vsize: 50884
[startup+380.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11636 0 0 0 37974 31 0 0 25 0 1 0 546591165 52105216 11239 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11239 603 41 0 12680 0
vsize: 50884
[startup+390.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11636 0 0 0 38974 31 0 0 25 0 1 0 546591165 52105216 11239 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11239 603 41 0 12680 0
vsize: 50884
[startup+400.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11637 0 0 0 39974 31 0 0 25 0 1 0 546591165 52105216 11240 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11240 603 41 0 12680 0
vsize: 50884
[startup+410.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11639 0 0 0 40975 31 0 0 25 0 1 0 546591165 52105216 11242 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11242 603 41 0 12680 0
vsize: 50884
[startup+420.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11641 0 0 0 41975 31 0 0 25 0 1 0 546591165 52105216 11244 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11244 603 41 0 12680 0
vsize: 50884
[startup+430.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11642 0 0 0 42975 31 0 0 25 0 1 0 546591165 52105216 11245 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11245 603 41 0 12680 0
vsize: 50884
[startup+440.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11642 0 0 0 43975 31 0 0 25 0 1 0 546591165 52105216 11245 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11245 603 41 0 12680 0
vsize: 50884
[startup+450.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11648 0 0 0 44975 31 0 0 25 0 1 0 546591165 52105216 11251 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+460.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11648 0 0 0 45976 31 0 0 25 0 1 0 546591165 52105216 11251 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+470.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11648 0 0 0 46976 31 0 0 25 0 1 0 546591165 52105216 11251 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+480.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11648 0 0 0 47976 31 0 0 25 0 1 0 546591165 52105216 11251 4294967295 134512640 134672761 3221224544 3221223712 134564695 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11251 603 41 0 12680 0
vsize: 50884
[startup+490.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11649 0 0 0 48976 31 0 0 25 0 1 0 546591165 52105216 11252 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11252 603 41 0 12680 0
vsize: 50884
[startup+500.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11649 0 0 0 49976 31 0 0 25 0 1 0 546591165 52105216 11252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11252 603 41 0 12680 0
vsize: 50884
[startup+510.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11651 0 0 0 50976 31 0 0 25 0 1 0 546591165 52105216 11254 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11254 603 41 0 12680 0
vsize: 50884
[startup+520.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11653 0 0 0 51977 31 0 0 25 0 1 0 546591165 52105216 11256 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11256 603 41 0 12680 0
vsize: 50884
[startup+530.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11653 0 0 0 52977 31 0 0 25 0 1 0 546591165 52105216 11256 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11256 603 41 0 12680 0
vsize: 50884
[startup+540.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11655 0 0 0 53977 31 0 0 25 0 1 0 546591165 52105216 11258 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11258 603 41 0 12680 0
vsize: 50884
[startup+550.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11657 0 0 0 54977 31 0 0 25 0 1 0 546591165 52105216 11260 4294967295 134512640 134672761 3221224544 3221223752 134561962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11260 603 41 0 12680 0
vsize: 50884
[startup+560.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11658 0 0 0 55977 31 0 0 25 0 1 0 546591165 52105216 11261 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11261 603 41 0 12680 0
vsize: 50884
[startup+570.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11659 0 0 0 56977 31 0 0 25 0 1 0 546591165 52105216 11262 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11262 603 41 0 12680 0
vsize: 50884
[startup+580.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11660 0 0 0 57978 31 0 0 25 0 1 0 546591165 52105216 11263 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11263 603 41 0 12680 0
vsize: 50884
[startup+590.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11660 0 0 0 58977 31 0 0 25 0 1 0 546591165 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+600.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11664 0 0 0 59976 31 0 0 25 0 1 0 546591165 52105216 11267 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11664 0 0 0 60976 32 0 0 25 0 1 0 546591165 52105216 11267 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11267 603 41 0 12680 0
vsize: 50884
[startup+620.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11664 0 0 0 61976 32 0 0 25 0 1 0 546591165 52105216 11267 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12721 11267 603 41 0 12680 0
vsize: 50884
[startup+630.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11665 0 0 0 62976 32 0 0 25 0 1 0 546591165 52240384 11268 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11268 603 41 0 12713 0
vsize: 51016
[startup+640.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11666 0 0 0 63976 32 0 0 25 0 1 0 546591165 52240384 11269 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11269 603 41 0 12713 0
vsize: 51016
[startup+650.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11676 0 0 0 64976 32 0 0 25 0 1 0 546591165 52240384 11279 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+660.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11676 0 0 0 65976 32 0 0 25 0 1 0 546591165 52240384 11279 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+670.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11676 0 0 0 66977 32 0 0 25 0 1 0 546591165 52240384 11279 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+680.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11676 0 0 0 67977 32 0 0 25 0 1 0 546591165 52240384 11279 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11279 603 41 0 12713 0
vsize: 51016
[startup+690.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11681 0 0 0 68977 32 0 0 25 0 1 0 546591165 52240384 11284 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11284 603 41 0 12713 0
vsize: 51016
[startup+700.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11681 0 0 0 69977 32 0 0 25 0 1 0 546591165 52240384 11284 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11284 603 41 0 12713 0
vsize: 51016
[startup+710.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11683 0 0 0 70977 32 0 0 25 0 1 0 546591165 52240384 11286 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11683 0 0 0 71978 32 0 0 25 0 1 0 546591165 52240384 11286 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11683 0 0 0 72978 32 0 0 25 0 1 0 546591165 52240384 11286 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11683 0 0 0 73978 32 0 0 25 0 1 0 546591165 52240384 11286 4294967295 134512640 134672761 3221224544 3221223808 134562262 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.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11684 0 0 0 74978 32 0 0 25 0 1 0 546591165 52240384 11287 4294967295 134512640 134672761 3221224544 3221223716 134556680 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.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11684 0 0 0 75978 32 0 0 25 0 1 0 546591165 52240384 11287 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11684 0 0 0 76978 32 0 0 25 0 1 0 546591165 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+780.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11684 0 0 0 77979 32 0 0 25 0 1 0 546591165 52240384 11287 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11684 0 0 0 78979 32 0 0 25 0 1 0 546591165 52240384 11287 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11287 603 41 0 12713 0
vsize: 51016
[startup+800.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11685 0 0 0 79979 32 0 0 25 0 1 0 546591165 52240384 11288 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11685 0 0 0 80978 32 0 0 25 0 1 0 546591165 52240384 11288 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11685 0 0 0 81978 32 0 0 25 0 1 0 546591165 52240384 11288 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11685 0 0 0 82978 32 0 0 25 0 1 0 546591165 52240384 11288 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11685 0 0 0 83978 32 0 0 25 0 1 0 546591165 52240384 11288 4294967295 134512640 134672761 3221224544 3221223668 134566151 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.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11686 0 0 0 84979 32 0 0 25 0 1 0 546591165 52240384 11289 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11686 0 0 0 85979 32 0 0 25 0 1 0 546591165 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+870.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11686 0 0 0 86979 32 0 0 25 0 1 0 546591165 52240384 11289 4294967295 134512640 134672761 3221224544 3221223712 134561139 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.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11686 0 0 0 87979 32 0 0 25 0 1 0 546591165 52240384 11289 4294967295 134512640 134672761 3221224544 3221223668 134566109 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.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11687 0 0 0 88979 32 0 0 25 0 1 0 546591165 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.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11687 0 0 0 89980 32 0 0 25 0 1 0 546591165 52240384 11290 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11687 0 0 0 90980 32 0 0 25 0 1 0 546591165 52240384 11290 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12754 11290 603 41 0 12713 0
vsize: 51016
[startup+920.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 91980 32 0 0 25 0 1 0 546591165 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+930.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 92980 32 0 0 25 0 1 0 546591165 52240384 11291 4294967295 134512640 134672761 3221224544 3221223716 134556685 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.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 93980 32 0 0 25 0 1 0 546591165 52240384 11291 4294967295 134512640 134672761 3221224544 3221223668 134566118 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.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 94981 32 0 0 25 0 1 0 546591165 52240384 11291 4294967295 134512640 134672761 3221224544 3221223668 134566071 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.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 95981 32 0 0 25 0 1 0 546591165 52240384 11291 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 96981 32 0 0 25 0 1 0 546591165 52240384 11291 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11688 0 0 0 97981 32 0 0 25 0 1 0 546591165 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+990.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 98981 32 0 0 25 0 1 0 546591165 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+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 99982 32 0 0 25 0 1 0 546591165 52240384 11292 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 100982 32 0 0 25 0 1 0 546591165 52240384 11292 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 101982 32 0 0 25 0 1 0 546591165 52240384 11292 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 102982 32 0 0 25 0 1 0 546591165 52240384 11292 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 103982 32 0 0 25 0 1 0 546591165 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+1050.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11689 0 0 0 104982 32 0 0 25 0 1 0 546591165 52240384 11292 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 105983 32 0 0 25 0 1 0 546591165 52240384 11294 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 106983 32 0 0 25 0 1 0 546591165 52240384 11294 4294967295 134512640 134672761 3221224544 3221223760 134561993 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 107983 32 0 0 25 0 1 0 546591165 52240384 11294 4294967295 134512640 134672761 3221224544 3221223668 134566047 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 108983 32 0 0 25 0 1 0 546591165 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+1100.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 109983 32 0 0 25 0 1 0 546591165 52240384 11294 4294967295 134512640 134672761 3221224544 3221223712 134564746 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 110984 32 0 0 25 0 1 0 546591165 52240384 11294 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11691 0 0 0 111984 32 0 0 25 0 1 0 546591165 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+1130.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11708 0 0 0 112984 32 0 0 25 0 1 0 546591165 52441088 11311 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11708 0 0 0 113984 32 0 0 25 0 1 0 546591165 52441088 11311 4294967295 134512640 134672761 3221224544 3221223696 134565086 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11708 0 0 0 114984 32 0 0 25 0 1 0 546591165 52441088 11311 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12803 11311 603 41 0 12762 0
vsize: 51212
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11709 0 0 0 115984 32 0 0 25 0 1 0 546591165 52441088 11312 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11709 0 0 0 116983 33 0 0 25 0 1 0 546591165 52441088 11312 4294967295 134512640 134672761 3221224544 3221223712 134565153 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.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 5012
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11709 0 0 0 117984 33 0 0 25 0 1 0 546591165 52441088 11312 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.02 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 5065
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11709 0 0 0 118983 33 0 0 25 0 1 0 546591165 52441088 11312 4294967295 134512640 134672761 3221224544 3221223668 134566071 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.02 s]
Raw data (loadavg): 1.13 1.01 0.93 2/54 5065
Raw data (stat): 5012 (minisat+) R 5011 26298 26297 0 -1 0 11709 0 0 0 119984 33 0 0 25 0 1 0 546591165 52441088 11312 4294967295 134512640 134672761 3221224544 3221223668 134566029 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.04 s]
Raw data (loadavg): 1.13 1.01 0.93 1/54 5065
Raw data (stat): 5012 (minisat+) Z 5011 26298 26297 0 -1 12 11711 0 0 0 119984 35 0 0 25 0 1 0 546591165 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.04
CPU time (s): 1200.2
CPU user time (s): 1199.84
CPU system time (s): 0.352946
CPU usage (%): 100.013
Max. virtual memory (Kb): 51212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####