PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-count.b.opb
MD5SUM	f13ba9c997276002b5bd6db1f679a6f5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	24
Optimality of the best value was proved	NO
Number of terms in the objective function	467
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	467
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	467
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	466
Total number of constraints	694
Number of constraints which are clauses	694
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	78
Trace number 5414

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 23:48:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3825 boxname=wulflinc5 idbench=65 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f13ba9c997276002b5bd6db1f679a6f5  /oldhome/oroussel/tmp/wulflinc5/normalized-count.b.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-count.b.opb /oldhome/oroussel/tmp/wulflinc5/normalized-count.b.opb
IDLAUNCH: 3825
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        901264 kB
Buffers:         33808 kB
Cached:          78228 kB
SwapCached:       2272 kB
Active:          53828 kB
Inactive:        63340 kB
HighTotal:      131008 kB
HighFree:        48860 kB
LowTotal:       903652 kB
LowFree:        852404 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10628 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:08:36 (client local time) WITH STATUS 10 IN 1200.1 SECONDS
stats: 3825 7 1200.1 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 694 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     671    16758 |     201       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  445/445          
c |         0 |     660    16327 |      --       0       --      -- |     --   | -11/-431
c |         0 |     660    16327 |     264       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.176973 s)
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17658     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   19684    60642 |    5905       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12806          
c   -- var.elim.:  2000/12806          
c   -- var.elim.:  3000/12806          
c   -- var.elim.:  4000/12806          
c   -- var.elim.:  5000/12806          
c   -- var.elim.:  6000/12806          
c   -- var.elim.:  7000/12806          
c   -- var.elim.:  8000/12806          
c   -- var.elim.:  9000/12806          
c   -- var.elim.:  10000/12806          
c   -- var.elim.:  11000/12806          
c   -- var.elim.:  12000/12806          
c   -- var.elim.:  12806/12806          
c   -- var.elim.:  1000/6359          
c   -- var.elim.:  2000/6359          
c   -- var.elim.:  3000/6359          
c   -- var.elim.:  4000/6359          
c   -- var.elim.:  5000/6359          
c   -- var.elim.:  6000/6359          
c   -- var.elim.:  6359/6359          
c   -- var.elim.:  341/341          
c   -- var.elim.:  199/199          
c   -- subsuming                       
c   -- var.elim.:  1000/4611          
c   -- var.elim.:  2000/4611          
c   -- var.elim.:  3000/4611          
c   -- var.elim.:  4000/4611          
c   -- var.elim.:  4611/4611          
c   -- var.elim.:  85/85          
c |         0 |   13337    91329 |      --       0       --      -- |     --   | -6276/30886
c |         0 |   13337    91329 |    5334       0        0     nan |  0.000 % |
c |       100 |   13221    90494 |    5817      91     5990    65.8 |  1.661 % |
c ==============================================================================
c (current CPU-time: 6.90095 s)
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       241 |   13385    90848 |    4015     229    11548    50.4 |  1.661 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1645          
c   -- var.elim.:  1645/1645          
c   -- var.elim.:  316/316          
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  34/34          
c |       241 |   13228    90555 |      --     229       --      -- |     --   | -142/-130
c |       241 |   13228    90555 |    5291     228    11533    50.6 |  1.661 % |
c |       341 |   13228    90555 |    5820     328    18021    54.9 |  1.929 % |
c |       493 |   13228    90555 |    6402     480    29786    62.1 |  1.929 % |
c ==============================================================================
c (current CPU-time: 8.01078 s)
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       694 |   13479    91196 |    4043     680    42159    62.0 |  1.929 % |
c   -- subsuming                       
c   -- var.elim.:  471/471          
c   -- var.elim.:  217/217          
c   -- var.elim.:  88/88          
c   -- var.elim.:  17/17          
c |       694 |   13256    90869 |      --     680       --      -- |     --   | -221/-322
c |       694 |   13256    90869 |    5302     680    42159    62.0 |  1.929 % |
c |       794 |   13256    90869 |    5832     780    49377    63.3 |  2.112 % |
c |       944 |   13256    90869 |    6415     930    58430    62.8 |  2.112 % |
c |      1169 |   13256    90869 |    7057    1155    77045    66.7 |  2.112 % |
c |      1507 |   13256    90869 |    7763    1493    96706    64.8 |  2.112 % |
c |      2016 |   13256    90869 |    8539    2002   143696    71.8 |  2.112 % |
c |      2775 |   13256    90869 |    9393    2761   193748    70.2 |  2.112 % |
c |      3914 |   13256    90869 |   10332    3900   273085    70.0 |  2.112 % |
c ==============================================================================
c (current CPU-time: 13.6529 s)
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5266 |   13257    90834 |    3977    5251   391396    74.5 |  2.112 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2389          
c   -- var.elim.:  2000/2389          
c   -- var.elim.:  2389/2389          
c   -- var.elim.:  1000/2382          
c   -- var.elim.:  2000/2382          
c   -- var.elim.:  2382/2382          
c   -- var.elim.:  409/409          
c   -- var.elim.:  345/345          
c   -- var.elim.:  266/266          
c   -- var.elim.:  167/167          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  830/830          
c   -- var.elim.:  20/20          
c |      5266 |   12544    82016 |      --    5251       --      -- |     --   | -252/1003
c |      5266 |   12544    82016 |    5017    3455   224846    65.1 |  2.112 % |
c |      5366 |   12544    82016 |    5519    3555   228817    64.4 |  3.580 % |
c |      5516 |   12544    82016 |    6071    3705   235960    63.7 |  3.580 % |
c |      5741 |   12544    82016 |    6678    3930   245618    62.5 |  3.580 % |
c |      6086 |   12544    82016 |    7346    4275   269597    63.1 |  3.580 % |
c |      6593 |   12544    82016 |    8080    4782   307847    64.4 |  3.580 % |
c |      7358 |   12544    82016 |    8888    5547   396203    71.4 |  3.580 % |
c |      8500 |   12544    82016 |    9777    6689   520079    77.8 |  3.580 % |
c |     10209 |   12544    82016 |   10755    8398   652332    77.7 |  3.580 % |
c |     12771 |   12544    82016 |   11831   10960   831551    75.9 |  3.580 % |
c ==============================================================================
c (current CPU-time: 23.5604 s)
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13326 |   14558    87735 |    4367   11515   885341    76.9 |  3.580 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3604          
c   -- var.elim.:  2000/3604          
c   -- var.elim.:  3000/3604          
c   -- var.elim.:  3604/3604          
c   -- var.elim.:  1000/1879          
c   -- var.elim.:  1879/1879          
c   -- var.elim.:  1000/1142          
c   -- var.elim.:  1142/1142          
c   -- var.elim.:  861/861          
c   -- var.elim.:  50/50          
c   -- subsuming                       
c |     13326 |   12578    82178 |      --   11515       --      -- |     --   | -1968/-5480
c |     13326 |   12578    82178 |    5031   11468   882803    77.0 |  3.580 % |
c |     13426 |   12578    82178 |    5534    5198   332921    64.0 |  3.718 % |
c |     13577 |   12578    82178 |    6087    5349   342427    64.0 |  3.718 % |
c |     13802 |   12578    82178 |    6696    5574   357500    64.1 |  3.718 % |
c |     14139 |   12578    82178 |    7366    5911   381279    64.5 |  3.718 % |
c |     14645 |   12578    82178 |    8102    6417   435330    67.8 |  3.718 % |
c |     15406 |   12578    82178 |    8913    7178   502787    70.0 |  3.718 % |
c |     16546 |   12578    82178 |    9804    8318   584572    70.3 |  3.718 % |
c |     18254 |   12578    82178 |   10784   10026   731920    73.0 |  3.718 % |
c |     20817 |   12578    82178 |   11863   12589  1019930    81.0 |  3.718 % |
c |     24664 |   12578    82178 |   13049   12240  1137691    92.9 |  3.718 % |
c |     30431 |   12578    82178 |   14354   12805  1475221   115.2 |  3.718 % |
c |     39080 |   12578    82178 |   15790   11454  1322004   115.4 |  3.718 % |
c |     52054 |   12578    82178 |   17369   12922  1269530    98.2 |  3.718 % |
c |     71518 |   12406    80526 |   18844   13953  1311537    94.0 |  4.335 % |
c ==============================================================================
c (current CPU-time: 173.522 s)
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     90766 |   15432    89135 |    4629   18561  2167395   116.8 |  4.335 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5503          
c   -- var.elim.:  2000/5503          
c   -- var.elim.:  3000/5503          
c   -- var.elim.:  4000/5503          
c   -- var.elim.:  5000/5503          
c   -- var.elim.:  5503/5503          
c   -- var.elim.:  1000/2977          
c   -- var.elim.:  2000/2977          
c   -- var.elim.:  2977/2977          
c   -- var.elim.:  1000/1486          
c   -- var.elim.:  1486/1486          
c   -- var.elim.:  1000/1865          
c   -- var.elim.:  1865/1865          
c   -- var.elim.:  376/376          
c   -- subsuming                       
c   -- var.elim.:  66/66          
c   -- var.elim.:  11/11          
c |     90766 |   12349    80791 |      --   18561       --      -- |     --   | -3082/-8341
c |     90766 |   12349    80791 |    4939   10409  1000184    96.1 |  4.335 % |
c |     90868 |   12349    80791 |    5433    4729   396500    83.8 |  4.447 % |
c |     91018 |   12349    80791 |    5976    4879   412572    84.6 |  4.447 % |
c |     91245 |   12349    80791 |    6574    5106   422741    82.8 |  4.447 % |
c |     91584 |   12349    80791 |    7232    5445   442304    81.2 |  4.447 % |
c |     92091 |   12349    80791 |    7955    5952   472739    79.4 |  4.447 % |
c |     92850 |   12349    80791 |    8750    6711   530784    79.1 |  4.447 % |
c |     93990 |   12349    80791 |    9625    7851   613563    78.2 |  4.447 % |
c |     95699 |   12349    80791 |   10588    9560   718846    75.2 |  4.447 % |
c |     98262 |   12349    80791 |   11647    8145   504037    61.9 |  4.447 % |
c |    102106 |   12349    80791 |   12812   11989   873448    72.9 |  4.447 % |
c |    107872 |   12349    80791 |   14093   13085  1007418    77.0 |  4.447 % |
c |    116529 |   12349    80791 |   15502   11365   926813    81.5 |  4.447 % |
c |    129503 |   12349    80791 |   17052   13033  1059399    81.3 |  4.447 % |
c |    148964 |   12324    80623 |   18720   14478  1336594    92.3 |  4.496 % |
c |    178159 |   12324    80623 |   20592   15378  1162387    75.6 |  4.496 % |
c |    221948 |   12324    80623 |   22651   17011  1317677    77.5 |  4.496 % |
c |    287633 |   12324    80623 |   24916   20874  1954985    93.7 |  4.496 % |
c |    386161 |   12324    80623 |   27408   18960  1517515    80.0 |  4.496 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 x177 -x178 -x179 x180 -x181 -x182 -x183 -x184 x185 -x186 -x187 -x188 -x189 x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 x212 -x213 -x214 -x215 -x216 -x217 -x218 x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 #### 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.92 0.95 0.90 2/54 27423
Raw data (stat): 27423 (runsolver) R 27422 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421811971 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 2855 0 0 0 989 9 0 0 25 0 1 0 421811971 11194368 2198 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2733 2198 603 41 0 2692 0
vsize: 10932
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 3758 0 0 0 1985 12 0 0 25 0 1 0 421811971 13393920 2711 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2711 603 41 0 3229 0
vsize: 13080
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 4545 0 0 0 2982 16 0 0 25 0 1 0 421811971 15089664 3178 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3684 3178 603 41 0 3643 0
vsize: 14736
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 4765 0 0 0 3980 17 0 0 25 0 1 0 421811971 16011264 3398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3909 3398 603 41 0 3868 0
vsize: 15636
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5324 0 0 0 4978 19 0 0 25 0 1 0 421811971 18268160 3957 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4460 3957 603 41 0 4419 0
vsize: 17840
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5511 0 0 0 5978 20 0 0 25 0 1 0 421811971 19058688 4144 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4144 603 41 0 4612 0
vsize: 18612
[startup+70.0049 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5631 0 0 0 6977 20 0 0 25 0 1 0 421811971 19591168 4264 4294967295 134512640 134672761 3221224576 3221223760 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4783 4264 603 41 0 4742 0
vsize: 19132
[startup+80.0057 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5632 0 0 0 7977 21 0 0 25 0 1 0 421811971 19591168 4265 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4783 4265 603 41 0 4742 0
vsize: 19132
[startup+90.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5809 0 0 0 8976 22 0 0 25 0 1 0 421811971 20365312 4441 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4441 603 41 0 4931 0
vsize: 19888
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5809 0 0 0 9975 22 0 0 25 0 1 0 421811971 20365312 4441 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4441 603 41 0 4931 0
vsize: 19888
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5810 0 0 0 10975 22 0 0 25 0 1 0 421811971 20365312 4442 4294967295 134512640 134672761 3221224576 3221223760 134615622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4442 603 41 0 4931 0
vsize: 19888
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5811 0 0 0 11975 23 0 0 25 0 1 0 421811971 20365312 4443 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4443 603 41 0 4931 0
vsize: 19888
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5811 0 0 0 12974 23 0 0 25 0 1 0 421811971 20365312 4443 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4443 603 41 0 4931 0
vsize: 19888
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 5811 0 0 0 13974 23 0 0 25 0 1 0 421811971 20365312 4443 4294967295 134512640 134672761 3221224576 3221223712 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4443 603 41 0 4931 0
vsize: 19888
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6056 0 0 0 14973 24 0 0 25 0 1 0 421811971 21430272 4688 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5232 4688 603 41 0 5191 0
vsize: 20928
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6107 0 0 0 15973 24 0 0 25 0 1 0 421811971 21565440 4739 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4739 603 41 0 5224 0
vsize: 21060
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6144 0 0 0 16973 24 0 0 25 0 1 0 421811971 21712896 4775 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5301 4775 603 41 0 5260 0
vsize: 21204
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 17969 28 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 18968 28 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 19968 29 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 20967 29 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 21967 30 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 22966 30 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 23966 30 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 24966 30 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223776 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 25966 30 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 26965 31 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 27965 31 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 28965 31 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 29964 32 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 30964 32 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 31963 32 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 32963 33 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 33963 33 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 34962 33 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 35962 33 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6813 0 0 0 36962 34 0 0 25 0 1 0 421811971 23715840 5058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5058 603 41 0 5749 0
vsize: 23160
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 37961 34 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 38961 34 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 39961 34 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 40960 35 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 41960 35 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 42960 35 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 43959 36 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 44959 36 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 45959 36 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6814 0 0 0 46958 37 0 0 25 0 1 0 421811971 23715840 5059 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5059 603 41 0 5749 0
vsize: 23160
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6826 0 0 0 47958 37 0 0 25 0 1 0 421811971 23785472 5071 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5807 5071 603 41 0 5766 0
vsize: 23228
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6826 0 0 0 48958 37 0 0 25 0 1 0 421811971 23785472 5071 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5807 5071 603 41 0 5766 0
vsize: 23228
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6826 0 0 0 49957 38 0 0 25 0 1 0 421811971 23785472 5071 4294967295 134512640 134672761 3221224576 3221223776 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5807 5071 603 41 0 5766 0
vsize: 23228
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6842 0 0 0 50957 38 0 0 25 0 1 0 421811971 23851008 5086 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5823 5086 603 41 0 5782 0
vsize: 23292
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6842 0 0 0 51957 39 0 0 25 0 1 0 421811971 23851008 5086 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5823 5086 603 41 0 5782 0
vsize: 23292
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 6906 0 0 0 52956 39 0 0 25 0 1 0 421811971 24121344 5150 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5889 5150 603 41 0 5848 0
vsize: 23556
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7017 0 0 0 53955 40 0 0 25 0 1 0 421811971 24567808 5260 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5998 5260 603 41 0 5957 0
vsize: 23992
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7017 0 0 0 54954 41 0 0 25 0 1 0 421811971 24567808 5260 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5998 5260 603 41 0 5957 0
vsize: 23992
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7034 0 0 0 55954 41 0 0 25 0 1 0 421811971 24633344 5276 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5276 603 41 0 5973 0
vsize: 24056
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7034 0 0 0 56955 41 0 0 25 0 1 0 421811971 24633344 5276 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5276 603 41 0 5973 0
vsize: 24056
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7034 0 0 0 57955 41 0 0 25 0 1 0 421811971 24633344 5276 4294967295 134512640 134672761 3221224576 3221223616 134614348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5276 603 41 0 5973 0
vsize: 24056
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7037 0 0 0 58955 41 0 0 25 0 1 0 421811971 24637440 5278 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6015 5278 603 41 0 5974 0
vsize: 24060
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7037 0 0 0 59955 41 0 0 25 0 1 0 421811971 24637440 5278 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6015 5278 603 41 0 5974 0
vsize: 24060
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7037 0 0 0 60955 41 0 0 25 0 1 0 421811971 24637440 5278 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6015 5278 603 41 0 5974 0
vsize: 24060
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7091 0 0 0 61955 41 0 0 25 0 1 0 421811971 24862720 5332 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6070 5332 603 41 0 6029 0
vsize: 24280
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7091 0 0 0 62956 41 0 0 25 0 1 0 421811971 24862720 5332 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6070 5332 603 41 0 6029 0
vsize: 24280
[startup+640.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7189 0 0 0 63956 41 0 0 25 0 1 0 421811971 25260032 5430 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5430 603 41 0 6126 0
vsize: 24668
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7348 0 0 0 64955 42 0 0 25 0 1 0 421811971 25899008 5589 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5589 603 41 0 6282 0
vsize: 25292
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7348 0 0 0 65955 42 0 0 25 0 1 0 421811971 25899008 5589 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5589 603 41 0 6282 0
vsize: 25292
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7348 0 0 0 66956 42 0 0 25 0 1 0 421811971 25899008 5589 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5589 603 41 0 6282 0
vsize: 25292
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27423
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7350 0 0 0 67956 42 0 0 25 0 1 0 421811971 25899008 5591 4294967295 134512640 134672761 3221224576 3221223672 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5591 603 41 0 6282 0
vsize: 25292
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27426
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7350 0 0 0 68956 42 0 0 25 0 1 0 421811971 25899008 5591 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5591 603 41 0 6282 0
vsize: 25292
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7350 0 0 0 69956 42 0 0 25 0 1 0 421811971 25899008 5591 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5591 603 41 0 6282 0
vsize: 25292
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7351 0 0 0 70956 42 0 0 25 0 1 0 421811971 25899008 5592 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5592 603 41 0 6282 0
vsize: 25292
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7377 0 0 0 71956 42 0 0 25 0 1 0 421811971 26013696 5618 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5618 603 41 0 6310 0
vsize: 25404
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7377 0 0 0 72956 42 0 0 25 0 1 0 421811971 26013696 5618 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5618 603 41 0 6310 0
vsize: 25404
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7377 0 0 0 73956 42 0 0 25 0 1 0 421811971 26013696 5618 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5618 603 41 0 6310 0
vsize: 25404
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7377 0 0 0 74956 42 0 0 25 0 1 0 421811971 26013696 5618 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5618 603 41 0 6310 0
vsize: 25404
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27476
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7377 0 0 0 75957 42 0 0 25 0 1 0 421811971 26013696 5618 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5618 603 41 0 6310 0
vsize: 25404
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7377 0 0 0 76957 42 0 0 25 0 1 0 421811971 26013696 5618 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5618 603 41 0 6310 0
vsize: 25404
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7443 0 0 0 77957 42 0 0 25 0 1 0 421811971 26275840 5684 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5684 603 41 0 6374 0
vsize: 25660
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7482 0 0 0 78957 42 0 0 25 0 1 0 421811971 26439680 5722 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6455 5722 603 41 0 6414 0
vsize: 25820
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7482 0 0 0 79957 42 0 0 25 0 1 0 421811971 26439680 5722 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6455 5722 603 41 0 6414 0
vsize: 25820
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7482 0 0 0 80958 42 0 0 25 0 1 0 421811971 26439680 5722 4294967295 134512640 134672761 3221224576 3221223344 1075352301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6455 5722 603 41 0 6414 0
vsize: 25820
[startup+820.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7543 0 0 0 81958 42 0 0 25 0 1 0 421811971 26689536 5783 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6516 5783 603 41 0 6475 0
vsize: 26064
[startup+830.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7543 0 0 0 82958 42 0 0 25 0 1 0 421811971 26689536 5783 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6516 5783 603 41 0 6475 0
vsize: 26064
[startup+840.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7543 0 0 0 83958 42 0 0 25 0 1 0 421811971 26689536 5783 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6516 5783 603 41 0 6475 0
vsize: 26064
[startup+850.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7556 0 0 0 84958 42 0 0 25 0 1 0 421811971 26738688 5795 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6528 5795 603 41 0 6487 0
vsize: 26112
[startup+860.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7556 0 0 0 85958 42 0 0 25 0 1 0 421811971 26738688 5795 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6528 5795 603 41 0 6487 0
vsize: 26112
[startup+870.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7556 0 0 0 86958 42 0 0 25 0 1 0 421811971 26738688 5795 4294967295 134512640 134672761 3221224576 3221223776 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6528 5795 603 41 0 6487 0
vsize: 26112
[startup+880.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7565 0 0 0 87959 42 0 0 25 0 1 0 421811971 26771456 5803 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6536 5803 603 41 0 6495 0
vsize: 26144
[startup+890.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7565 0 0 0 88959 42 0 0 25 0 1 0 421811971 26771456 5803 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6536 5803 603 41 0 6495 0
vsize: 26144
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7565 0 0 0 89959 42 0 0 25 0 1 0 421811971 26771456 5803 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6536 5803 603 41 0 6495 0
vsize: 26144
[startup+910.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7609 0 0 0 90959 43 0 0 25 0 1 0 421811971 26931200 5846 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5846 603 41 0 6534 0
vsize: 26300
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7609 0 0 0 91959 43 0 0 25 0 1 0 421811971 26931200 5846 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5846 603 41 0 6534 0
vsize: 26300
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7609 0 0 0 92959 43 0 0 25 0 1 0 421811971 26931200 5846 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5846 603 41 0 6534 0
vsize: 26300
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7609 0 0 0 93960 43 0 0 25 0 1 0 421811971 26931200 5846 4294967295 134512640 134672761 3221224576 3221223712 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5846 603 41 0 6534 0
vsize: 26300
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7625 0 0 0 94960 43 0 0 25 0 1 0 421811971 26992640 5861 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6590 5861 603 41 0 6549 0
vsize: 26360
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7625 0 0 0 95960 43 0 0 25 0 1 0 421811971 26992640 5861 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6590 5861 603 41 0 6549 0
vsize: 26360
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7625 0 0 0 96960 43 0 0 25 0 1 0 421811971 26992640 5861 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6590 5861 603 41 0 6549 0
vsize: 26360
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7649 0 0 0 97960 43 0 0 25 0 1 0 421811971 27156480 5885 4294967295 134512640 134672761 3221224576 3221223632 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5885 603 41 0 6589 0
vsize: 26520
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7649 0 0 0 98960 43 0 0 25 0 1 0 421811971 27090944 5885 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6614 5885 603 41 0 6573 0
vsize: 26456
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7649 0 0 0 99961 43 0 0 25 0 1 0 421811971 27090944 5885 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6614 5885 603 41 0 6573 0
vsize: 26456
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7649 0 0 0 100961 43 0 0 25 0 1 0 421811971 27090944 5885 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6614 5885 603 41 0 6573 0
vsize: 26456
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27478
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 101961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 102961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223616 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 103961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 104961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 105961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 106961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 107961 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 108962 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 109962 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7657 0 0 0 110962 43 0 0 25 0 1 0 421811971 27123712 5892 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5892 603 41 0 6581 0
vsize: 26488
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7667 0 0 0 111962 43 0 0 25 0 1 0 421811971 27156480 5901 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5901 603 41 0 6589 0
vsize: 26520
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7667 0 0 0 112962 43 0 0 25 0 1 0 421811971 27156480 5901 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5901 603 41 0 6589 0
vsize: 26520
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7667 0 0 0 113963 43 0 0 25 0 1 0 421811971 27156480 5901 4294967295 134512640 134672761 3221224576 3221223616 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5901 603 41 0 6589 0
vsize: 26520
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7667 0 0 0 114963 43 0 0 25 0 1 0 421811971 27156480 5901 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5901 603 41 0 6589 0
vsize: 26520
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7667 0 0 0 115963 43 0 0 25 0 1 0 421811971 27156480 5901 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5901 603 41 0 6589 0
vsize: 26520
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 7667 0 0 0 116963 43 0 0 25 0 1 0 421811971 27156480 5901 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5901 603 41 0 6589 0
vsize: 26520
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 8033 0 0 0 117962 44 0 0 25 0 1 0 421811971 28753920 6267 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7020 6267 603 41 0 6979 0
vsize: 28080
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 8132 0 0 0 118962 44 0 0 25 0 1 0 421811971 29065216 6365 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7096 6365 603 41 0 7055 0
vsize: 28384
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27480
Raw data (stat): 27423 (minisat+) R 27422 24215 24214 0 -1 0 8132 0 0 0 119962 44 0 0 25 0 1 0 421811971 29065216 6365 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7096 6365 603 41 0 7055 0
vsize: 28384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27480
Raw data (stat): 27423 (minisat+) Z 27422 24215 24214 0 -1 12 8133 0 0 0 119963 46 0 0 25 0 1 0 421811971 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.06
CPU time (s): 1200.1
CPU user time (s): 1199.63
CPU system time (s): 0.464929
CPU usage (%): 100.003
Max. virtual memory (Kb): 28384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####