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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-4.opb
MD5SUM	615f734b8951521e89cf22f42d6d26cc
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
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	450
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.05084
Number of variables	450
Total number of constraints	17831
Number of constraints which are clauses	17831
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	2
Trace number 5610

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 00:49:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4077 boxname=wulflinc15 idbench=317 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  615f734b8951521e89cf22f42d6d26cc  /oldhome/oroussel/tmp/wulflinc15/normalized-frb30-15-4.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-frb30-15-4.opb /oldhome/oroussel/tmp/wulflinc15/normalized-frb30-15-4.opb
IDLAUNCH: 4077
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        902028 kB
Buffers:         36036 kB
Cached:          74904 kB
SwapCached:       2144 kB
Active:          63848 kB
Inactive:        52080 kB
HighTotal:      131008 kB
HighFree:        52248 kB
LowTotal:       903652 kB
LowFree:        849780 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11224 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:09:47 (client local time) WITH STATUS 30 IN 1191.81 SECONDS
stats: 4077 0 1191.81 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17831 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 |   17831    35662 |    5349       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   17831    35662 |    7132       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.626904 s)
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   34844    75677 |   10453       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11709          
c   -- var.elim.:  2000/11709          
c   -- var.elim.:  3000/11709          
c   -- var.elim.:  4000/11709          
c   -- var.elim.:  5000/11709          
c   -- var.elim.:  6000/11709          
c   -- var.elim.:  7000/11709          
c   -- var.elim.:  8000/11709          
c   -- var.elim.:  9000/11709          
c   -- var.elim.:  10000/11709          
c   -- var.elim.:  11000/11709          
c   -- var.elim.:  11709/11709          
c   -- var.elim.:  1000/5970          
c   -- var.elim.:  2000/5970          
c   -- var.elim.:  3000/5970          
c   -- var.elim.:  4000/5970          
c   -- var.elim.:  5000/5970          
c   -- var.elim.:  5970/5970          
c   -- var.elim.:  115/115          
c   -- subsuming                       
c   -- var.elim.:  1000/2268          
c   -- var.elim.:  2000/2268          
c   -- var.elim.:  2268/2268          
c   -- var.elim.:  472/472          
c |         0 |   22800    70968 |      --       0       --      -- |     --   | -12039/-4694
c |         0 |   22800    70968 |    9120       0        0     nan |  0.000 % |
c |       100 |   22800    70968 |   10032     100     7886    78.9 | 52.391 % |
c |       250 |   22800    70968 |   11035     250    17424    69.7 | 52.390 % |
c |       475 |   22800    70968 |   12138     475    47120    99.2 | 52.391 % |
c |       812 |   22800    70968 |   13352     812    99795   122.9 | 52.390 % |
c |      1319 |   22800    70968 |   14687    1319   157625   119.5 | 52.391 % |
c ==============================================================================
c (current CPU-time: 12.93 s)
c ==============================================================================
c [1mFound solution: -23[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 |      1821 |   26009    79535 |    7802    1821   228772   125.6 | 52.391 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5224          
c   -- var.elim.:  2000/5224          
c   -- var.elim.:  3000/5224          
c   -- var.elim.:  4000/5224          
c   -- var.elim.:  5000/5224          
c   -- var.elim.:  5224/5224          
c   -- var.elim.:  1000/2152          
c   -- var.elim.:  2000/2152          
c   -- var.elim.:  2152/2152          
c   -- var.elim.:  24/24          
c |      1821 |   22911    76521 |      --    1821       --      -- |     --   | -3088/-2993
c |      1821 |   22911    76521 |    9164    1821   228772   125.6 | 52.391 % |
c |      1923 |   22911    76521 |   10080    1923   243298   126.5 | 61.707 % |
c |      2073 |   22911    76521 |   11088    2073   263878   127.3 | 61.707 % |
c |      2298 |   22911    76521 |   12197    2298   296171   128.9 | 61.707 % |
c |      2635 |   22799    74383 |   13352    2624   334022   127.3 | 62.374 % |
c |      3141 |   22762    74121 |   14663    3128   425726   136.1 | 62.587 % |
c |      3901 |   22596    72549 |   16012    3862   538025   139.3 | 63.560 % |
c ==============================================================================
c (current CPU-time: 18.5292 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 |      4138 |   22696    72857 |    6808    4099   581937   142.0 | 63.560 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2708          
c   -- var.elim.:  2000/2708          
c   -- var.elim.:  2708/2708          
c   -- var.elim.:  297/297          
c |      4138 |   22574    71981 |      --    4099       --      -- |     --   | -110/-604
c |      4138 |   22574    71981 |    9029    3697   393953   106.6 | 63.560 % |
c |      4238 |   22574    71981 |    9932    3797   406863   107.2 | 63.753 % |
c |      4388 |   22548    71725 |   10913    3944   442413   112.2 | 63.927 % |
c |      4613 |   22548    71725 |   12004    4169   462016   110.8 | 63.927 % |
c |      4950 |   22415    70437 |   13127    4495   492791   109.6 | 64.767 % |
c |      5456 |   22371    70058 |   14411    4978   566977   113.9 | 65.035 % |
c |      6216 |   22315    69549 |   15812    5731   681194   118.9 | 65.408 % |
c |      7355 |   22198    68568 |   17303    6845   864936   126.4 | 66.182 % |
c |      9063 |   22152    68176 |   18993    8542  1220979   142.9 | 66.489 % |
c |     11625 |   21860    65867 |   20617   11052  1635465   148.0 | 68.438 % |
c ==============================================================================
c (current CPU-time: 32.832 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 |     13159 |   22530    66831 |    6758   12482  1946966   156.0 | 68.438 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3078          
c   -- var.elim.:  2000/3078          
c   -- var.elim.:  3000/3078          
c   -- var.elim.:  3078/3078          
c   -- var.elim.:  770/770          
c |     13159 |   21721    65355 |      --   12482       --      -- |     --   | -809/-1475
c |     13159 |   21721    65355 |    8688   12370  1924374   155.6 | 68.438 % |
c |     13262 |   21721    65355 |    9557   12473  1943972   155.9 | 70.094 % |
c |     13413 |   21721    65355 |   10512   12624  1977641   156.7 | 70.094 % |
c |     13639 |   21721    65355 |   11564   12850  2015736   156.9 | 70.095 % |
c |     13977 |   21721    65355 |   12720   13188  2066683   156.7 | 70.095 % |
c |     14483 |   21721    65355 |   13992   13694  2141614   156.4 | 70.094 % |
c |     15242 |   21721    65355 |   15392   14453  2263969   156.6 | 70.094 % |
c |     16381 |   21648    64775 |   16874   15579  2470186   158.6 | 70.566 % |
c |     18089 |   21578    64221 |   18501   17266  2771641   160.5 | 70.999 % |
c |     20651 |   21533    63869 |   20309   19771  3300937   167.0 | 71.274 % |
c ==============================================================================
c (current CPU-time: 49.3865 s)
c ==============================================================================
c [1mFound solution: -26[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 |     21111 |   22158    65682 |    6647   20231  3428843   169.5 | 71.274 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2694          
c   -- var.elim.:  2000/2694          
c   -- var.elim.:  2694/2694          
c   -- var.elim.:  1000/1165          
c   -- var.elim.:  1165/1165          
c |     21111 |   21522    63362 |      --   20231       --      -- |     --   | -620/-961
c |     21111 |   21522    63362 |    8608   16195  1576459    97.3 | 71.274 % |
c |     21211 |   21522    63362 |    9469   10594   774017    73.1 | 71.380 % |
c |     21361 |   21522    63362 |   10416   10744   803899    74.8 | 71.380 % |
c |     21586 |   21522    63362 |   11458   10969   840830    76.7 | 71.381 % |
c |     21925 |   21522    63362 |   12604   11308   915660    81.0 | 71.381 % |
c |     22432 |   21498    63188 |   13849   11811   992817    84.1 | 71.537 % |
c |     23192 |   21478    63014 |   15219   12559  1147989    91.4 | 71.669 % |
c |     24332 |   21476    62996 |   16740   13695  1349200    98.5 | 71.681 % |
c |     26041 |   21429    62646 |   18373   15398  1668449   108.4 | 71.984 % |
c |     28603 |   21362    62114 |   20148   17951  2273166   126.6 | 72.402 % |
c |     32448 |   21338    61930 |   22138   21789  3077331   141.2 | 72.546 % |
c |     38215 |   21272    61432 |   24276   27544  4265608   154.9 | 72.966 % |
c |     46865 |   21050    59675 |   26425   21828  3516517   161.1 | 74.302 % |
c ==============================================================================
c (current CPU-time: 136.713 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 |     58011 |   22471    62537 |    6741   17065  2461031   144.2 | 74.302 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3400          
c   -- var.elim.:  2000/3400          
c   -- var.elim.:  3000/3400          
c   -- var.elim.:  3400/3400          
c   -- var.elim.:  1000/1000          
c   -- var.elim.:  2/2          
c |     58011 |   20946    60265 |      --   17065       --      -- |     --   | -1513/-2247
c |     58011 |   20946    60265 |    8378   17065  2461031   144.2 | 74.302 % |
c |     58111 |   20946    60265 |    9216   11477  1541994   134.4 | 76.775 % |
c |     58261 |   20946    60265 |   10137   11627  1571648   135.2 | 76.775 % |
c |     58486 |   20919    60042 |   11137   11846  1609136   135.8 | 76.934 % |
c |     58823 |   20919    60042 |   12251   12183  1672400   137.3 | 76.933 % |
c |     59329 |   20919    60042 |   13476   12689  1764749   139.1 | 76.934 % |
c |     60088 |   20859    59597 |   14781   13430  1863347   138.7 | 77.275 % |
c |     61228 |   20830    59390 |   16236   14564  2052191   140.9 | 77.434 % |
c |     62936 |   20729    58568 |   17773   16246  2295439   141.3 | 77.995 % |
c |     65498 |   20703    58354 |   19526   18804  2686834   142.9 | 78.154 % |
c |     69343 |   20703    58354 |   21479   22649  3498526   154.5 | 78.154 % |
c |     75111 |   20633    57812 |   23547   28407  4615537   162.5 | 78.520 % |
c |     83760 |   20482    56651 |   25712   22381  3404622   152.1 | 79.385 % |
c |     96734 |   20380    55875 |   28142   18728  2705938   144.5 | 79.983 % |
c ==============================================================================
c (current CPU-time: 266.021 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 |    113111 |   20924    56835 |    6277   35067  6021050   171.7 | 79.983 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2209          
c   -- var.elim.:  2000/2209          
c   -- var.elim.:  2209/2209          
c   -- var.elim.:  484/484          
c |    113111 |   20268    54536 |      --   35067       --      -- |     --   | -635/-1236
c |    113111 |   20268    54536 |    8107   21891  1546609    70.7 | 79.983 % |
c |    113211 |   20268    54536 |    8917   10955   695622    63.5 | 80.763 % |
c |    113361 |   20268    54536 |    9809   11105   713867    64.3 | 80.763 % |
c |    113586 |   20247    54374 |   10779   11327   742911    65.6 | 80.872 % |
c |    113924 |   20247    54374 |   11857   11665   794889    68.1 | 80.872 % |
c |    114430 |   20247    54374 |   13043   12171   872172    71.7 | 80.872 % |
c |    115191 |   20247    54374 |   14347   12932  1035508    80.1 | 80.872 % |
c |    116330 |   20200    53989 |   15745   14061  1235221    87.8 | 81.140 % |
c |    118038 |   20200    53989 |   17320   15769  1525552    96.7 | 81.140 % |
c |    120601 |   20200    53989 |   19052   18332  2020212   110.2 | 81.139 % |
c |    124445 |   20200    53989 |   20957   22176  2691088   121.4 | 81.140 % |
c |    130211 |   20109    53310 |   22949   27841  3668417   131.8 | 81.650 % |
c |    138861 |   19966    52249 |   25064   23133  3068146   132.6 | 82.451 % |
c |    151835 |   19928    51926 |   27518   20259  2519135   124.3 | 82.682 % |
c |    171296 |   19822    51091 |   30109   20462  2622409   128.2 | 83.301 % |
c |    200488 |   19731    50345 |   32968   28829  3800487   131.8 | 83.836 % |
c ==============================================================================
c (current CPU-time: 477.766 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 |    207415 |   19824    50491 |    5947   35749  4907177   137.3 | 83.836 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1410          
c   -- var.elim.:  1410/1410          
c   -- var.elim.:  245/245          
c |    207415 |   19742    50375 |      --   35749       --      -- |     --   | -81/-113
c |    207415 |   19742    50375 |    7896   20360  1859944    91.4 | 83.836 % |
c |    207515 |   19742    50375 |    8686   10506   886025    84.3 | 84.025 % |
c |    207665 |   19742    50375 |    9555   10656   907601    85.2 | 84.025 % |
c |    207890 |   19742    50375 |   10510   10881   939385    86.3 | 84.025 % |
c |    208227 |   19742    50375 |   11561   11218   986389    87.9 | 84.025 % |
c |    208733 |   19742    50375 |   12717   11724  1058355    90.3 | 84.025 % |
c |    209493 |   19742    50375 |   13989   12484  1172874    94.0 | 84.025 % |
c |    210632 |   19742    50375 |   15388   13623  1335006    98.0 | 84.025 % |
c |    212340 |   19742    50375 |   16927   15331  1580546   103.1 | 84.025 % |
c |    214902 |   19742    50375 |   18620   17893  1956319   109.3 | 84.025 % |
c |    218746 |   19710    50133 |   20449   21729  2580785   118.8 | 84.206 % |
c |    224512 |   19685    49936 |   22465   27484  3431715   124.9 | 84.338 % |
c |    233162 |   19626    49517 |   24637   21797  2769359   127.1 | 84.664 % |
c |    246136 |   19602    49352 |   27068   18294  2018091   110.3 | 84.809 % |
c |    265598 |   19545    48935 |   29688   20522  2273287   110.8 | 85.146 % |
c |    294790 |   19479    48472 |   32547   28918  3333902   115.3 | 85.532 % |
c |    338579 |   19183    46353 |   35258   28333  2636845    93.1 | 87.184 % |
c |    404264 |   18695    44166 |   37797   31671  2575201    81.3 | 88.775 % |
c |    502790 |   17507    40665 |   38934   25885  1403531    54.2 | 90.318 % |
c ==============================================================================
c (current CPU-time: 1153.66 s)
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:14716     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    547460 |   28559    66337 |    8567   46779  2210596    47.3 | 90.318 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8577          
c   -- var.elim.:  2000/8577          
c   -- var.elim.:  3000/8577          
c   -- var.elim.:  4000/8577          
c   -- var.elim.:  5000/8577          
c   -- var.elim.:  6000/8577          
c   -- var.elim.:  7000/8577          
c   -- var.elim.:  8000/8577          
c   -- var.elim.:  8577/8577          
c   -- var.elim.:  1000/4060          
c   -- var.elim.:  2000/4060          
c   -- var.elim.:  3000/4060          
c   -- var.elim.:  4000/4060          
c   -- var.elim.:  4060/4060          
c   -- var.elim.:  1000/1215          
c   -- var.elim.:  1215/1215          
c   -- subsuming                       
c   -- var.elim.:  1000/1805          
c   -- var.elim.:  1805/1805          
c   -- var.elim.:  1000/1089          
c   -- var.elim.:  1089/1089          
c   -- var.elim.:  6/6          
c |    547460 |   20583    63736 |      --   46779       --      -- |     --   | -7816/-2276
c |    547460 |   20583    63736 |    8233   39415  1766751    44.8 | 90.318 % |
c |    547560 |   20583    63736 |    9056   14289   462568    32.4 | 82.177 % |
c |    547710 |   20583    63736 |    9962   14439   467411    32.4 | 82.177 % |
c |    547935 |   20483    63511 |   10905   14636   479080    32.7 | 82.185 % |
c |    548272 |   20483    63511 |   11995   14973   492912    32.9 | 82.185 % |
c |    548778 |   20483    63511 |   13195   15479   513987    33.2 | 82.184 % |
c |    549537 |   20371    63209 |   14435   15796   525691    33.3 | 82.243 % |
c |    550678 |   20259    62869 |   15791   16011   529305    33.1 | 82.336 % |
c |    552387 |   20172    62680 |   17296   17719   590569    33.3 | 82.344 % |
c |    554949 |   20080    62443 |   18939   19104   645404    33.8 | 82.373 % |
c |    558793 |   19803    61750 |   20545   21775   756199    34.7 | 82.488 % |
c |    564559 |   18707    56527 |   21349   18522   565621    30.5 | 83.139 % |
c ==============================================================================
c [1mOptimal solution: -30[0m
s OPTIMUM FOUND
v -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 C436 -C435 -C434 -C433 -C432 C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 C166 -C165 -C164 -C163 -C162 -C161 -C160 C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 C95 -C94 -C93 -C92 -C91 C90 -C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75 C74 -C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 -C62 -C61 -C60 -C59 -C58 -C57 C56 -C55 -C54 -C53 -C52 -C51 -C50 -C49 -C48 -C47 -C46 -C45 -C44 -C43 -C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 -C34 C33 -C32 -C31 -C30 -C29 -C28 C27 -C26 -C25 -C24 -C23 -C22 -C21 -C20 -C19 -C18 -C17 -C16 -C15 -C14 C13 -C12 -C11 -C10 -C9 -C8 -C7 -C6 -C5 -C4 -C3 -C2 -C1
c _______________________________________________________________________________
c 
c restarts              : 108
c conflicts             : 569194         (478 /sec)
c decisions             : 834772         (701 /sec)
c propagations          : 52346379       (43947 /sec)
c inspects              : 1894487946     (1590506 /sec)
c CPU time              : 1191.12 s
c _______________________________________________________________________________
#### 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 3189
Raw data (stat): 3189 (runsolver) R 3188 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422176895 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.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 2491 0 0 0 989 9 0 0 25 0 1 0 422176895 12292096 2382 4294967295 134512640 134672761 3221224560 3221222960 134604069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3001 2382 603 41 0 2960 0
vsize: 12004
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 3928 0 0 0 1978 19 0 0 25 0 1 0 422176895 16179200 3218 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3950 3218 603 41 0 3909 0
vsize: 15800
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 4803 0 0 0 2975 21 0 0 25 0 1 0 422176895 19705856 4093 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4811 4093 603 41 0 4770 0
vsize: 19244
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 6036 0 0 0 3968 27 0 0 25 0 1 0 422176895 23678976 5066 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5781 5066 603 41 0 5740 0
vsize: 23124
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 7788 0 0 0 4963 34 0 0 25 0 1 0 422176895 30056448 6529 4294967295 134512640 134672761 3221224560 3221223200 134622580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7338 6529 603 41 0 7297 0
vsize: 29352
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 7788 0 0 0 5962 34 0 0 25 0 1 0 422176895 30056448 6529 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7338 6529 603 41 0 7297 0
vsize: 29352
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 7789 0 0 0 6962 34 0 0 25 0 1 0 422176895 30056448 6530 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7338 6530 603 41 0 7297 0
vsize: 29352
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 7948 0 0 0 7961 35 0 0 25 0 1 0 422176895 30318592 6689 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7402 6689 603 41 0 7361 0
vsize: 29608
[startup+90.0052 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 8550 0 0 0 8960 36 0 0 25 0 1 0 422176895 32825344 7291 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8014 7291 603 41 0 7973 0
vsize: 32056
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 9058 0 0 0 9959 38 0 0 25 0 1 0 422176895 34799616 7799 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8496 7799 603 41 0 8455 0
vsize: 33984
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 9059 0 0 0 10959 38 0 0 25 0 1 0 422176895 34799616 7800 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8496 7800 603 41 0 8455 0
vsize: 33984
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 9059 0 0 0 11959 38 0 0 25 0 1 0 422176895 34799616 7800 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8496 7800 603 41 0 8455 0
vsize: 33984
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 9444 0 0 0 12958 39 0 0 25 0 1 0 422176895 36499456 8185 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8911 8185 603 41 0 8870 0
vsize: 35644
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 13951 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 14950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 15950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 16950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 17950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 18950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 19950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 20950 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10469 0 0 0 21951 46 0 0 25 0 1 0 422176895 38596608 8755 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8755 603 41 0 9382 0
vsize: 37692
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10535 0 0 0 22951 46 0 0 25 0 1 0 422176895 38858752 8788 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9487 8788 603 41 0 9446 0
vsize: 37948
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10535 0 0 0 23951 46 0 0 25 0 1 0 422176895 38858752 8788 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9487 8788 603 41 0 9446 0
vsize: 37948
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10535 0 0 0 24951 46 0 0 25 0 1 0 422176895 38858752 8788 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9487 8788 603 41 0 9446 0
vsize: 37948
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 10538 0 0 0 25951 46 0 0 25 0 1 0 422176895 38989824 8791 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9519 8791 603 41 0 9478 0
vsize: 38076
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11760 0 0 0 26947 51 0 0 25 0 1 0 422176895 41320448 9400 4294967295 134512640 134672761 3221224560 3221223600 134614348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10088 9400 603 41 0 10047 0
vsize: 40352
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11760 0 0 0 27946 51 0 0 25 0 1 0 422176895 41320448 9400 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9400 603 41 0 10047 0
vsize: 40352
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11760 0 0 0 28945 51 0 0 25 0 1 0 422176895 41320448 9400 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10088 9400 603 41 0 10047 0
vsize: 40352
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11760 0 0 0 29945 51 0 0 25 0 1 0 422176895 41320448 9400 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9400 603 41 0 10047 0
vsize: 40352
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11760 0 0 0 30945 51 0 0 25 0 1 0 422176895 41320448 9400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9400 603 41 0 10047 0
vsize: 40352
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 31945 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 32946 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 33946 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223704 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 34946 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 35946 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 36946 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 37947 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 38947 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 39947 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 40947 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 41947 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11761 0 0 0 42948 51 0 0 25 0 1 0 422176895 41320448 9401 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9401 603 41 0 10047 0
vsize: 40352
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11763 0 0 0 43948 51 0 0 25 0 1 0 422176895 41320448 9403 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9403 603 41 0 10047 0
vsize: 40352
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11763 0 0 0 44948 51 0 0 25 0 1 0 422176895 41320448 9403 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9403 603 41 0 10047 0
vsize: 40352
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11763 0 0 0 45948 51 0 0 25 0 1 0 422176895 41320448 9403 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9403 603 41 0 10047 0
vsize: 40352
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 11763 0 0 0 46948 51 0 0 25 0 1 0 422176895 41320448 9403 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10088 9403 603 41 0 10047 0
vsize: 40352
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 47945 55 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 48944 55 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 49943 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 50942 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 51941 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 52941 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 53941 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 54941 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 55941 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 56942 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 57942 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12221 0 0 0 58943 56 0 0 25 0 1 0 422176895 41676800 9492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9492 603 41 0 10134 0
vsize: 40700
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3189
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 59943 56 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223664 134603947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+610.028 s]
Raw data (loadavg): 1.23 1.02 0.93 3/57 3228
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 60943 56 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223600 134603512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+620.029 s]
Raw data (loadavg): 1.20 1.02 0.93 2/54 3242
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 61943 56 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+630.029 s]
Raw data (loadavg): 1.17 1.02 0.93 2/54 3242
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 62943 56 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+640.029 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 3242
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 63943 57 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+650.029 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 3242
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 64943 57 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+660.029 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 3242
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 65943 57 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+670.03 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 3242
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 66944 57 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+680.03 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12222 0 0 0 67944 57 0 0 25 0 1 0 422176895 41676800 9493 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9493 603 41 0 10134 0
vsize: 40700
[startup+690.031 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 68944 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+700.031 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 69944 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+710.031 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 70944 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+720.032 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 71944 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+730.032 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 72945 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+740.033 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 73945 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+750.033 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 74945 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+760.032 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 75945 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+770.032 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 76945 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223720 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+780.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12225 0 0 0 77945 57 0 0 25 0 1 0 422176895 41676800 9496 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9496 603 41 0 10134 0
vsize: 40700
[startup+790.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12226 0 0 0 78946 57 0 0 25 0 1 0 422176895 41676800 9497 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9497 603 41 0 10134 0
vsize: 40700
[startup+800.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 79946 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+810.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 80946 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+820.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 81946 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223704 134616339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+830.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 82946 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+840.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 83947 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+850.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 84947 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+860.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 85947 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+870.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 86947 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+880.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 87947 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+890.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 88948 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+900.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 89948 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223600 134613116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+910.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 90948 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+920.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 91948 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+930.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12228 0 0 0 92948 57 0 0 25 0 1 0 422176895 41676800 9499 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9499 603 41 0 10134 0
vsize: 40700
[startup+940.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 93949 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+950.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 94949 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+960.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3244
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 95949 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+970.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 96949 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+980.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 97949 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+990.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 98950 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 99950 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223600 134614207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 100950 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 101950 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 102950 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1040.04 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 103951 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1050.04 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 104950 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1060.04 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 105951 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1070.04 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 106951 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1080.04 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 107951 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1090.04 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 108951 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1100.04 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 109951 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1110.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 110952 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1120.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 111952 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1130.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 112952 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1140.04 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 113952 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1150.04 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12230 0 0 0 114952 57 0 0 25 0 1 0 422176895 41676800 9501 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9501 603 41 0 10134 0
vsize: 40700
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12999 0 0 0 115944 65 0 0 25 0 1 0 422176895 41377792 9550 4294967295 134512640 134672761 3221224560 3221223616 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10102 9550 603 41 0 10061 0
vsize: 40408
[startup+1170.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12999 0 0 0 116944 65 0 0 25 0 1 0 422176895 41115648 9511 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10038 9511 603 41 0 9997 0
vsize: 40152
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12999 0 0 0 117944 65 0 0 25 0 1 0 422176895 41115648 9511 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10038 9511 603 41 0 9997 0
vsize: 40152
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12999 0 0 0 118944 65 0 0 25 0 1 0 422176895 41115648 9511 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10038 9511 603 41 0 9997 0
vsize: 40152
[startup+1191.76 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 3246
Raw data (stat): 3189 (minisat+) R 3188 29151 29150 0 -1 0 12999 0 0 0 118944 65 0 0 25 0 1 0 422176895 41115648 9511 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10038 9511 603 41 0 9997 0
vsize: 0

Child status: 30
Real time (s): 1191.76
CPU time (s): 1191.81
CPU user time (s): 1191.13
CPU system time (s): 0.679896
CPU usage (%): 100.005
Max. virtual memory (Kb): 40700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-30
#### END VERIFIER DATA ####