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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran13x13.opb
MD5SUM	688d61d0de54e028c8c4910e094a132c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	893343
Optimality of the best value was proved	NO
Number of terms in the objective function	3549
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	949933178
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	949933178
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	3549
Total number of constraints	195
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	195
Minimum length of a constraint	21
Maximum length of a constraint	260
Trace number 31269

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-05-25 23:39:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22668 boxname=wulflinc9 idbench=1484 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  688d61d0de54e028c8c4910e094a132c  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-ran13x13.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-ran13x13.opb
IDLAUNCH: 22668
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        517228 kB
Buffers:         38172 kB
Cached:         458188 kB
SwapCached:        584 kB
Active:          18772 kB
Inactive:       479644 kB
HighTotal:      131008 kB
HighFree:        31304 kB
LowTotal:       903652 kB
LowFree:        485924 kB
SwapTotal:     2097136 kB
SwapFree:      2095648 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            13408 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:59:51 (client local time) WITH STATUS 152 IN 1229.91 SECONDS
stats: 22668 7 1229.91 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 219]---> Adder-cost: 250   maxlim: 16883   bits: 15/15
c ---[ 217]---> Adder-cost: 258   maxlim: 26227   bits: 15/15
c ---[ 215]---> Adder-cost: 258   maxlim: 26867   bits: 15/15
c ---[ 213]---> Adder-cost: 250   maxlim: 17139   bits: 15/15
c ---[ 211]---> Adder-cost: 258   maxlim: 26355   bits: 15/15
c ---[ 209]---> Adder-cost: 250   maxlim: 17267   bits: 15/15
c ---[ 207]---> Adder-cost: 258   maxlim: 25331   bits: 15/15
c ---[ 205]---> Adder-cost: 250   maxlim: 17011   bits: 15/15
c ---[ 203]---> Adder-cost: 234   maxlim: 10611   bits: 14/14
c ---[ 201]---> Adder-cost: 258   maxlim: 26227   bits: 15/15
c ---[ 199]---> Adder-cost: 234   maxlim: 10611   bits: 14/14
c ---[ 197]---> Adder-cost: 258   maxlim: 26611   bits: 15/15
c ---[ 195]---> Adder-cost: 250   maxlim: 17139   bits: 15/15
c ---[ 193]---> Adder-cost: 272   maxlim: 34291   bits: 16/16
c ---[ 191]---> Adder-cost: 272   maxlim: 33267   bits: 16/16
c ---[ 189]---> Adder-cost: 216   maxlim: 6387   bits: 13/13
c ---[ 187]---> Adder-cost: 258   maxlim: 23411   bits: 15/15
c ---[ 185]---> Adder-cost: 240   maxlim: 12659   bits: 14/14
c ---[ 183]---> Adder-cost: 258   maxlim: 22899   bits: 15/15
c ---[ 181]---> Adder-cost: 240   maxlim: 12531   bits: 14/14
c ---[ 179]---> Adder-cost: 216   maxlim: 6259   bits: 13/13
c ---[ 177]---> Adder-cost: 272   maxlim: 31347   bits: 16/15
c ---[ 175]---> Adder-cost: 240   maxlim: 12787   bits: 14/14
c ---[ 173]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[ 171]---> Adder-cost: 272   maxlim: 32499   bits: 16/15
c ---[ 169]---> Adder-cost: 272   maxlim: 32755   bits: 16/15
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   10
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   10
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   16
c ---[ 160]---> BDD-cost:   16
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   16
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:   16
c ---[ 151]---> BDD-cost:   16
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   15
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   13
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   10
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   12
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   15
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   15
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   15
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   10
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   49961   167448 |   16653       0        0     nan |  0.000 % |
c |       101 |   49827   167107 |   18318      93      434     4.7 | 20.562 % |
c |       252 |   49788   166980 |   20150     238      965     4.1 | 20.617 % |
c |       477 |   49519   166320 |   22165     443     1783     4.0 | 21.187 % |
c |       815 |   49377   165842 |   24381     768     2903     3.8 | 21.390 % |
c |      1321 |   49087   165095 |   26819    1253     4530     3.6 | 22.006 % |
c |      2080 |   48957   164719 |   29501    1995     7982     4.0 | 22.225 % |
c |      3220 |   48957   164719 |   32451    3135    14990     4.8 | 22.225 % |
c |      4929 |   48556   163744 |   35697    4828    30968     6.4 | 23.224 % |
c |      7492 |   48457   163458 |   39266    7380    56954     7.7 | 23.404 % |
c |     11336 |   48242   162798 |   43193   11203   116759    10.4 | 23.794 % |
c |     17103 |   48174   162576 |   47512   16959   372390    22.0 | 23.880 % |
c |     25752 |   48057   162220 |   52264   25595  1058459    41.4 | 24.114 % |
c |     38727 |   47376   160224 |   57490   38486  1289829    33.5 | 25.379 % |
c |     58188 |   47002   159003 |   63239   57887  1746797    30.2 | 25.941 % |
c ==============================================================================
c [1mFound solution: 4024630[0m
c ---[   0]---> Adder-cost: 6663   maxlim: 1668164   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63706 |   93412   324815 |   31137   63382  1833123    28.9 | 25.941 % |
c |     63806 |   93412   324815 |   34250   21313   322945    15.2 | 17.225 % |
c |     63956 |   93412   324815 |   37675   21463   325652    15.2 | 17.225 % |
c |     64181 |   93412   324815 |   41443   21688   327834    15.1 | 17.225 % |
c |     64519 |   93412   324815 |   45587   22026   331360    15.0 | 17.225 % |
c |     65025 |   93405   324798 |   50146   22531   337207    15.0 | 17.236 % |
c |     65784 |   93405   324798 |   55161   23290   345611    14.8 | 17.236 % |
c |     66924 |   93405   324798 |   60677   24430   357901    14.7 | 17.236 % |
c |     68633 |   93278   324443 |   66744   26100   380811    14.6 | 17.384 % |
c |     71195 |   93245   324330 |   73419   28654   412333    14.4 | 17.410 % |
c |     75039 |   93139   323968 |   80761   32473   463203    14.3 | 17.497 % |
c ==============================================================================
c [1mFound solution: 3886697[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1806097   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75559 |   93170   324170 |   31056   32993   470167    14.3 | 17.497 % |
c |     75659 |   93170   324170 |   34161   33093   471064    14.2 | 17.535 % |
c |     75809 |   93170   324170 |   37577   33243   472570    14.2 | 17.535 % |
c |     76034 |   93170   324170 |   41335   33468   474817    14.2 | 17.535 % |
c |     76371 |   93161   324141 |   45469   33804   484509    14.3 | 17.546 % |
c |     76877 |   93152   324110 |   50015   34307   488624    14.2 | 17.551 % |
c |     77636 |   93152   324110 |   55017   35066   500194    14.3 | 17.551 % |
c |     78775 |   93143   324081 |   60519   36204   526126    14.5 | 17.561 % |
c ==============================================================================
c [1mFound solution: 3643228[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2049566   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80098 |   93168   324292 |   31056   37527   541695    14.4 | 17.561 % |
c |     80198 |   93168   324292 |   34161   18864   174598     9.3 | 17.606 % |
c |     80349 |   93159   324272 |   37577   19014   175573     9.2 | 17.621 % |
c |     80574 |   93159   324272 |   41335   19239   177301     9.2 | 17.621 % |
c |     80911 |   93159   324272 |   45469   19576   181915     9.3 | 17.621 % |
c |     81417 |   93159   324272 |   50015   20082   187299     9.3 | 17.621 % |
c |     82176 |   93159   324272 |   55017   20841   193212     9.3 | 17.621 % |
c |     83315 |   93126   324194 |   60519   21976   201431     9.2 | 17.683 % |
c |     85023 |   93101   324113 |   66571   23681   220770     9.3 | 17.708 % |
c ==============================================================================
c [1mFound solution: 3634438[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2058356   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86716 |   93115   324255 |   31038   25374   239138     9.4 | 17.708 % |
c |     86816 |   93115   324255 |   34141   25474   239884     9.4 | 17.735 % |
c |     86967 |   93115   324255 |   37555   25625   241334     9.4 | 17.735 % |
c |     87192 |   93115   324255 |   41311   25850   243683     9.4 | 17.735 % |
c |     87529 |   93115   324255 |   45442   26187   262950    10.0 | 17.735 % |
c |     88035 |   93115   324255 |   49987   26693   267803    10.0 | 17.735 % |
c ==============================================================================
c [1mFound solution: 3490387[0m
c ---[   0]---> Adder-cost: 2   maxlim: 2202407   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88371 |   93137   324407 |   31045   27029   271480    10.0 | 17.735 % |
c |     88471 |   93137   324407 |   34149   27129   272716    10.1 | 17.770 % |
c |     88621 |   93130   324384 |   37564   27278   274062    10.0 | 17.775 % |
c |     88846 |   93130   324384 |   41320   27503   276299    10.0 | 17.775 % |
c |     89183 |   93130   324384 |   45452   27840   280352    10.1 | 17.775 % |
c |     89689 |   93130   324384 |   49998   28346   284703    10.0 | 17.775 % |
c |     90448 |   93121   324353 |   54998   29103   292534    10.1 | 17.781 % |
c |     91587 |   93112   324322 |   60497   30236   305192    10.1 | 17.786 % |
c |     93295 |   93112   324322 |   66547   31944   432924    13.6 | 17.786 % |
c |     95857 |   93112   324322 |   73202   34506   484766    14.0 | 17.786 % |
c |     99701 |   93112   324322 |   80522   38350   747982    19.5 | 17.786 % |
c |    105469 |   93078   324219 |   88575   44113  1262340    28.6 | 17.827 % |
c ==============================================================================
c [1mFound solution: 3347499[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2345295   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107685 |   93080   324297 |   31026   46327  1311358    28.3 | 17.827 % |
c |    107785 |   93080   324297 |   34128   20519   855845    41.7 | 17.868 % |
c |    107936 |   93080   324297 |   37541   20670   856908    41.5 | 17.868 % |
c |    108161 |   93080   324297 |   41295   20895   858293    41.1 | 17.868 % |
c |    108498 |   93080   324297 |   45425   21232   860559    40.5 | 17.868 % |
c |    109005 |   93080   324297 |   49967   21739   864916    39.8 | 17.868 % |
c |    109764 |   93080   324297 |   54964   22498   872415    38.8 | 17.868 % |
c |    110903 |   93080   324297 |   60460   23637   881764    37.3 | 17.868 % |
c |    112611 |   93080   324297 |   66506   25345   894589    35.3 | 17.868 % |
c |    115173 |   93080   324297 |   73157   27907   913145    32.7 | 17.868 % |
c |    119017 |   93071   324266 |   80473   31750   958208    30.2 | 17.873 % |
c |    124786 |   92987   324066 |   88520   37511  1466662    39.1 | 17.996 % |
c |    133435 |   92951   323963 |   97372   46151  1843380    39.9 | 18.042 % |
c ==============================================================================
c [1mFound solution: 3283408[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2409386   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137890 |   92948   324082 |   30982   50605  2139997    42.3 | 18.042 % |
c |    137990 |   92948   324082 |   34080   21283   666148    31.3 | 18.102 % |
c |    138140 |   92948   324082 |   37488   21433   667480    31.1 | 18.102 % |
c |    138365 |   92948   324082 |   41237   21658   669391    30.9 | 18.102 % |
c |    138702 |   92948   324082 |   45360   21995   671373    30.5 | 18.102 % |
c |    139208 |   92948   324082 |   49896   22501   674557    30.0 | 18.102 % |
c |    139967 |   92948   324082 |   54886   23260   679684    29.2 | 18.102 % |
c |    141106 |   92942   324062 |   60375   24398   688282    28.2 | 18.107 % |
c |    142814 |   92942   324062 |   66412   26106   704913    27.0 | 18.107 % |
c |    145376 |   92942   324062 |   73053   28668   726695    25.3 | 18.107 % |
c |    149221 |   92942   324062 |   80359   32513   766271    23.6 | 18.107 % |
c |    154987 |   92942   324062 |   88395   38279   832015    21.7 | 18.107 % |
c |    163638 |   92942   324062 |   97234   46930  2548251    54.3 | 18.107 % |
c |    176616 |   92920   323988 |  106958   59900  3196261    53.4 | 18.123 % |
c ==============================================================================
c [1mFound solution: 1741875[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3950919   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    190860 |   92932   324088 |   30977   74144  3969570    53.5 | 18.123 % |
c |    190961 |   92932   324088 |   34074   23456   743205    31.7 | 18.153 % |
c |    191111 |   92932   324088 |   37482   23606   744104    31.5 | 18.153 % |
c |    191336 |   92923   324059 |   41230   23830   745741    31.3 | 18.163 % |
c |    191673 |   92923   324059 |   45353   24167   748173    31.0 | 18.163 % |
c |    192179 |   92923   324059 |   49888   24673   753078    30.5 | 18.163 % |
c |    192938 |   92923   324059 |   54877   25432   759316    29.9 | 18.163 % |
c |    194077 |   92899   323997 |   60365   26569   774123    29.1 | 18.204 % |
c |    195785 |   92890   323966 |   66401   28274   797590    28.2 | 18.209 % |
c |    198348 |   92890   323966 |   73042   30837   845219    27.4 | 18.209 % |
c |    202195 |   92890   323966 |   80346   34684   964322    27.8 | 18.209 % |
c |    207961 |   92890   323966 |   88380   40450  1087358    26.9 | 18.209 % |
c |    216613 |   92890   323966 |   97219   49102  1398742    28.5 | 18.209 % |
c |    229587 |   92881   323935 |  106941   62073  1844783    29.7 | 18.214 % |
c |    249049 |   92874   323915 |  117635   81533  2966279    36.4 | 18.219 % |
c |    278243 |   92837   323818 |  129398  110725  5102966    46.1 | 18.280 % |
c |    322034 |   92837   323818 |  142338   30827  5136593   166.6 | 18.280 % |
c |    387718 |   92837   323818 |  156572   96511  8750292    90.7 | 18.280 % |
c |    486245 |   92822   323784 |  172229   45653  8072144   176.8 | 18.301 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25452 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.91 0.97 0.91 2/54 25448
Raw data (stat): 25448 (runsolver) R 25447 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784684048 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.07 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.07 s]
Raw data (loadavg): 1.14 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.07 s]
Raw data (loadavg): 1.11 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.07 s]
Raw data (loadavg): 1.10 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.07 s]
Raw data (loadavg): 1.08 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.07 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.07 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.07 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.07 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.07 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.77 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 25452
Raw data (stat): 25448 (minisat+_script) S 25447 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784684048 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.76
CPU time (s): 1229.91
CPU user time (s): 1228.69
CPU system time (s): 1.21581
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####