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/miplib3/normalized-mps-v2-13-7-misc07.opb
MD5SUM54df16ee65da54d5975ffedee80d2bb9
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 18085 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 13:30:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18589 boxname=wulflinc28 idbench=1430 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  54df16ee65da54d5975ffedee80d2bb9  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 18589
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        526672 kB
Buffers:         31608 kB
Cached:         449116 kB
SwapCached:        104 kB
Active:         190780 kB
Inactive:       292396 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        526420 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19216 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:50:55 (client local time) WITH STATUS 10 IN 1200.39 SECONDS
stats: 18589 7 1200.39 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.81 0.95 0.90 2/54 26791
Raw data (stat): 26791 (runsolver) R 26790 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545460504 1052672 99 4294967295 134512640 135381576 3221224432 3221219684 134863769 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.84 0.95 0.90 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 51884 0 0 0 879 119 0 0 25 0 1 0 545460504 215732224 43952 4294967295 134512640 134672761 3221224544 3221145472 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52669 43953 603 41 0 52628 0
vsize: 210676
[startup+20.002 s]
Raw data (loadavg): 0.86 0.95 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 106121 0 0 0 1745 254 0 0 25 0 1 0 545460504 487071744 98189 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118914 98189 603 41 0 118873 0
vsize: 475656
[startup+30.0022 s]
Raw data (loadavg): 0.88 0.95 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 110375 0 0 0 2736 262 0 0 25 0 1 0 545460504 500723712 102443 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.0024 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 110518 0 0 0 3736 262 0 0 25 0 1 0 545460504 500994048 102586 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122313 102586 603 41 0 122272 0
vsize: 489252
[startup+50.0031 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112034 0 0 0 4731 266 0 0 25 0 1 0 545460504 506544128 104102 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0033 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112038 0 0 0 5731 267 0 0 25 0 1 0 545460504 511385600 104106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124850 104106 603 41 0 124809 0
vsize: 499400
[startup+70.0042 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112050 0 0 0 6731 267 0 0 25 0 1 0 545460504 511459328 104118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124868 104118 603 41 0 124827 0
vsize: 499472
[startup+80.0041 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112051 0 0 0 7731 267 0 0 25 0 1 0 545460504 511459328 104119 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0043 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112056 0 0 0 8731 267 0 0 25 0 1 0 545460504 511459328 104124 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124868 104124 603 41 0 124827 0
vsize: 499472
[startup+100.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112077 0 0 0 9731 267 0 0 25 0 1 0 545460504 511569920 104145 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124895 104145 603 41 0 124854 0
vsize: 499580
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112083 0 0 0 10731 267 0 0 25 0 1 0 545460504 511569920 104151 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124895 104151 603 41 0 124854 0
vsize: 499580
[startup+120.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112101 0 0 0 11731 267 0 0 25 0 1 0 545460504 511569920 104169 4294967295 134512640 134672761 3221224544 3221223696 1074743855 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.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112104 0 0 0 12731 267 0 0 25 0 1 0 545460504 511705088 104172 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124928 104172 603 41 0 124887 0
vsize: 499712
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112108 0 0 0 13731 267 0 0 25 0 1 0 545460504 511705088 104176 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124928 104176 603 41 0 124887 0
vsize: 499712
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112168 0 0 0 14731 267 0 0 25 0 1 0 545460504 512339968 104236 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125083 104236 603 41 0 125042 0
vsize: 500332
[startup+160.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112205 0 0 0 15731 267 0 0 25 0 1 0 545460504 512434176 104273 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125106 104273 603 41 0 125065 0
vsize: 500424
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112215 0 0 0 16732 267 0 0 25 0 1 0 545460504 512434176 104283 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125106 104283 603 41 0 125065 0
vsize: 500424
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112217 0 0 0 17732 267 0 0 25 0 1 0 545460504 512434176 104285 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125106 104285 603 41 0 125065 0
vsize: 500424
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112227 0 0 0 18732 267 0 0 25 0 1 0 545460504 512491520 104294 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125120 104294 603 41 0 125079 0
vsize: 500480
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112228 0 0 0 19732 267 0 0 25 0 1 0 545460504 512491520 104295 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125120 104295 603 41 0 125079 0
vsize: 500480
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112228 0 0 0 20732 267 0 0 25 0 1 0 545460504 512491520 104295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125120 104295 603 41 0 125079 0
vsize: 500480
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112245 0 0 0 21732 267 0 0 25 0 1 0 545460504 512548864 104311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112245 0 0 0 22733 267 0 0 25 0 1 0 545460504 512548864 104311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112245 0 0 0 23733 267 0 0 25 0 1 0 545460504 512548864 104311 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112245 0 0 0 24733 267 0 0 25 0 1 0 545460504 512548864 104311 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125134 104311 603 41 0 125093 0
vsize: 500536
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112277 0 0 0 25733 267 0 0 25 0 1 0 545460504 512741376 104343 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104343 603 41 0 125140 0
vsize: 500724
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112282 0 0 0 26733 267 0 0 25 0 1 0 545460504 512741376 104348 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104348 603 41 0 125140 0
vsize: 500724
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112290 0 0 0 27733 267 0 0 25 0 1 0 545460504 512741376 104356 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112290 0 0 0 28734 267 0 0 25 0 1 0 545460504 512741376 104356 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112290 0 0 0 29734 267 0 0 25 0 1 0 545460504 512741376 104356 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112290 0 0 0 30734 267 0 0 25 0 1 0 545460504 512741376 104356 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104356 603 41 0 125140 0
vsize: 500724
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112291 0 0 0 31734 267 0 0 25 0 1 0 545460504 512741376 104357 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104357 603 41 0 125140 0
vsize: 500724
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112291 0 0 0 32735 267 0 0 25 0 1 0 545460504 512741376 104357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104357 603 41 0 125140 0
vsize: 500724
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112291 0 0 0 33735 267 0 0 25 0 1 0 545460504 512741376 104357 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104357 603 41 0 125140 0
vsize: 500724
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112292 0 0 0 34735 267 0 0 25 0 1 0 545460504 512741376 104358 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104358 603 41 0 125140 0
vsize: 500724
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112298 0 0 0 35735 267 0 0 25 0 1 0 545460504 512741376 104364 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125181 104364 603 41 0 125140 0
vsize: 500724
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112310 0 0 0 36735 268 0 0 25 0 1 0 545460504 512860160 104376 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125210 104376 603 41 0 125169 0
vsize: 500840
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112310 0 0 0 37735 268 0 0 25 0 1 0 545460504 512860160 104376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125210 104376 603 41 0 125169 0
vsize: 500840
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112325 0 0 0 38736 268 0 0 25 0 1 0 545460504 512860160 104391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125210 104391 603 41 0 125169 0
vsize: 500840
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112338 0 0 0 39736 268 0 0 25 0 1 0 545460504 512942080 104404 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125230 104404 603 41 0 125189 0
vsize: 500920
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112340 0 0 0 40736 268 0 0 25 0 1 0 545460504 512942080 104406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125230 104406 603 41 0 125189 0
vsize: 500920
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112350 0 0 0 41736 268 0 0 25 0 1 0 545460504 512958464 104415 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125234 104415 603 41 0 125193 0
vsize: 500936
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112356 0 0 0 42736 268 0 0 25 0 1 0 545460504 512991232 104420 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125242 104420 603 41 0 125201 0
vsize: 500968
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112358 0 0 0 43737 268 0 0 25 0 1 0 545460504 512991232 104422 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125242 104422 603 41 0 125201 0
vsize: 500968
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112358 0 0 0 44737 268 0 0 25 0 1 0 545460504 512991232 104422 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125242 104422 603 41 0 125201 0
vsize: 500968
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112366 0 0 0 45737 268 0 0 25 0 1 0 545460504 513048576 104429 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125256 104429 603 41 0 125215 0
vsize: 501024
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112366 0 0 0 46737 268 0 0 25 0 1 0 545460504 513048576 104429 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125256 104429 603 41 0 125215 0
vsize: 501024
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112379 0 0 0 47737 268 0 0 25 0 1 0 545460504 513118208 104442 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125273 104442 603 41 0 125232 0
vsize: 501092
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112381 0 0 0 48737 268 0 0 25 0 1 0 545460504 513118208 104444 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112381 0 0 0 49738 268 0 0 25 0 1 0 545460504 513118208 104444 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112381 0 0 0 50738 268 0 0 25 0 1 0 545460504 513118208 104444 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125273 104444 603 41 0 125232 0
vsize: 501092
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112386 0 0 0 51738 268 0 0 25 0 1 0 545460504 513118208 104449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125273 104449 603 41 0 125232 0
vsize: 501092
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112394 0 0 0 52738 268 0 0 25 0 1 0 545460504 513196032 104457 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125292 104457 603 41 0 125251 0
vsize: 501168
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112400 0 0 0 53738 268 0 0 25 0 1 0 545460504 513196032 104463 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125292 104463 603 41 0 125251 0
vsize: 501168
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112400 0 0 0 54738 268 0 0 25 0 1 0 545460504 513196032 104463 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125292 104463 603 41 0 125251 0
vsize: 501168
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112400 0 0 0 55738 268 0 0 25 0 1 0 545460504 513196032 104463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125292 104463 603 41 0 125251 0
vsize: 501168
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112421 0 0 0 56738 268 0 0 25 0 1 0 545460504 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+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112427 0 0 0 57738 268 0 0 25 0 1 0 545460504 513306624 104490 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104490 603 41 0 125278 0
vsize: 501276
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112427 0 0 0 58738 268 0 0 25 0 1 0 545460504 513306624 104490 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104490 603 41 0 125278 0
vsize: 501276
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112429 0 0 0 59739 268 0 0 25 0 1 0 545460504 513306624 104492 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104492 603 41 0 125278 0
vsize: 501276
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112429 0 0 0 60739 268 0 0 25 0 1 0 545460504 513306624 104492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104492 603 41 0 125278 0
vsize: 501276
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112431 0 0 0 61739 268 0 0 25 0 1 0 545460504 513306624 104494 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104494 603 41 0 125278 0
vsize: 501276
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112432 0 0 0 62739 268 0 0 25 0 1 0 545460504 513306624 104495 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125319 104495 603 41 0 125278 0
vsize: 501276
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112444 0 0 0 63739 268 0 0 25 0 1 0 545460504 513380352 104507 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125337 104507 603 41 0 125296 0
vsize: 501348
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112447 0 0 0 64739 268 0 0 25 0 1 0 545460504 513380352 104510 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125337 104510 603 41 0 125296 0
vsize: 501348
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112448 0 0 0 65739 268 0 0 25 0 1 0 545460504 513380352 104511 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125337 104511 603 41 0 125296 0
vsize: 501348
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112450 0 0 0 66739 268 0 0 25 0 1 0 545460504 513380352 104513 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125337 104513 603 41 0 125296 0
vsize: 501348
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112451 0 0 0 67740 268 0 0 25 0 1 0 545460504 513380352 104514 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125337 104514 603 41 0 125296 0
vsize: 501348
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112472 0 0 0 68740 268 0 0 25 0 1 0 545460504 513454080 104535 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125355 104535 603 41 0 125314 0
vsize: 501420
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112472 0 0 0 69740 268 0 0 25 0 1 0 545460504 513454080 104535 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125355 104535 603 41 0 125314 0
vsize: 501420
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112478 0 0 0 70740 268 0 0 25 0 1 0 545460504 513503232 104540 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125367 104540 603 41 0 125326 0
vsize: 501468
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112494 0 0 0 71740 268 0 0 25 0 1 0 545460504 513531904 104555 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125374 104555 603 41 0 125333 0
vsize: 501496
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112504 0 0 0 72741 268 0 0 25 0 1 0 545460504 513597440 104564 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125390 104564 603 41 0 125349 0
vsize: 501560
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112504 0 0 0 73741 268 0 0 25 0 1 0 545460504 513597440 104564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125390 104564 603 41 0 125349 0
vsize: 501560
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112521 0 0 0 74741 268 0 0 25 0 1 0 545460504 513654784 104580 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125404 104580 603 41 0 125363 0
vsize: 501616
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112521 0 0 0 75741 268 0 0 25 0 1 0 545460504 513654784 104580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125404 104580 603 41 0 125363 0
vsize: 501616
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112521 0 0 0 76741 268 0 0 25 0 1 0 545460504 513654784 104580 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125404 104580 603 41 0 125363 0
vsize: 501616
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112532 0 0 0 77741 268 0 0 25 0 1 0 545460504 513736704 104591 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104591 603 41 0 125383 0
vsize: 501696
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112539 0 0 0 78742 268 0 0 25 0 1 0 545460504 513736704 104598 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112539 0 0 0 79741 268 0 0 25 0 1 0 545460504 513736704 104598 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112539 0 0 0 80742 268 0 0 25 0 1 0 545460504 513736704 104598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112539 0 0 0 81742 268 0 0 25 0 1 0 545460504 513736704 104598 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104598 603 41 0 125383 0
vsize: 501696
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112547 0 0 0 82742 268 0 0 25 0 1 0 545460504 513736704 104606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104606 603 41 0 125383 0
vsize: 501696
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112548 0 0 0 83742 268 0 0 25 0 1 0 545460504 513736704 104607 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125424 104607 603 41 0 125383 0
vsize: 501696
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112564 0 0 0 84742 268 0 0 25 0 1 0 545460504 513822720 104623 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125445 104623 603 41 0 125404 0
vsize: 501780
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112564 0 0 0 85743 268 0 0 25 0 1 0 545460504 513822720 104623 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125445 104623 603 41 0 125404 0
vsize: 501780
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112568 0 0 0 86743 268 0 0 25 0 1 0 545460504 513839104 104626 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125449 104626 603 41 0 125408 0
vsize: 501796
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112570 0 0 0 87743 269 0 0 25 0 1 0 545460504 513855488 104627 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125453 104627 603 41 0 125412 0
vsize: 501812
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112578 0 0 0 88743 269 0 0 25 0 1 0 545460504 513863680 104634 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125455 104634 603 41 0 125414 0
vsize: 501820
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112578 0 0 0 89743 269 0 0 25 0 1 0 545460504 513863680 104634 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125455 104634 603 41 0 125414 0
vsize: 501820
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112582 0 0 0 90743 269 0 0 25 0 1 0 545460504 513863680 104638 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125455 104638 603 41 0 125414 0
vsize: 501820
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112585 0 0 0 91744 269 0 0 25 0 1 0 545460504 513904640 104640 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125465 104640 603 41 0 125424 0
vsize: 501860
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112595 0 0 0 92744 269 0 0 25 0 1 0 545460504 513974272 104650 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125482 104650 603 41 0 125441 0
vsize: 501928
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112604 0 0 0 93744 269 0 0 25 0 1 0 545460504 513974272 104659 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125482 104659 603 41 0 125441 0
vsize: 501928
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112604 0 0 0 94744 269 0 0 25 0 1 0 545460504 513974272 104659 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125482 104659 603 41 0 125441 0
vsize: 501928
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112609 0 0 0 95744 269 0 0 25 0 1 0 545460504 513998848 104663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125488 104663 603 41 0 125447 0
vsize: 501952
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112611 0 0 0 96744 269 0 0 25 0 1 0 545460504 513998848 104665 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125488 104665 603 41 0 125447 0
vsize: 501952
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112611 0 0 0 97745 269 0 0 25 0 1 0 545460504 513998848 104665 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125488 104665 603 41 0 125447 0
vsize: 501952
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112625 0 0 0 98745 269 0 0 25 0 1 0 545460504 514072576 104679 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125506 104679 603 41 0 125465 0
vsize: 502024
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112625 0 0 0 99745 269 0 0 25 0 1 0 545460504 514072576 104679 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125506 104679 603 41 0 125465 0
vsize: 502024
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112626 0 0 0 100745 269 0 0 25 0 1 0 545460504 514072576 104680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125506 104680 603 41 0 125465 0
vsize: 502024
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112636 0 0 0 101745 269 0 0 25 0 1 0 545460504 514072576 104690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125506 104690 603 41 0 125465 0
vsize: 502024
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112636 0 0 0 102746 269 0 0 25 0 1 0 545460504 514072576 104690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125506 104690 603 41 0 125465 0
vsize: 502024
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112657 0 0 0 103746 269 0 0 25 0 1 0 545460504 514162688 104711 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125528 104711 603 41 0 125487 0
vsize: 502112
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112659 0 0 0 104746 269 0 0 25 0 1 0 545460504 514162688 104713 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125528 104713 603 41 0 125487 0
vsize: 502112
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112659 0 0 0 105746 269 0 0 25 0 1 0 545460504 514162688 104713 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125528 104713 603 41 0 125487 0
vsize: 502112
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112667 0 0 0 106746 269 0 0 25 0 1 0 545460504 514240512 104721 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125547 104721 603 41 0 125506 0
vsize: 502188
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112676 0 0 0 107746 269 0 0 25 0 1 0 545460504 514277376 104729 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125556 104729 603 41 0 125515 0
vsize: 502224
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112677 0 0 0 108747 269 0 0 25 0 1 0 545460504 514277376 104730 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125556 104730 603 41 0 125515 0
vsize: 502224
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112694 0 0 0 109747 269 0 0 25 0 1 0 545460504 514334720 104746 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125570 104746 603 41 0 125529 0
vsize: 502280
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112694 0 0 0 110747 269 0 0 25 0 1 0 545460504 514334720 104746 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125570 104746 603 41 0 125529 0
vsize: 502280
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112705 0 0 0 111747 269 0 0 25 0 1 0 545460504 514404352 104757 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125587 104757 603 41 0 125546 0
vsize: 502348
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112708 0 0 0 112747 269 0 0 25 0 1 0 545460504 514404352 104760 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125587 104760 603 41 0 125546 0
vsize: 502348
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112717 0 0 0 113748 269 0 0 25 0 1 0 545460504 514404352 104769 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125587 104769 603 41 0 125546 0
vsize: 502348
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112718 0 0 0 114747 269 0 0 25 0 1 0 545460504 514404352 104770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125587 104770 603 41 0 125546 0
vsize: 502348
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112720 0 0 0 115748 269 0 0 25 0 1 0 545460504 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+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112720 0 0 0 116748 269 0 0 25 0 1 0 545460504 514404352 104772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125587 104772 603 41 0 125546 0
vsize: 502348
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112729 0 0 0 117748 269 0 0 25 0 1 0 545460504 514502656 104781 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125611 104781 603 41 0 125570 0
vsize: 502444
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112730 0 0 0 118748 269 0 0 25 0 1 0 545460504 514502656 104782 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125611 104782 603 41 0 125570 0
vsize: 502444
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26791
Raw data (stat): 26791 (minisat+) R 26790 10614 10613 0 -1 0 112737 0 0 0 119748 269 0 0 25 0 1 0 545460504 514502656 104789 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125611 104789 603 41 0 125570 0
vsize: 502444
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 26791
Raw data (stat): 26791 (minisat+) Z 26790 10614 10613 0 -1 12 112740 0 0 0 119748 290 0 0 25 0 1 0 545460504 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.24
CPU time (s): 1200.39
CPU user time (s): 1197.49
CPU system time (s): 2.90156
CPU usage (%): 100.013
Max. virtual memory (Kb): 502444
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####