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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc07.opb
MD5SUM9cc94d1db4d494288ef67a8d5ad5d77e
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1408128
Optimality of the best value was proved NO
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 11486079
Number of bits of the biggest sum of numbers24
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables280
Total number of constraints471
Number of constraints which are clauses127
Number of constraints which are cardinality constraints (but not clauses)272
Number of constraints which are nor clauses,nor cardinality constraints72
Minimum length of a constraint1
Maximum length of a constraint253

Trace number 15651 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 05:24:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17016 boxname=wulflinc10 idbench=1309 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9cc94d1db4d494288ef67a8d5ad5d77e  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17016
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        552116 kB
Buffers:         32652 kB
Cached:         427912 kB
SwapCached:          0 kB
Active:         129916 kB
Inactive:       333164 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        551864 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13852 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:44:17 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 17016 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> BDD-cost:1205780
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> BDD-cost:   78
c ---[  97]---> BDD-cost:   78
c ---[  95]---> BDD-cost:   78
c ---[  93]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   78
c ---[  89]---> BDD-cost:   78
c ---[  87]---> BDD-cost:   78
c ---[  85]---> BDD-cost:   78
c ---[  83]---> BDD-cost:   78
c ---[  81]---> BDD-cost:   78
c ---[  79]---> BDD-cost:   78
c ---[  77]---> BDD-cost:   78
c ---[  75]---> BDD-cost:   78
c ---[  73]---> BDD-cost:   78
c ---[  71]---> BDD-cost:   78
c ---[  69]---> BDD-cost:   78
c ---[  67]---> BDD-cost:   78
c ---[  65]---> BDD-cost:   78
c ---[  63]---> BDD-cost:   78
c ---[  61]---> BDD-cost:   78
c ---[  59]---> BDD-cost:   78
c ---[  57]---> BDD-cost:   78
c ---[  55]---> BDD-cost:   78
c ---[  53]---> BDD-cost:   78
c ---[  51]---> BDD-cost:   78
c ---[  49]---> BDD-cost:   78
c ---[  47]---> BDD-cost:   78
c ---[  46]---> BDD-cost:   25
c ---[  45]---> BDD-cost:   25
c ---[  44]---> BDD-cost:   25
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   50
c ---[  28]---> BDD-cost:   50
c ---[  27]---> BDD-cost:   50
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   50
c ---[  16]---> BDD-cost:   50
c ---[  15]---> BDD-cost:   50
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   50
c ---[   4]---> BDD-cost:   50
c ---[   3]---> BDD-cost:   50
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3565828 10573606 | 1188609       0        0     nan |  0.000 % |
c |       100 | 3565828 10573606 | 1307469     100     6422    64.2 |  0.007 % |
c ==============================================================================
c Found solution: 1557888
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   75     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       134 | 3565966 10573933 | 1188655     134     7995    59.7 |  0.007 % |
c ==============================================================================
c Found solution: 1467008
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   76     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       154 | 3566110 10574271 | 1188703     154    10875    70.6 |  0.007 % |
c |       255 | 3566110 10574271 | 1307573     255    18567    72.8 |  0.007 % |
c ==============================================================================
c Found solution: 1454208
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   66     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       284 | 3566228 10574548 | 1188742     284    20572    72.4 |  0.007 % |
c |       385 | 3566228 10574548 | 1307616     385    58981   153.2 |  0.007 % |
c ==============================================================================
c Found solution: 1442688
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   67     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       480 | 3566346 10574824 | 1188782     480    67307   140.2 |  0.007 % |
c ==============================================================================
c Found solution: 1408128
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   50     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       570 | 3566433 10575032 | 1188811     570    98697   173.2 |  0.007 % |
c |       672 | 3566433 10575032 | 1307692     672   116833   173.9 |  0.007 % |
c |       825 | 3566433 10575032 | 1438461     825   129912   157.5 |  0.007 % |
c |      1050 | 3566433 10575032 | 1582307    1050   158299   150.8 |  0.007 % |
c |      1387 | 3566433 10575032 | 1740538    1387   186879   134.7 |  0.007 % |
c |      1893 | 3566433 10575032 | 1914592    1893   266636   140.9 |  0.007 % |
c |      2652 | 3566433 10575032 | 2106051    2652   378066   142.6 |  0.007 % |
c |      3792 | 3566433 10575032 | 2316656    3792   544588   143.6 |  0.007 % |
#### 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.84 0.94 0.90 2/54 24979
Raw data (stat): 24979 (runsolver) R 24978 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484322188 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.0011 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 52219 0 0 0 877 121 0 0 25 0 1 0 484322188 216825856 44287 4294967295 134512640 134672761 3221224544 3221201536 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52936 44288 603 41 0 52895 0
vsize: 211744
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 106779 0 0 0 1745 254 0 0 25 0 1 0 484322188 489775104 98847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119574 98847 603 41 0 119533 0
vsize: 478296
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 110375 0 0 0 2735 262 0 0 25 0 1 0 484322188 500723712 102443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122247 102443 603 41 0 122206 0
vsize: 488988
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 110571 0 0 0 3734 263 0 0 25 0 1 0 484322188 500994048 102639 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122313 102639 603 41 0 122272 0
vsize: 489252
[startup+50.002 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112034 0 0 0 4731 266 0 0 25 0 1 0 484322188 506544128 104102 4294967295 134512640 134672761 3221224544 3221223676 134565974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123668 104102 603 41 0 123627 0
vsize: 494672
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112038 0 0 0 5731 266 0 0 25 0 1 0 484322188 511385600 104106 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124850 104106 603 41 0 124809 0
vsize: 499400
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112050 0 0 0 6731 266 0 0 25 0 1 0 484322188 511459328 104118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124868 104118 603 41 0 124827 0
vsize: 499472
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112051 0 0 0 7730 267 0 0 25 0 1 0 484322188 511459328 104119 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124868 104119 603 41 0 124827 0
vsize: 499472
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112056 0 0 0 8730 267 0 0 25 0 1 0 484322188 511459328 104124 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124868 104124 603 41 0 124827 0
vsize: 499472
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112077 0 0 0 9731 267 0 0 25 0 1 0 484322188 511569920 104145 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124895 104145 603 41 0 124854 0
vsize: 499580
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112083 0 0 0 10731 267 0 0 25 0 1 0 484322188 511569920 104151 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124895 104151 603 41 0 124854 0
vsize: 499580
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112101 0 0 0 11731 267 0 0 25 0 1 0 484322188 511569920 104169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124895 104169 603 41 0 124854 0
vsize: 499580
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112105 0 0 0 12730 267 0 0 25 0 1 0 484322188 511705088 104173 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124928 104173 603 41 0 124887 0
vsize: 499712
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112108 0 0 0 13731 267 0 0 25 0 1 0 484322188 511705088 104176 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124928 104176 603 41 0 124887 0
vsize: 499712
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112174 0 0 0 14731 267 0 0 25 0 1 0 484322188 512339968 104242 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125083 104242 603 41 0 125042 0
vsize: 500332
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112205 0 0 0 15731 267 0 0 25 0 1 0 484322188 512434176 104273 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125106 104273 603 41 0 125065 0
vsize: 500424
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112215 0 0 0 16731 267 0 0 25 0 1 0 484322188 512434176 104283 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125106 104283 603 41 0 125065 0
vsize: 500424
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112217 0 0 0 17731 267 0 0 25 0 1 0 484322188 512434176 104285 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125106 104285 603 41 0 125065 0
vsize: 500424
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112228 0 0 0 18731 267 0 0 25 0 1 0 484322188 512491520 104295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125120 104295 603 41 0 125079 0
vsize: 500480
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112228 0 0 0 19731 267 0 0 25 0 1 0 484322188 512491520 104295 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125120 104295 603 41 0 125079 0
vsize: 500480
[startup+210.001 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112228 0 0 0 20732 267 0 0 25 0 1 0 484322188 512491520 104295 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125120 104295 603 41 0 125079 0
vsize: 500480
[startup+220.002 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112245 0 0 0 21732 267 0 0 25 0 1 0 484322188 512548864 104311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+230.001 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112245 0 0 0 22732 267 0 0 25 0 1 0 484322188 512548864 104311 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+240.001 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112245 0 0 0 23732 267 0 0 25 0 1 0 484322188 512548864 104311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+250 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112277 0 0 0 24732 267 0 0 25 0 1 0 484322188 512741376 104343 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104343 603 41 0 125140 0
vsize: 500724
[startup+260.001 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112279 0 0 0 25732 267 0 0 25 0 1 0 484322188 512741376 104345 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104345 603 41 0 125140 0
vsize: 500724
[startup+270.001 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112282 0 0 0 26733 267 0 0 25 0 1 0 484322188 512741376 104348 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104348 603 41 0 125140 0
vsize: 500724
[startup+280 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112290 0 0 0 27733 267 0 0 25 0 1 0 484322188 512741376 104356 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+290 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112290 0 0 0 28733 267 0 0 25 0 1 0 484322188 512741376 104356 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+300 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112290 0 0 0 29733 267 0 0 25 0 1 0 484322188 512741376 104356 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+310.001 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112290 0 0 0 30733 267 0 0 25 0 1 0 484322188 512741376 104356 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+320 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112291 0 0 0 31733 267 0 0 25 0 1 0 484322188 512741376 104357 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104357 603 41 0 125140 0
vsize: 500724
[startup+330 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112291 0 0 0 32734 267 0 0 25 0 1 0 484322188 512741376 104357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104357 603 41 0 125140 0
vsize: 500724
[startup+340 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112291 0 0 0 33734 267 0 0 25 0 1 0 484322188 512741376 104357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104357 603 41 0 125140 0
vsize: 500724
[startup+350 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112294 0 0 0 34734 267 0 0 25 0 1 0 484322188 512741376 104360 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104360 603 41 0 125140 0
vsize: 500724
[startup+360.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112299 0 0 0 35734 267 0 0 25 0 1 0 484322188 512741376 104365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125181 104365 603 41 0 125140 0
vsize: 500724
[startup+370 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112310 0 0 0 36734 267 0 0 25 0 1 0 484322188 512860160 104376 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125210 104376 603 41 0 125169 0
vsize: 500840
[startup+380 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112310 0 0 0 37734 267 0 0 25 0 1 0 484322188 512860160 104376 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125210 104376 603 41 0 125169 0
vsize: 500840
[startup+390 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112327 0 0 0 38735 267 0 0 25 0 1 0 484322188 512860160 104393 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125210 104393 603 41 0 125169 0
vsize: 500840
[startup+400.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112339 0 0 0 39735 267 0 0 25 0 1 0 484322188 512942080 104405 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125230 104405 603 41 0 125189 0
vsize: 500920
[startup+410.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112345 0 0 0 40735 267 0 0 25 0 1 0 484322188 512958464 104410 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125234 104410 603 41 0 125193 0
vsize: 500936
[startup+420.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112356 0 0 0 41735 267 0 0 25 0 1 0 484322188 512991232 104420 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125242 104420 603 41 0 125201 0
vsize: 500968
[startup+430 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112358 0 0 0 42735 267 0 0 25 0 1 0 484322188 512991232 104422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125242 104422 603 41 0 125201 0
vsize: 500968
[startup+440.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112358 0 0 0 43735 267 0 0 25 0 1 0 484322188 512991232 104422 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125242 104422 603 41 0 125201 0
vsize: 500968
[startup+450 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112359 0 0 0 44736 267 0 0 25 0 1 0 484322188 512991232 104423 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125242 104423 603 41 0 125201 0
vsize: 500968
[startup+460 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112366 0 0 0 45736 267 0 0 25 0 1 0 484322188 513048576 104429 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125256 104429 603 41 0 125215 0
vsize: 501024
[startup+470 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112367 0 0 0 46736 267 0 0 25 0 1 0 484322188 513048576 104430 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125256 104430 603 41 0 125215 0
vsize: 501024
[startup+480 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112381 0 0 0 47736 267 0 0 25 0 1 0 484322188 513118208 104444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+490 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112381 0 0 0 48736 267 0 0 25 0 1 0 484322188 513118208 104444 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+500 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112381 0 0 0 49736 267 0 0 25 0 1 0 484322188 513118208 104444 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+510.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112381 0 0 0 50737 267 0 0 25 0 1 0 484322188 513118208 104444 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+520 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112386 0 0 0 51737 267 0 0 25 0 1 0 484322188 513118208 104449 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125273 104449 603 41 0 125232 0
vsize: 501092
[startup+530 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112400 0 0 0 52737 268 0 0 25 0 1 0 484322188 513196032 104463 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125292 104463 603 41 0 125251 0
vsize: 501168
[startup+540 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112400 0 0 0 53737 268 0 0 25 0 1 0 484322188 513196032 104463 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125292 104463 603 41 0 125251 0
vsize: 501168
[startup+550 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112400 0 0 0 54737 268 0 0 25 0 1 0 484322188 513196032 104463 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125292 104463 603 41 0 125251 0
vsize: 501168
[startup+560.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112421 0 0 0 55737 268 0 0 25 0 1 0 484322188 513306624 104484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104484 603 41 0 125278 0
vsize: 501276
[startup+570.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112427 0 0 0 56737 268 0 0 25 0 1 0 484322188 513306624 104490 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125319 104490 603 41 0 125278 0
vsize: 501276
[startup+580.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112427 0 0 0 57737 268 0 0 25 0 1 0 484322188 513306624 104490 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125319 104490 603 41 0 125278 0
vsize: 501276
[startup+590.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112427 0 0 0 58737 268 0 0 25 0 1 0 484322188 513306624 104490 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125319 104490 603 41 0 125278 0
vsize: 501276
[startup+600 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112429 0 0 0 59738 268 0 0 25 0 1 0 484322188 513306624 104492 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125319 104492 603 41 0 125278 0
vsize: 501276
[startup+610.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112429 0 0 0 60738 268 0 0 25 0 1 0 484322188 513306624 104492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125319 104492 603 41 0 125278 0
vsize: 501276
[startup+620.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112432 0 0 0 61738 268 0 0 25 0 1 0 484322188 513306624 104495 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125319 104495 603 41 0 125278 0
vsize: 501276
[startup+630 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112440 0 0 0 62738 268 0 0 25 0 1 0 484322188 513380352 104503 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125337 104503 603 41 0 125296 0
vsize: 501348
[startup+640.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112447 0 0 0 63738 268 0 0 25 0 1 0 484322188 513380352 104510 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125337 104510 603 41 0 125296 0
vsize: 501348
[startup+650 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112448 0 0 0 64738 268 0 0 25 0 1 0 484322188 513380352 104511 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125337 104511 603 41 0 125296 0
vsize: 501348
[startup+660 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112448 0 0 0 65739 268 0 0 25 0 1 0 484322188 513380352 104511 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125337 104511 603 41 0 125296 0
vsize: 501348
[startup+670 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112451 0 0 0 66739 268 0 0 25 0 1 0 484322188 513380352 104514 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125337 104514 603 41 0 125296 0
vsize: 501348
[startup+679.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112472 0 0 0 67739 268 0 0 25 0 1 0 484322188 513454080 104535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125355 104535 603 41 0 125314 0
vsize: 501420
[startup+690 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112472 0 0 0 68739 268 0 0 25 0 1 0 484322188 513454080 104535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125355 104535 603 41 0 125314 0
vsize: 501420
[startup+699.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112478 0 0 0 69739 268 0 0 25 0 1 0 484322188 513503232 104540 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125367 104540 603 41 0 125326 0
vsize: 501468
[startup+710 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112478 0 0 0 70740 268 0 0 25 0 1 0 484322188 513503232 104540 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125367 104540 603 41 0 125326 0
vsize: 501468
[startup+719.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112494 0 0 0 71740 268 0 0 25 0 1 0 484322188 513531904 104555 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125374 104555 603 41 0 125333 0
vsize: 501496
[startup+729.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112504 0 0 0 72740 268 0 0 25 0 1 0 484322188 513597440 104564 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125390 104564 603 41 0 125349 0
vsize: 501560
[startup+740 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112521 0 0 0 73740 268 0 0 25 0 1 0 484322188 513654784 104580 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125404 104580 603 41 0 125363 0
vsize: 501616
[startup+749.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112521 0 0 0 74740 268 0 0 25 0 1 0 484322188 513654784 104580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125404 104580 603 41 0 125363 0
vsize: 501616
[startup+759.999 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112521 0 0 0 75740 268 0 0 25 0 1 0 484322188 513654784 104580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125404 104580 603 41 0 125363 0
vsize: 501616
[startup+769.998 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112532 0 0 0 76740 268 0 0 25 0 1 0 484322188 513736704 104591 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104591 603 41 0 125383 0
vsize: 501696
[startup+779.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112539 0 0 0 77740 268 0 0 25 0 1 0 484322188 513736704 104598 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+789.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112539 0 0 0 78740 268 0 0 25 0 1 0 484322188 513736704 104598 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+799.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112539 0 0 0 79740 268 0 0 25 0 1 0 484322188 513736704 104598 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+809.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112539 0 0 0 80740 268 0 0 25 0 1 0 484322188 513736704 104598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+819.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112547 0 0 0 81740 268 0 0 25 0 1 0 484322188 513736704 104606 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104606 603 41 0 125383 0
vsize: 501696
[startup+829.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112548 0 0 0 82741 268 0 0 25 0 1 0 484322188 513736704 104607 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125424 104607 603 41 0 125383 0
vsize: 501696
[startup+839.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112564 0 0 0 83741 268 0 0 25 0 1 0 484322188 513822720 104623 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125445 104623 603 41 0 125404 0
vsize: 501780
[startup+849.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112564 0 0 0 84741 268 0 0 25 0 1 0 484322188 513822720 104623 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125445 104623 603 41 0 125404 0
vsize: 501780
[startup+859.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112568 0 0 0 85741 268 0 0 25 0 1 0 484322188 513839104 104626 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125449 104626 603 41 0 125408 0
vsize: 501796
[startup+869.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112570 0 0 0 86741 268 0 0 25 0 1 0 484322188 513855488 104627 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125453 104627 603 41 0 125412 0
vsize: 501812
[startup+879.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112578 0 0 0 87741 268 0 0 25 0 1 0 484322188 513863680 104634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125455 104634 603 41 0 125414 0
vsize: 501820
[startup+889.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112582 0 0 0 88741 268 0 0 25 0 1 0 484322188 513863680 104638 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125455 104638 603 41 0 125414 0
vsize: 501820
[startup+899.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112582 0 0 0 89742 268 0 0 25 0 1 0 484322188 513863680 104638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125455 104638 603 41 0 125414 0
vsize: 501820
[startup+909.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112585 0 0 0 90742 268 0 0 25 0 1 0 484322188 513904640 104640 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125465 104640 603 41 0 125424 0
vsize: 501860
[startup+919.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112595 0 0 0 91742 268 0 0 25 0 1 0 484322188 513974272 104650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125482 104650 603 41 0 125441 0
vsize: 501928
[startup+929.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112604 0 0 0 92742 268 0 0 25 0 1 0 484322188 513974272 104659 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125482 104659 603 41 0 125441 0
vsize: 501928
[startup+939.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112604 0 0 0 93742 268 0 0 25 0 1 0 484322188 513974272 104659 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125482 104659 603 41 0 125441 0
vsize: 501928
[startup+949.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112609 0 0 0 94743 268 0 0 25 0 1 0 484322188 513998848 104663 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125488 104663 603 41 0 125447 0
vsize: 501952
[startup+959.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112611 0 0 0 95743 268 0 0 25 0 1 0 484322188 513998848 104665 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125488 104665 603 41 0 125447 0
vsize: 501952
[startup+969.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112611 0 0 0 96743 268 0 0 25 0 1 0 484322188 513998848 104665 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125488 104665 603 41 0 125447 0
vsize: 501952
[startup+979.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112625 0 0 0 97743 268 0 0 25 0 1 0 484322188 514072576 104679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125506 104679 603 41 0 125465 0
vsize: 502024
[startup+989.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112625 0 0 0 98743 268 0 0 25 0 1 0 484322188 514072576 104679 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125506 104679 603 41 0 125465 0
vsize: 502024
[startup+999.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112626 0 0 0 99744 268 0 0 25 0 1 0 484322188 514072576 104680 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125506 104680 603 41 0 125465 0
vsize: 502024
[startup+1010 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112636 0 0 0 100744 268 0 0 25 0 1 0 484322188 514072576 104690 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125506 104690 603 41 0 125465 0
vsize: 502024
[startup+1020 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112643 0 0 0 101744 268 0 0 25 0 1 0 484322188 514162688 104697 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125528 104697 603 41 0 125487 0
vsize: 502112
[startup+1030 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112659 0 0 0 102744 269 0 0 25 0 1 0 484322188 514162688 104713 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125528 104713 603 41 0 125487 0
vsize: 502112
[startup+1040 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112659 0 0 0 103744 269 0 0 25 0 1 0 484322188 514162688 104713 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125528 104713 603 41 0 125487 0
vsize: 502112
[startup+1050 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112659 0 0 0 104744 269 0 0 25 0 1 0 484322188 514162688 104713 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125528 104713 603 41 0 125487 0
vsize: 502112
[startup+1060 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112667 0 0 0 105745 269 0 0 25 0 1 0 484322188 514240512 104721 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125547 104721 603 41 0 125506 0
vsize: 502188
[startup+1070 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112676 0 0 0 106745 269 0 0 25 0 1 0 484322188 514277376 104729 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125556 104729 603 41 0 125515 0
vsize: 502224
[startup+1080 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112680 0 0 0 107745 269 0 0 25 0 1 0 484322188 514277376 104733 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125556 104733 603 41 0 125515 0
vsize: 502224
[startup+1090 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112694 0 0 0 108745 269 0 0 25 0 1 0 484322188 514334720 104746 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125570 104746 603 41 0 125529 0
vsize: 502280
[startup+1100 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112694 0 0 0 109745 269 0 0 25 0 1 0 484322188 514334720 104746 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125570 104746 603 41 0 125529 0
vsize: 502280
[startup+1110 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112708 0 0 0 110746 269 0 0 25 0 1 0 484322188 514404352 104760 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125587 104760 603 41 0 125546 0
vsize: 502348
[startup+1120 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112708 0 0 0 111746 269 0 0 25 0 1 0 484322188 514404352 104760 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125587 104760 603 41 0 125546 0
vsize: 502348
[startup+1130 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112717 0 0 0 112746 269 0 0 25 0 1 0 484322188 514404352 104769 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125587 104769 603 41 0 125546 0
vsize: 502348
[startup+1140 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112720 0 0 0 113745 269 0 0 25 0 1 0 484322188 514404352 104772 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125587 104772 603 41 0 125546 0
vsize: 502348
[startup+1150 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112720 0 0 0 114745 269 0 0 25 0 1 0 484322188 514404352 104772 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125587 104772 603 41 0 125546 0
vsize: 502348
[startup+1160 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112727 0 0 0 115745 269 0 0 25 0 1 0 484322188 514502656 104779 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125611 104779 603 41 0 125570 0
vsize: 502444
[startup+1170 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112729 0 0 0 116745 269 0 0 25 0 1 0 484322188 514502656 104781 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125611 104781 603 41 0 125570 0
vsize: 502444
[startup+1180 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112736 0 0 0 117745 269 0 0 25 0 1 0 484322188 514502656 104788 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125611 104788 603 41 0 125570 0
vsize: 502444
[startup+1190 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112740 0 0 0 118746 269 0 0 25 0 1 0 484322188 514502656 104792 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125611 104792 603 41 0 125570 0
vsize: 502444
[startup+1200 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 24979
Raw data (stat): 24979 (minisat+) R 24978 25347 25346 0 -1 0 112758 0 0 0 119746 269 0 0 25 0 1 0 484322188 514592768 104809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125633 104809 603 41 0 125592 0
vsize: 502532
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 24979
Raw data (stat): 24979 (minisat+) Z 24978 25347 25346 0 -1 12 112761 0 0 0 119746 290 0 0 25 0 1 0 484322188 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: 10
Real time (s): 1200.21
CPU time (s): 1200.37
CPU user time (s): 1197.46
CPU system time (s): 2.90456
CPU usage (%): 100.013
Max. virtual memory (Kb): 502532
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####