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/frb35-17-opb/normalized-frb35-17-5.opb
MD5SUM	70070c820bc7d178cc8f33b42e0deead
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	28143
Number of constraints which are clauses	28143
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 5615

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        851032 kB
Buffers:         40652 kB
Cached:         118808 kB
SwapCached:          0 kB
Active:         108192 kB
Inactive:        54444 kB
HighTotal:      131008 kB
HighFree:        19404 kB
LowTotal:       903652 kB
LowFree:        831628 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15352 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:17:46 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4083 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28143 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 |   28143    56286 |    8442       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   28143    56286 |   11257       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.09283 s)
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   56290   122394 |   16886       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19251          
c   -- var.elim.:  2000/19251          
c   -- var.elim.:  3000/19251          
c   -- var.elim.:  4000/19251          
c   -- var.elim.:  5000/19251          
c   -- var.elim.:  6000/19251          
c   -- var.elim.:  7000/19251          
c   -- var.elim.:  8000/19251          
c   -- var.elim.:  9000/19251          
c   -- var.elim.:  10000/19251          
c   -- var.elim.:  11000/19251          
c   -- var.elim.:  12000/19251          
c   -- var.elim.:  13000/19251          
c   -- var.elim.:  14000/19251          
c   -- var.elim.:  15000/19251          
c   -- var.elim.:  16000/19251          
c   -- var.elim.:  17000/19251          
c   -- var.elim.:  18000/19251          
c   -- var.elim.:  19000/19251          
c   -- var.elim.:  19251/19251          
c   -- var.elim.:  1000/9800          
c   -- var.elim.:  2000/9800          
c   -- var.elim.:  3000/9800          
c   -- var.elim.:  4000/9800          
c   -- var.elim.:  5000/9800          
c   -- var.elim.:  6000/9800          
c   -- var.elim.:  7000/9800          
c   -- var.elim.:  8000/9800          
c   -- var.elim.:  9000/9800          
c   -- var.elim.:  9800/9800          
c   -- var.elim.:  75/75          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  1000/3806          
c   -- var.elim.:  2000/3806          
c   -- var.elim.:  3000/3806          
c   -- var.elim.:  3806/3806          
c   -- var.elim.:  353/353          
c |         0 |   36440   121761 |      --       0       --      -- |     --   | -19850/-632
c |         0 |   36440   121761 |   14576       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 42.7585 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 |        44 |   41399   135135 |   12419      44     3445    78.3 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8882          
c   -- var.elim.:  2000/8882          
c   -- var.elim.:  3000/8882          
c   -- var.elim.:  4000/8882          
c   -- var.elim.:  5000/8882          
c   -- var.elim.:  6000/8882          
c   -- var.elim.:  7000/8882          
c   -- var.elim.:  8000/8882          
c   -- var.elim.:  8882/8882          
c   -- var.elim.:  1000/3452          
c   -- var.elim.:  2000/3452          
c   -- var.elim.:  3000/3452          
c   -- var.elim.:  3452/3452          
c   -- var.elim.:  43/43          
c   -- subsuming                       
c   -- var.elim.:  1000/3352          
c   -- var.elim.:  2000/3352          
c   -- var.elim.:  3000/3352          
c   -- var.elim.:  3352/3352          
c   -- var.elim.:  132/132          
c |        44 |   36533   127511 |      --      44       --      -- |     --   | -4846/-7336
c |        44 |   36533   127511 |   14613      41     1845    45.0 |  0.000 % |
c |       144 |   36533   127511 |   16074     141    24500   173.8 | 61.862 % |
c |       294 |   36533   127511 |   17681     291    33424   114.9 | 61.862 % |
c |       519 |   36533   127511 |   19450     516    68641   133.0 | 61.862 % |
c ==============================================================================
c (current CPU-time: 59.7039 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 |       776 |   39002   134238 |   11700     767   112754   147.0 | 61.862 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6105          
c   -- var.elim.:  2000/6105          
c   -- var.elim.:  3000/6105          
c   -- var.elim.:  4000/6105          
c   -- var.elim.:  5000/6105          
c   -- var.elim.:  6000/6105          
c   -- var.elim.:  6105/6105          
c   -- var.elim.:  1000/1956          
c   -- var.elim.:  1956/1956          
c |       776 |   36558   130127 |      --     767       --      -- |     --   | -2444/-4110
c |       776 |   36558   130127 |   14623     767   112754   147.0 | 61.862 % |
c |       876 |   36558   130127 |   16085     867   131898   152.1 | 61.927 % |
c |      1026 |   36558   130127 |   17694    1017   154895   152.3 | 61.927 % |
c |      1251 |   36558   130127 |   19463    1242   181189   145.9 | 61.927 % |
c |      1590 |   36558   130127 |   21409    1581   243644   154.1 | 61.927 % |
c |      2097 |   36532   129889 |   23534    2085   338138   162.2 | 62.034 % |
c ==============================================================================
c (current CPU-time: 68.8705 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 |      2588 |   37678   133143 |   11303    2576   434657   168.7 | 62.034 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5018          
c   -- var.elim.:  2000/5018          
c   -- var.elim.:  3000/5018          
c   -- var.elim.:  4000/5018          
c   -- var.elim.:  5000/5018          
c   -- var.elim.:  5018/5018          
c   -- var.elim.:  1000/1055          
c   -- var.elim.:  1055/1055          
c |      2588 |   36524   128872 |      --    2576       --      -- |     --   | -1137/-1762
c |      2588 |   36524   128872 |   14609    2341   278850   119.1 | 62.034 % |
c |      2688 |   36524   128872 |   16070    2441   296199   121.3 | 62.076 % |
c |      2839 |   36524   128872 |   17677    2592   331253   127.8 | 62.076 % |
c |      3064 |   36454   128083 |   19408    2813   362618   128.9 | 62.315 % |
c |      3401 |   36422   127796 |   21330    3144   403498   128.3 | 62.446 % |
c ==============================================================================
c (current CPU-time: 76.7533 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 |      3855 |   39129   134852 |   11738    3591   480031   133.7 | 62.446 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6841          
c   -- var.elim.:  2000/6841          
c   -- var.elim.:  3000/6841          
c   -- var.elim.:  4000/6841          
c   -- var.elim.:  5000/6841          
c   -- var.elim.:  6000/6841          
c   -- var.elim.:  6841/6841          
c   -- var.elim.:  1000/1945          
c   -- var.elim.:  1945/1945          
c   -- var.elim.:  168/168          
c |      3855 |   36482   131045 |      --    3591       --      -- |     --   | -2640/-3792
c |      3855 |   36482   131045 |   14592    3591   480031   133.7 | 62.446 % |
c |      3955 |   36482   131045 |   16052    3691   490564   132.9 | 62.684 % |
c |      4106 |   36441   130711 |   17637    3840   504822   131.5 | 62.830 % |
c |      4331 |   36409   130388 |   19384    4061   544271   134.0 | 62.960 % |
c |      4668 |   36337   129694 |   21280    4391   595494   135.6 | 63.213 % |
c |      5174 |   36291   129306 |   23378    4887   665778   136.2 | 63.359 % |
c |      5933 |   36143   128024 |   25611    5631   789055   140.1 | 63.919 % |
c |      7072 |   35897   125638 |   27981    6732   926234   137.6 | 64.887 % |
c |      8780 |   35845   125175 |   30734    8414  1221535   145.2 | 65.098 % |
c |     11342 |   35599   122829 |   33576   10932  1699087   155.4 | 66.098 % |
c |     15186 |   35128   118567 |   36445   14644  2455103   167.7 | 67.992 % |
c |     20953 |   34448   112138 |   39313   20166  3628725   179.9 | 70.658 % |
c |     29604 |   33801   106235 |   42432   28563  5782011   202.4 | 73.218 % |
c |     42578 |   33090    99636 |   45694   41072  9050077   220.3 | 76.047 % |
c ==============================================================================
c (current CPU-time: 233.827 s)
c ==============================================================================
c [1mFound solution: -30[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 |     52156 |   32697    95960 |    9809   50313 11331332   225.2 | 76.047 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2753          
c   -- var.elim.:  2000/2753          
c   -- var.elim.:  2753/2753          
c   -- var.elim.:  252/252          
c |     52156 |   32676    94024 |      --   50313       --      -- |     --   | -9/-1145
c |     52156 |   32676    94024 |   13070   36914  4504768   122.0 | 76.047 % |
c |     52256 |   32676    94024 |   14377   14331  1165939    81.4 | 77.797 % |
c |     52408 |   32676    94024 |   15815   14483  1207729    83.4 | 77.797 % |
c |     52633 |   32676    94024 |   17396   14708  1252250    85.1 | 77.797 % |
c |     52970 |   32676    94024 |   19136   15045  1326140    88.1 | 77.797 % |
c |     53476 |   32674    94004 |   21048   15547  1418237    91.2 | 77.805 % |
c |     54237 |   32648    93750 |   23135   16290  1600367    98.2 | 77.911 % |
c |     55376 |   32618    93485 |   25425   17428  1897672   108.9 | 78.033 % |
c |     57084 |   32317    90850 |   27709   19116  2218460   116.1 | 79.165 % |
c |     59648 |   32315    90827 |   30478   21653  2687705   124.1 | 79.173 % |
c ==============================================================================
c (current CPU-time: 256.181 s)
c ==============================================================================
c [1mFound solution: -31[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 |     61601 |   34382    96141 |   10314   23602  3029590   128.4 | 79.173 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3939          
c   -- var.elim.:  2000/3939          
c   -- var.elim.:  3000/3939          
c   -- var.elim.:  3939/3939          
c   -- var.elim.:  1000/1267          
c   -- var.elim.:  1267/1267          
c   -- var.elim.:  9/9          
c |     61601 |   32363    92933 |      --   23602       --      -- |     --   | -2010/-3189
c |     61601 |   32363    92933 |   12945   23580  3028784   128.4 | 79.173 % |
c |     61701 |   32363    92933 |   14239   23680  3050247   128.8 | 82.153 % |
c |     61851 |   32363    92933 |   15663   23830  3068612   128.8 | 82.153 % |
c |     62076 |   32271    92144 |   17181   24027  3080199   128.2 | 82.458 % |
c |     62413 |   32271    92144 |   18899   24364  3140041   128.9 | 82.459 % |
c |     62919 |   32245    91934 |   20772   24830  3223405   129.8 | 82.549 % |
c |     63678 |   32199    91628 |   22816   25588  3391365   132.5 | 82.695 % |
c |     64817 |   32081    90586 |   25006   26719  3602519   134.8 | 83.063 % |
c |     66525 |   31998    89904 |   27436   28385  4108398   144.7 | 83.326 % |
c |     69087 |   31923    89303 |   30109   30920  4544951   147.0 | 83.542 % |
c |     72931 |   31862    88826 |   33056   34731  5269199   151.7 | 83.722 % |
c |     78699 |   31810    88457 |   36303   40454  6485793   160.3 | 83.854 % |
c |     87349 |   31770    88123 |   39883   48970  8778114   179.3 | 83.993 % |
c |    100323 |   31525    85804 |   43533   26816  5147662   192.0 | 84.806 % |
c |    119785 |   31304    83838 |   47550   46203  9472691   205.0 | 85.556 % |
c |    148977 |   31037    81376 |   51859   31877  6032489   189.2 | 86.465 % |
c ==============================================================================
c (current CPU-time: 671.927 s)
c ==============================================================================
c [1mFound solution: -32[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 |    184777 |   30878    79739 |    9263   20520  3207283   156.3 | 86.465 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1882          
c   -- var.elim.:  1882/1882          
c   -- var.elim.:  284/284          
c |    184777 |   30805    77917 |      --   20520       --      -- |     --   | -48/-283
c |    184777 |   30805    77917 |   12322   12251   660534    53.9 | 86.465 % |
c |    184878 |   30805    77917 |   13554   12352   676610    54.8 | 87.329 % |
c |    185028 |   30805    77917 |   14909   12502   697124    55.8 | 87.329 % |
c |    185253 |   30805    77917 |   16400   12727   709566    55.8 | 87.329 % |
c |    185591 |   30805    77917 |   18040   13065   759392    58.1 | 87.329 % |
c |    186097 |   30805    77917 |   19844   13571   856965    63.1 | 87.329 % |
c |    186856 |   30805    77917 |   21829   14330   991052    69.2 | 87.329 % |
c |    187995 |   30805    77917 |   24012   15469  1130545    73.1 | 87.329 % |
c |    189703 |   30805    77917 |   26413   17177  1472180    85.7 | 87.329 % |
c |    192265 |   30801    77886 |   29050   19727  1987851   100.8 | 87.336 % |
c |    196111 |   30801    77886 |   31955   23573  2735627   116.0 | 87.335 % |
c |    201877 |   30775    77695 |   35121   29318  3809157   129.9 | 87.426 % |
c |    210528 |   30720    77258 |   38565   37959  5411712   142.6 | 87.592 % |
c |    223502 |   30658    76791 |   42335   50814  7848034   154.4 | 87.807 % |
c |    242964 |   30634    76599 |   46533   32686  4669229   142.9 | 87.876 % |
c |    272156 |   30460    75200 |   50895   19431  2715051   139.7 | 88.451 % |
c |    315945 |   30458    75180 |   55981   63218 11233981   177.7 | 88.458 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 C462 -C461 -C460 -C459 C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -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 -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 1/56 18894
Raw data (stat): 18894 (runsolver) R 18893 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 365371979 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.0002 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 3710 0 0 0 985 14 0 0 25 0 1 0 365371979 17604608 3650 4294967295 134512640 134672761 3221224560 3221222992 134604046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4298 3650 603 41 0 4257 0
vsize: 17192
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 3720 0 0 0 1985 14 0 0 25 0 1 0 365371979 17604608 3660 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4298 3660 603 41 0 4257 0
vsize: 17192
[startup+30.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 3748 0 0 0 2985 14 0 0 25 0 1 0 365371979 17850368 3688 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4358 3688 603 41 0 4317 0
vsize: 17432
[startup+40.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 3858 0 0 0 3984 15 0 0 25 0 1 0 365371979 18538496 3798 4294967295 134512640 134672761 3221224560 3221223104 134621049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4526 3798 603 41 0 4485 0
vsize: 18104
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 4737 0 0 0 4966 33 0 0 25 0 1 0 365371979 18239488 3906 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4453 3906 603 41 0 4412 0
vsize: 17812
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 4854 0 0 0 5966 33 0 0 25 0 1 0 365371979 18239488 3913 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4453 3913 603 41 0 4412 0
vsize: 17812
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 6563 0 0 0 6948 50 0 0 25 0 1 0 365371979 21213184 4689 4294967295 134512640 134672761 3221224560 3221223104 134621110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5179 4689 603 41 0 5138 0
vsize: 20716
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 7586 0 0 0 7937 61 0 0 25 0 1 0 365371979 23867392 4846 4294967295 134512640 134672761 3221224560 3221222848 134565586 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5827 4846 603 41 0 5786 0
vsize: 23308
[startup+90.0043 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 7594 0 0 0 8931 67 0 0 25 0 1 0 365371979 23867392 4854 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5827 4854 603 41 0 5786 0
vsize: 23308
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 8517 0 0 0 9929 69 0 0 25 0 1 0 365371979 27549696 5777 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6726 5777 603 41 0 6685 0
vsize: 26904
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 9423 0 0 0 10928 71 0 0 25 0 1 0 365371979 31330304 6683 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7649 6683 603 41 0 7608 0
vsize: 30596
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 10255 0 0 0 11926 73 0 0 25 0 1 0 365371979 34693120 7515 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8470 7515 603 41 0 8429 0
vsize: 33880
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18894
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 11069 0 0 0 12924 75 0 0 25 0 1 0 365371979 38092800 8329 4294967295 134512640 134672761 3221224560 3221223600 134612504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9300 8329 603 41 0 9259 0
vsize: 37200
[startup+140.006 s]
Raw data (loadavg): 1.07 0.98 0.91 2/59 18903
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 11819 0 0 0 13921 77 0 0 25 0 1 0 365371979 41099264 9079 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10034 9079 603 41 0 9993 0
vsize: 40136
[startup+150.007 s]
Raw data (loadavg): 1.06 0.98 0.91 2/56 18947
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 12679 0 0 0 14919 80 0 0 25 0 1 0 365371979 44605440 9939 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 9939 603 41 0 10849 0
vsize: 43560
[startup+160.006 s]
Raw data (loadavg): 1.05 0.98 0.91 2/56 18947
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 13406 0 0 0 15917 81 0 0 25 0 1 0 365371979 47603712 10666 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10666 603 41 0 11581 0
vsize: 46488
[startup+170.007 s]
Raw data (loadavg): 1.04 0.98 0.91 2/56 18947
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 14138 0 0 0 16916 83 0 0 25 0 1 0 365371979 50728960 11398 4294967295 134512640 134672761 3221224560 3221223704 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12385 11398 603 41 0 12344 0
vsize: 49540
[startup+180.008 s]
Raw data (loadavg): 1.03 0.98 0.91 2/56 18947
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 15004 0 0 0 17914 85 0 0 25 0 1 0 365371979 54206464 12264 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13234 12264 603 41 0 13193 0
vsize: 52936
[startup+190.008 s]
Raw data (loadavg): 1.03 0.98 0.91 2/56 18947
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 15729 0 0 0 18911 88 0 0 25 0 1 0 365371979 57225216 12989 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13971 12989 603 41 0 13930 0
vsize: 55884
[startup+200.009 s]
Raw data (loadavg): 1.02 0.98 0.91 2/56 18949
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 16510 0 0 0 19910 90 0 0 25 0 1 0 365371979 60334080 13770 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14730 13770 603 41 0 14689 0
vsize: 58920
[startup+210.008 s]
Raw data (loadavg): 1.02 0.98 0.91 2/56 18951
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 16990 0 0 0 20909 91 0 0 25 0 1 0 365371979 62291968 14250 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15208 14250 603 41 0 15167 0
vsize: 60832
[startup+220.009 s]
Raw data (loadavg): 1.02 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 17537 0 0 0 21908 92 0 0 25 0 1 0 365371979 64638976 14797 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15781 14797 603 41 0 15740 0
vsize: 63124
[startup+230.009 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 18146 0 0 0 22907 94 0 0 25 0 1 0 365371979 67125248 15406 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16388 15406 603 41 0 16347 0
vsize: 65552
[startup+240.009 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 19964 0 0 0 23896 104 0 0 25 0 1 0 365371979 70488064 16226 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17209 16226 603 41 0 17168 0
vsize: 68836
[startup+250.01 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 19964 0 0 0 24897 104 0 0 25 0 1 0 365371979 70488064 16226 4294967295 134512640 134672761 3221224560 3221223684 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17209 16226 603 41 0 17168 0
vsize: 68836
[startup+260.01 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20876 0 0 0 25885 115 0 0 25 0 1 0 365371979 69283840 16027 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16027 603 41 0 16874 0
vsize: 67660
[startup+270.01 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 26885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223472 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+280.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 27885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+290.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 28885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+300.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 29885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+310.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 30885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+320.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 31885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+330.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 32885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+340.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20877 0 0 0 33885 116 0 0 25 0 1 0 365371979 69283840 16028 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16028 603 41 0 16874 0
vsize: 67660
[startup+350.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20878 0 0 0 34885 117 0 0 25 0 1 0 365371979 69283840 16029 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16029 603 41 0 16874 0
vsize: 67660
[startup+360.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 35885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+370.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 36885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+380.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 37885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+390.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 38885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+400.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 39885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+410.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 40885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+420.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 41885 117 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+430.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 42885 118 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+440.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 43885 118 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+450.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 44885 118 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+460.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20879 0 0 0 45885 118 0 0 25 0 1 0 365371979 69283840 16030 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16915 16030 603 41 0 16874 0
vsize: 67660
[startup+470.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 20985 0 0 0 46884 119 0 0 25 0 1 0 365371979 69804032 16136 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17042 16136 603 41 0 17001 0
vsize: 68168
[startup+480.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 21344 0 0 0 47884 120 0 0 25 0 1 0 365371979 71262208 16495 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17398 16495 603 41 0 17357 0
vsize: 69592
[startup+490.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 21879 0 0 0 48883 121 0 0 25 0 1 0 365371979 73379840 17030 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17915 17030 603 41 0 17874 0
vsize: 71660
[startup+500.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22485 0 0 0 49881 122 0 0 25 0 1 0 365371979 75870208 17636 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18523 17636 603 41 0 18482 0
vsize: 74092
[startup+510.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18953
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 50881 123 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+520.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 51880 123 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+530.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 52880 123 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+540.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 53880 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+550.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 54881 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+560.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 55881 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+570.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 56881 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+580.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 57881 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223568 134522547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+590.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 58881 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+600.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 59881 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+610.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 60882 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+620.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 61882 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+630.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 62882 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+640.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22811 0 0 0 63882 124 0 0 25 0 1 0 365371979 77045760 17933 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 17933 603 41 0 18769 0
vsize: 75240
[startup+650.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 22852 0 0 0 64882 124 0 0 25 0 1 0 365371979 77307904 17974 4294967295 134512640 134672761 3221224560 3221223704 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18874 17974 603 41 0 18833 0
vsize: 75496
[startup+660.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 23221 0 0 0 65881 125 0 0 25 0 1 0 365371979 78757888 18343 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19228 18344 603 41 0 19187 0
vsize: 76912
[startup+670.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 23832 0 0 0 66880 126 0 0 25 0 1 0 365371979 81215488 18889 4294967295 134512640 134672761 3221224560 3221223372 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19828 18889 603 41 0 19787 0
vsize: 79312
[startup+680.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 67871 135 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+690.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 68871 135 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+700.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 69871 135 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+710.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 70871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+720.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 71871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+730.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 72871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+740.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 73871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+750.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 74871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+760.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 75871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+770.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 76871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+780.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 77872 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+790.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25058 0 0 0 78871 136 0 0 25 0 1 0 365371979 81350656 18923 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 18923 603 41 0 19820 0
vsize: 79444
[startup+800.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 79871 137 0 0 25 0 1 0 365371979 81612800 18979 4294967295 134512640 134672761 3221224560 3221223540 1075351154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19925 18979 603 41 0 19884 0
vsize: 79700
[startup+810.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18955
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 80871 137 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+820.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 81871 137 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+830.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 82871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+840.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 83871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+850.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 84871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+860.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 85871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+870.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 86871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223704 134616339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+880.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 87871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+890.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 88871 138 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+900.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 89871 139 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+910.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 90871 139 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+920.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25114 0 0 0 91871 139 0 0 25 0 1 0 365371979 81338368 18920 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19858 18920 603 41 0 19817 0
vsize: 79432
[startup+930.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 92871 139 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+940.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 93871 139 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+950.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 94871 139 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+960.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 95871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+970.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 96871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223600 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+980.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 97871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+990.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 98871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223600 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 99871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223724 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 100871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 101871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 102871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 103871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 104871 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 105872 140 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.98 0.91 3/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25173 0 0 0 106871 141 0 0 25 0 1 0 365371979 81293312 18909 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18909 603 41 0 19806 0
vsize: 79388
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25174 0 0 0 107871 141 0 0 25 0 1 0 365371979 81293312 18910 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18910 603 41 0 19806 0
vsize: 79388
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25176 0 0 0 108871 141 0 0 25 0 1 0 365371979 81293312 18912 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19847 18912 603 41 0 19806 0
vsize: 79388
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 109871 142 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18957
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 110871 142 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 111871 142 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 112871 142 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 113871 142 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 114871 142 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 115871 143 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 116871 143 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 117871 143 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 118871 143 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 18959
Raw data (stat): 18894 (minisat+) R 18893 12452 12451 0 -1 0 25246 0 0 0 119871 143 0 0 25 0 1 0 365371979 81285120 18911 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.98 0.91 1/56 18959
Raw data (stat): 18894 (minisat+) Z 18893 12452 12451 0 -1 12 25247 0 0 0 119871 149 0 0 25 0 1 0 365371979 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.21
CPU user time (s): 1198.72
CPU system time (s): 1.49077
CPU usage (%): 100.01
Max. virtual memory (Kb): 79700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####