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-f51m.b.opb
MD5SUM	4fc22abde8250807abd95442a25fac44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	18
Optimality of the best value was proved	NO
Number of terms in the objective function	407
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	407
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	407
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.02684
Number of variables	406
Total number of constraints	538
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	18
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 5804

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 01:51:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4205 boxname=wulflinc32 idbench=69 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fc22abde8250807abd95442a25fac44  /oldhome/oroussel/tmp/wulflinc32/normalized-f51m.b.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc32/normalized-f51m.b.opb /oldhome/oroussel/tmp/wulflinc32/normalized-f51m.b.opb
IDLAUNCH: 4205
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        705164 kB
Buffers:         35176 kB
Cached:         182844 kB
SwapCached:       1212 kB
Active:         146516 kB
Inactive:       151888 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        704908 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25368 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:11:20 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4205 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 498 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     498    13351 |     166       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:14920     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   16604    50904 |    5534       1       18    18.0 |  0.000 % |
c |       101 |   16604    50904 |    6087     101     2898    28.7 |  0.055 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       208 |   16615    50935 |    5538     187    12825    68.6 |  0.055 % |
c |       309 |   16615    50935 |    6091     288    21975    76.3 |  0.192 % |
c |       459 |   16615    50935 |    6700     438    33909    77.4 |  0.192 % |
c |       686 |   16615    50935 |    7371     665    58415    87.8 |  0.192 % |
c |      1029 |   16615    50935 |    8108    1008    95310    94.6 |  0.192 % |
c |      1536 |   16615    50935 |    8919    1515   138105    91.2 |  0.192 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1913 |   16410    50460 |    5470    1862   174770    93.9 |  0.192 % |
c |      2013 |   16410    50460 |    6017    1962   183811    93.7 |  1.618 % |
c |      2163 |   16402    50444 |    6618    2111   189584    89.8 |  1.655 % |
c |      2388 |   16402    50444 |    7280    2336   201318    86.2 |  1.655 % |
c |      2726 |   16402    50444 |    8008    2674   217793    81.4 |  1.655 % |
c |      3232 |   16402    50444 |    8809    3180   247166    77.7 |  1.655 % |
c |      3992 |   16402    50444 |    9690    3940   279064    70.8 |  1.655 % |
c |      5131 |   16402    50444 |   10659    5079   327949    64.6 |  1.655 % |
c |      6839 |   16402    50444 |   11725    6787   409251    60.3 |  1.655 % |
c |      9401 |   16402    50444 |   12897    9349   513437    54.9 |  1.655 % |
c |     13245 |   16402    50444 |   14187   13193   698978    53.0 |  1.655 % |
c |     19011 |   16402    50444 |   15606   11519   497107    43.2 |  1.655 % |
c |     27660 |   16402    50444 |   17167   12053   609989    50.6 |  1.655 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33376 |   16414    50475 |    5471   17769   928999    52.3 |  1.655 % |
c |     33478 |   16414    50475 |    6018    4545   221744    48.8 |  1.663 % |
c |     33628 |   16414    50475 |    6619    4695   229759    48.9 |  1.663 % |
c |     33855 |   16414    50475 |    7281    4922   240660    48.9 |  1.663 % |
c |     34192 |   16414    50475 |    8010    5259   254469    48.4 |  1.663 % |
c |     34700 |   16414    50475 |    8811    5767   274708    47.6 |  1.663 % |
c |     35461 |   16414    50475 |    9692    6528   308203    47.2 |  1.663 % |
c |     36601 |   16414    50475 |   10661    7668   361716    47.2 |  1.663 % |
c |     38309 |   16414    50475 |   11727    9376   425326    45.4 |  1.663 % |
c |     40871 |   16414    50475 |   12900   11938   539786    45.2 |  1.663 % |
c |     44717 |   16414    50475 |   14190    9168   330073    36.0 |  1.663 % |
c |     50487 |   16414    50475 |   15609    7682   245410    31.9 |  1.663 % |
c |     59136 |   16414    50475 |   17170    8283   287557    34.7 |  1.663 % |
c |     72111 |   16414    50475 |   18887   12406   433973    35.0 |  1.663 % |
c |     91574 |   16414    50475 |   20776   12488   450296    36.1 |  1.663 % |
c |    120768 |   16414    50475 |   22853   20303   750005    36.9 |  1.663 % |
c |    164558 |   16414    50475 |   25139   17290   577512    33.4 |  1.663 % |
c |    230246 |   16414    50475 |   27653   18531   543896    29.4 |  1.663 % |
c |    328772 |   16414    50475 |   30418   14118   592755    42.0 |  1.663 % |
#### 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.98 0.92 2/53 14123
Raw data (stat): 14123 (runsolver) R 14122 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480764910 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 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.0006 s]
Raw data (loadavg): 0.93 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 1579 0 0 0 992 5 0 0 25 0 1 0 480764910 8355840 1553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2040 1553 603 41 0 1999 0
vsize: 8160
[startup+20.0023 s]
Raw data (loadavg): 0.94 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 1845 0 0 0 1991 6 0 0 25 0 1 0 480764910 9453568 1819 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2308 1819 603 41 0 2267 0
vsize: 9232
[startup+30.0031 s]
Raw data (loadavg): 0.95 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2113 0 0 0 2990 8 0 0 25 0 1 0 480764910 10539008 2087 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2573 2087 603 41 0 2532 0
vsize: 10292
[startup+40.0046 s]
Raw data (loadavg): 0.96 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2121 0 0 0 3990 8 0 0 25 0 1 0 480764910 10539008 2095 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2573 2095 603 41 0 2532 0
vsize: 10292
[startup+50.0056 s]
Raw data (loadavg): 0.96 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2140 0 0 0 4989 8 0 0 25 0 1 0 480764910 10674176 2114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2606 2114 603 41 0 2565 0
vsize: 10424
[startup+60.0064 s]
Raw data (loadavg): 0.97 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2173 0 0 0 5989 9 0 0 25 0 1 0 480764910 10805248 2147 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2638 2147 603 41 0 2597 0
vsize: 10552
[startup+70.0068 s]
Raw data (loadavg): 0.97 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2286 0 0 0 6988 10 0 0 25 0 1 0 480764910 11341824 2260 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2769 2260 603 41 0 2728 0
vsize: 11076
[startup+80.0076 s]
Raw data (loadavg): 0.98 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2412 0 0 0 7987 11 0 0 25 0 1 0 480764910 11866112 2386 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2386 603 41 0 2856 0
vsize: 11588
[startup+90.0081 s]
Raw data (loadavg): 0.98 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2412 0 0 0 8988 11 0 0 25 0 1 0 480764910 11866112 2386 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2386 603 41 0 2856 0
vsize: 11588
[startup+100.009 s]
Raw data (loadavg): 0.98 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2412 0 0 0 9988 11 0 0 25 0 1 0 480764910 11866112 2386 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2386 603 41 0 2856 0
vsize: 11588
[startup+110.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2412 0 0 0 10988 11 0 0 25 0 1 0 480764910 11866112 2386 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2386 603 41 0 2856 0
vsize: 11588
[startup+120.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2421 0 0 0 11988 11 0 0 25 0 1 0 480764910 11866112 2395 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2897 2395 603 41 0 2856 0
vsize: 11588
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2425 0 0 0 12988 11 0 0 25 0 1 0 480764910 11866112 2399 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2399 603 41 0 2856 0
vsize: 11588
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2433 0 0 0 13988 11 0 0 25 0 1 0 480764910 12013568 2407 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2933 2407 603 41 0 2892 0
vsize: 11732
[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2433 0 0 0 14988 11 0 0 25 0 1 0 480764910 12013568 2407 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2933 2407 603 41 0 2892 0
vsize: 11732
[startup+160.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2463 0 0 0 15988 11 0 0 25 0 1 0 480764910 12177408 2437 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2973 2437 603 41 0 2932 0
vsize: 11892
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2476 0 0 0 16988 11 0 0 25 0 1 0 480764910 12177408 2450 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2973 2450 603 41 0 2932 0
vsize: 11892
[startup+180.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2476 0 0 0 17989 11 0 0 25 0 1 0 480764910 12177408 2450 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2973 2450 603 41 0 2932 0
vsize: 11892
[startup+190.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2484 0 0 0 18989 11 0 0 25 0 1 0 480764910 12177408 2458 4294967295 134512640 134672761 3221224560 3221223664 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2973 2458 603 41 0 2932 0
vsize: 11892
[startup+200.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2495 0 0 0 19989 11 0 0 25 0 1 0 480764910 12324864 2469 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3009 2469 603 41 0 2968 0
vsize: 12036
[startup+210.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2515 0 0 0 20990 11 0 0 25 0 1 0 480764910 12324864 2489 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3009 2489 603 41 0 2968 0
vsize: 12036
[startup+220.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2572 0 0 0 21990 11 0 0 25 0 1 0 480764910 12595200 2546 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3075 2546 603 41 0 3034 0
vsize: 12300
[startup+230.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2579 0 0 0 22989 12 0 0 25 0 1 0 480764910 12595200 2553 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3075 2553 603 41 0 3034 0
vsize: 12300
[startup+240.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2590 0 0 0 23988 12 0 0 25 0 1 0 480764910 12742656 2564 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3111 2564 603 41 0 3070 0
vsize: 12444
[startup+250.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2609 0 0 0 24989 12 0 0 25 0 1 0 480764910 12742656 2583 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3111 2583 603 41 0 3070 0
vsize: 12444
[startup+260.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2611 0 0 0 25989 12 0 0 25 0 1 0 480764910 12742656 2585 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3111 2585 603 41 0 3070 0
vsize: 12444
[startup+270.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2619 0 0 0 26989 12 0 0 25 0 1 0 480764910 12890112 2593 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2593 603 41 0 3106 0
vsize: 12588
[startup+280.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2619 0 0 0 27989 12 0 0 25 0 1 0 480764910 12890112 2593 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2593 603 41 0 3106 0
vsize: 12588
[startup+290.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2619 0 0 0 28989 12 0 0 25 0 1 0 480764910 12890112 2593 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2593 603 41 0 3106 0
vsize: 12588
[startup+300.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2641 0 0 0 29989 12 0 0 25 0 1 0 480764910 12890112 2615 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2615 603 41 0 3106 0
vsize: 12588
[startup+310.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2708 0 0 0 30989 12 0 0 25 0 1 0 480764910 13156352 2682 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3212 2682 603 41 0 3171 0
vsize: 12848
[startup+320.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2727 0 0 0 31989 12 0 0 25 0 1 0 480764910 13299712 2701 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3247 2701 603 41 0 3206 0
vsize: 12988
[startup+330.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2739 0 0 0 32990 12 0 0 25 0 1 0 480764910 13299712 2713 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3247 2713 603 41 0 3206 0
vsize: 12988
[startup+340.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2751 0 0 0 33990 12 0 0 25 0 1 0 480764910 13463552 2725 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3287 2725 603 41 0 3246 0
vsize: 13148
[startup+350.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2753 0 0 0 34990 13 0 0 25 0 1 0 480764910 13463552 2727 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3287 2727 603 41 0 3246 0
vsize: 13148
[startup+360.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2753 0 0 0 35990 13 0 0 25 0 1 0 480764910 13463552 2727 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3287 2727 603 41 0 3246 0
vsize: 13148
[startup+370.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2758 0 0 0 36990 13 0 0 25 0 1 0 480764910 13463552 2732 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3287 2732 603 41 0 3246 0
vsize: 13148
[startup+380.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2758 0 0 0 37991 13 0 0 25 0 1 0 480764910 13463552 2732 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3287 2732 603 41 0 3246 0
vsize: 13148
[startup+390.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2765 0 0 0 38991 13 0 0 25 0 1 0 480764910 13463552 2739 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3287 2739 603 41 0 3246 0
vsize: 13148
[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2785 0 0 0 39991 13 0 0 25 0 1 0 480764910 13598720 2759 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3320 2759 603 41 0 3279 0
vsize: 13280
[startup+410.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2799 0 0 0 40991 13 0 0 25 0 1 0 480764910 13598720 2773 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3320 2773 603 41 0 3279 0
vsize: 13280
[startup+420.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2802 0 0 0 41991 13 0 0 25 0 1 0 480764910 13737984 2776 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3354 2776 603 41 0 3313 0
vsize: 13416
[startup+430.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2813 0 0 0 42991 13 0 0 25 0 1 0 480764910 13737984 2787 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3354 2787 603 41 0 3313 0
vsize: 13416
[startup+440.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2835 0 0 0 43991 13 0 0 25 0 1 0 480764910 13869056 2809 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2809 603 41 0 3345 0
vsize: 13544
[startup+450.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2845 0 0 0 44991 13 0 0 25 0 1 0 480764910 13869056 2819 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2819 603 41 0 3345 0
vsize: 13544
[startup+460.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2849 0 0 0 45991 13 0 0 25 0 1 0 480764910 13869056 2823 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2823 603 41 0 3345 0
vsize: 13544
[startup+470.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2884 0 0 0 46992 14 0 0 25 0 1 0 480764910 14000128 2858 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3418 2858 603 41 0 3377 0
vsize: 13672
[startup+480.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2884 0 0 0 47992 14 0 0 25 0 1 0 480764910 14000128 2858 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3418 2858 603 41 0 3377 0
vsize: 13672
[startup+490.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2891 0 0 0 48992 14 0 0 25 0 1 0 480764910 14143488 2865 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2865 603 41 0 3412 0
vsize: 13812
[startup+500.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2898 0 0 0 49992 14 0 0 25 0 1 0 480764910 14143488 2872 4294967295 134512640 134672761 3221224560 3221223556 1075351154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2872 603 41 0 3412 0
vsize: 13812
[startup+510.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2898 0 0 0 50992 14 0 0 25 0 1 0 480764910 14143488 2872 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2872 603 41 0 3412 0
vsize: 13812
[startup+520.039 s]
Raw data (loadavg): 1.07 1.00 0.93 2/53 14123
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2904 0 0 0 51993 14 0 0 25 0 1 0 480764910 14143488 2878 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2878 603 41 0 3412 0
vsize: 13812
[startup+530.041 s]
Raw data (loadavg): 1.14 1.02 0.93 3/56 14164
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2906 0 0 0 52990 16 0 0 25 0 1 0 480764910 14143488 2880 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2880 603 41 0 3412 0
vsize: 13812
[startup+540.043 s]
Raw data (loadavg): 1.12 1.02 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2917 0 0 0 53990 16 0 0 25 0 1 0 480764910 14143488 2891 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3453 2891 603 41 0 3412 0
vsize: 13812
[startup+550.043 s]
Raw data (loadavg): 1.10 1.01 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2923 0 0 0 54990 16 0 0 25 0 1 0 480764910 14290944 2897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3489 2897 603 41 0 3448 0
vsize: 13956
[startup+560.043 s]
Raw data (loadavg): 1.08 1.01 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2931 0 0 0 55990 16 0 0 25 0 1 0 480764910 14290944 2905 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3489 2905 603 41 0 3448 0
vsize: 13956
[startup+570.044 s]
Raw data (loadavg): 1.07 1.01 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2932 0 0 0 56991 16 0 0 25 0 1 0 480764910 14290944 2906 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3489 2906 603 41 0 3448 0
vsize: 13956
[startup+580.045 s]
Raw data (loadavg): 1.06 1.01 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2944 0 0 0 57991 16 0 0 25 0 1 0 480764910 14290944 2918 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 2918 603 41 0 3448 0
vsize: 13956
[startup+590.046 s]
Raw data (loadavg): 1.05 1.01 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2948 0 0 0 58990 16 0 0 25 0 1 0 480764910 14290944 2922 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3489 2922 603 41 0 3448 0
vsize: 13956
[startup+600.046 s]
Raw data (loadavg): 1.04 1.01 0.93 2/53 14176
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2956 0 0 0 59991 16 0 0 25 0 1 0 480764910 14290944 2930 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3489 2930 603 41 0 3448 0
vsize: 13956
[startup+610.047 s]
Raw data (loadavg): 1.04 1.01 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2967 0 0 0 60991 17 0 0 25 0 1 0 480764910 14487552 2941 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3537 2941 603 41 0 3496 0
vsize: 14148
[startup+620.048 s]
Raw data (loadavg): 1.03 1.01 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2977 0 0 0 61991 17 0 0 25 0 1 0 480764910 14487552 2951 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3537 2951 603 41 0 3496 0
vsize: 14148
[startup+630.049 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 2989 0 0 0 62991 17 0 0 25 0 1 0 480764910 14487552 2963 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3537 2963 603 41 0 3496 0
vsize: 14148
[startup+640.049 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3001 0 0 0 63991 17 0 0 25 0 1 0 480764910 14684160 2975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2975 603 41 0 3544 0
vsize: 14340
[startup+650.05 s]
Raw data (loadavg): 1.02 1.00 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3002 0 0 0 64992 17 0 0 25 0 1 0 480764910 14684160 2976 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2976 603 41 0 3544 0
vsize: 14340
[startup+660.051 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3002 0 0 0 65992 17 0 0 25 0 1 0 480764910 14684160 2976 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2976 603 41 0 3544 0
vsize: 14340
[startup+670.052 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3013 0 0 0 66992 17 0 0 25 0 1 0 480764910 14684160 2987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2987 603 41 0 3544 0
vsize: 14340
[startup+680.053 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3015 0 0 0 67992 17 0 0 25 0 1 0 480764910 14684160 2989 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2989 603 41 0 3544 0
vsize: 14340
[startup+690.053 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3016 0 0 0 68993 17 0 0 25 0 1 0 480764910 14684160 2990 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2990 603 41 0 3544 0
vsize: 14340
[startup+700.054 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 69993 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+710.054 s]
Raw data (loadavg): 1.08 1.02 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 70993 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+720.055 s]
Raw data (loadavg): 1.07 1.02 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 71993 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+730.055 s]
Raw data (loadavg): 1.06 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 72994 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223744 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+740.056 s]
Raw data (loadavg): 1.05 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 73994 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+750.057 s]
Raw data (loadavg): 1.04 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 74994 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+760.057 s]
Raw data (loadavg): 1.03 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 75994 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+770.058 s]
Raw data (loadavg): 1.03 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 76994 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+780.059 s]
Raw data (loadavg): 1.02 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3018 0 0 0 77995 17 0 0 25 0 1 0 480764910 14684160 2992 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3585 2992 603 41 0 3544 0
vsize: 14340
[startup+790.061 s]
Raw data (loadavg): 1.02 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3075 0 0 0 78995 17 0 0 25 0 1 0 480764910 14946304 3049 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3649 3049 603 41 0 3608 0
vsize: 14596
[startup+800.062 s]
Raw data (loadavg): 1.02 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3126 0 0 0 79995 17 0 0 25 0 1 0 480764910 15081472 3100 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3682 3100 603 41 0 3641 0
vsize: 14728
[startup+810.062 s]
Raw data (loadavg): 1.01 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3137 0 0 0 80995 17 0 0 25 0 1 0 480764910 15241216 3111 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3721 3111 603 41 0 3680 0
vsize: 14884
[startup+820.063 s]
Raw data (loadavg): 1.01 1.01 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3138 0 0 0 81995 17 0 0 25 0 1 0 480764910 15241216 3112 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3721 3112 603 41 0 3680 0
vsize: 14884
[startup+830.063 s]
Raw data (loadavg): 1.01 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3200 0 0 0 82995 17 0 0 25 0 1 0 480764910 15507456 3174 4294967295 134512640 134672761 3221224560 3221223620 1075349617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3786 3174 603 41 0 3745 0
vsize: 15144
[startup+840.065 s]
Raw data (loadavg): 1.01 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3204 0 0 0 83995 18 0 0 25 0 1 0 480764910 15507456 3178 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3786 3178 603 41 0 3745 0
vsize: 15144
[startup+850.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3215 0 0 0 84995 18 0 0 25 0 1 0 480764910 15507456 3189 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3786 3189 603 41 0 3745 0
vsize: 15144
[startup+860.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3309 0 0 0 85995 18 0 0 25 0 1 0 480764910 15908864 3283 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3884 3283 603 41 0 3843 0
vsize: 15536
[startup+870.066 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3440 0 0 0 86995 18 0 0 25 0 1 0 480764910 16445440 3414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4015 3414 603 41 0 3974 0
vsize: 16060
[startup+880.067 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3507 0 0 0 87995 19 0 0 25 0 1 0 480764910 16707584 3481 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3481 603 41 0 4038 0
vsize: 16316
[startup+890.067 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14178
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3519 0 0 0 88995 19 0 0 25 0 1 0 480764910 16846848 3493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3493 603 41 0 4072 0
vsize: 16452
[startup+900.068 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3522 0 0 0 89995 19 0 0 25 0 1 0 480764910 16846848 3496 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3496 603 41 0 4072 0
vsize: 16452
[startup+910.069 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3536 0 0 0 90995 19 0 0 25 0 1 0 480764910 16846848 3510 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3510 603 41 0 4072 0
vsize: 16452
[startup+920.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3538 0 0 0 91996 19 0 0 25 0 1 0 480764910 16846848 3512 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3512 603 41 0 4072 0
vsize: 16452
[startup+930.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3539 0 0 0 92996 19 0 0 25 0 1 0 480764910 16846848 3513 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3513 603 41 0 4072 0
vsize: 16452
[startup+940.071 s]
Raw data (loadavg): 1.08 1.02 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3543 0 0 0 93996 19 0 0 25 0 1 0 480764910 16846848 3517 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3517 603 41 0 4072 0
vsize: 16452
[startup+950.072 s]
Raw data (loadavg): 1.07 1.02 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3546 0 0 0 94996 19 0 0 25 0 1 0 480764910 16846848 3520 4294967295 134512640 134672761 3221224560 3221223728 134561366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3520 603 41 0 4072 0
vsize: 16452
[startup+960.073 s]
Raw data (loadavg): 1.06 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3554 0 0 0 95997 19 0 0 25 0 1 0 480764910 16846848 3528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3528 603 41 0 4072 0
vsize: 16452
[startup+970.073 s]
Raw data (loadavg): 1.05 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3554 0 0 0 96997 19 0 0 25 0 1 0 480764910 16846848 3528 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3528 603 41 0 4072 0
vsize: 16452
[startup+980.073 s]
Raw data (loadavg): 1.04 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3554 0 0 0 97997 19 0 0 25 0 1 0 480764910 16846848 3528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3528 603 41 0 4072 0
vsize: 16452
[startup+990.074 s]
Raw data (loadavg): 1.03 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3555 0 0 0 98997 19 0 0 25 0 1 0 480764910 16846848 3529 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4113 3529 603 41 0 4072 0
vsize: 16452
[startup+1000.07 s]
Raw data (loadavg): 1.03 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3568 0 0 0 99997 19 0 0 25 0 1 0 480764910 17010688 3542 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3542 603 41 0 4112 0
vsize: 16612
[startup+1010.07 s]
Raw data (loadavg): 1.02 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3576 0 0 0 100998 19 0 0 25 0 1 0 480764910 17010688 3550 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3550 603 41 0 4112 0
vsize: 16612
[startup+1020.08 s]
Raw data (loadavg): 1.02 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3583 0 0 0 101998 19 0 0 25 0 1 0 480764910 17010688 3557 4294967295 134512640 134672761 3221224560 3221223744 134558371 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3557 603 41 0 4112 0
vsize: 16612
[startup+1030.08 s]
Raw data (loadavg): 1.02 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3585 0 0 0 102998 19 0 0 25 0 1 0 480764910 17010688 3559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3559 603 41 0 4112 0
vsize: 16612
[startup+1040.08 s]
Raw data (loadavg): 1.01 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3587 0 0 0 103998 19 0 0 25 0 1 0 480764910 17010688 3561 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3561 603 41 0 4112 0
vsize: 16612
[startup+1050.08 s]
Raw data (loadavg): 1.01 1.01 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3587 0 0 0 104999 19 0 0 25 0 1 0 480764910 17010688 3561 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3561 603 41 0 4112 0
vsize: 16612
[startup+1060.08 s]
Raw data (loadavg): 1.01 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3587 0 0 0 105999 19 0 0 25 0 1 0 480764910 17010688 3561 4294967295 134512640 134672761 3221224560 3221223760 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3561 603 41 0 4112 0
vsize: 16612
[startup+1070.08 s]
Raw data (loadavg): 1.01 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3612 0 0 0 106999 19 0 0 25 0 1 0 480764910 17207296 3586 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3586 603 41 0 4160 0
vsize: 16804
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3627 0 0 0 107999 19 0 0 25 0 1 0 480764910 17207296 3601 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3601 603 41 0 4160 0
vsize: 16804
[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3627 0 0 0 109000 19 0 0 25 0 1 0 480764910 17207296 3601 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3601 603 41 0 4160 0
vsize: 16804
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3627 0 0 0 110000 19 0 0 25 0 1 0 480764910 17207296 3601 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3601 603 41 0 4160 0
vsize: 16804
[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3627 0 0 0 111000 19 0 0 25 0 1 0 480764910 17207296 3601 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3601 603 41 0 4160 0
vsize: 16804
[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3633 0 0 0 112000 19 0 0 25 0 1 0 480764910 17207296 3607 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3607 603 41 0 4160 0
vsize: 16804
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3642 0 0 0 113000 19 0 0 25 0 1 0 480764910 17371136 3616 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3616 603 41 0 4200 0
vsize: 16964
[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3644 0 0 0 114001 19 0 0 25 0 1 0 480764910 17371136 3618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3618 603 41 0 4200 0
vsize: 16964
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3644 0 0 0 115001 19 0 0 25 0 1 0 480764910 17371136 3618 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3618 603 41 0 4200 0
vsize: 16964
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3657 0 0 0 116001 19 0 0 25 0 1 0 480764910 17371136 3631 4294967295 134512640 134672761 3221224560 3221223696 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3631 603 41 0 4200 0
vsize: 16964
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3658 0 0 0 117001 19 0 0 25 0 1 0 480764910 17371136 3632 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3632 603 41 0 4200 0
vsize: 16964
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3659 0 0 0 118001 19 0 0 25 0 1 0 480764910 17371136 3633 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3633 603 41 0 4200 0
vsize: 16964
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3659 0 0 0 119002 19 0 0 25 0 1 0 480764910 17371136 3633 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3633 603 41 0 4200 0
vsize: 16964
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/53 14180
Raw data (stat): 14123 (minisat+) R 14122 7987 7986 0 -1 0 3664 0 0 0 120002 19 0 0 25 0 1 0 480764910 17371136 3638 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3638 603 41 0 4200 0
vsize: 16964
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 14180
Raw data (stat): 14123 (minisat+) Z 14122 7987 7986 0 -1 12 3667 0 0 0 120002 20 0 0 25 0 1 0 480764910 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.1
CPU time (s): 1200.23
CPU user time (s): 1200.03
CPU system time (s): 0.205968
CPU usage (%): 100.011
Max. virtual memory (Kb): 16964
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####