PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-1.opb
MD5SUM	84d0b0ba659c599a6c66454cd956a06b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04684
Number of variables	450
Total number of constraints	17827
Number of constraints which are clauses	17827
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 5596

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890520 kB
Buffers:         35172 kB
Cached:          72332 kB
SwapCached:          4 kB
Active:          52728 kB
Inactive:        58548 kB
HighTotal:      131008 kB
HighFree:        54152 kB
LowTotal:       903652 kB
LowFree:        836368 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27460 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:02:08 (client local time) WITH STATUS 30 IN 756.525 SECONDS
stats: 4074 0 756.525 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17827 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 |   17827    35654 |    5348       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   17827    35654 |    7130       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.645901 s)
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   34840    75669 |   10451       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11709          
c   -- var.elim.:  2000/11709          
c   -- var.elim.:  3000/11709          
c   -- var.elim.:  4000/11709          
c   -- var.elim.:  5000/11709          
c   -- var.elim.:  6000/11709          
c   -- var.elim.:  7000/11709          
c   -- var.elim.:  8000/11709          
c   -- var.elim.:  9000/11709          
c   -- var.elim.:  10000/11709          
c   -- var.elim.:  11000/11709          
c   -- var.elim.:  11709/11709          
c   -- var.elim.:  1000/5970          
c   -- var.elim.:  2000/5970          
c   -- var.elim.:  3000/5970          
c   -- var.elim.:  4000/5970          
c   -- var.elim.:  5000/5970          
c   -- var.elim.:  5970/5970          
c   -- var.elim.:  113/113          
c   -- subsuming                       
c   -- var.elim.:  1000/2274          
c   -- var.elim.:  2000/2274          
c   -- var.elim.:  2274/2274          
c   -- var.elim.:  206/206          
c |         0 |   22802    70407 |      --       0       --      -- |     --   | -12033/-5247
c |         0 |   22802    70407 |    9120       0        0     nan |  0.000 % |
c |       100 |   22802    70407 |   10032     100     6048    60.5 | 52.331 % |
c |       250 |   22802    70407 |   11036     250    25728   102.9 | 52.332 % |
c |       475 |   22768    70142 |   12121     472    49085   104.0 | 52.566 % |
c |       812 |   22712    69688 |   13301     802    83289   103.9 | 53.038 % |
c |      1318 |   22667    69375 |   14602    1306   130201    99.7 | 53.357 % |
c ==============================================================================
c (current CPU-time: 12.5471 s)
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1556 |   25815    77771 |    7744    1544   171919   111.3 | 53.357 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5271          
c   -- var.elim.:  2000/5271          
c   -- var.elim.:  3000/5271          
c   -- var.elim.:  4000/5271          
c   -- var.elim.:  5000/5271          
c   -- var.elim.:  5271/5271          
c   -- var.elim.:  1000/2130          
c   -- var.elim.:  2000/2130          
c   -- var.elim.:  2130/2130          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  1000/2016          
c   -- var.elim.:  2000/2016          
c   -- var.elim.:  2016/2016          
c   -- var.elim.:  33/33          
c |      1556 |   22769    73434 |      --    1544       --      -- |     --   | -3037/-4318
c |      1556 |   22769    73434 |    9107    1521   159846   105.1 | 53.357 % |
c |      1656 |   22769    73434 |   10018    1621   171277   105.7 | 62.843 % |
c |      1806 |   22769    73434 |   11020    1771   202897   114.6 | 62.843 % |
c |      2031 |   22769    73434 |   12122    1996   231087   115.8 | 62.844 % |
c |      2368 |   22596    71926 |   13233    2324   265604   114.3 | 63.850 % |
c |      2874 |   22310    69546 |   14372    2762   311230   112.7 | 65.718 % |
c |      3633 |   22310    69546 |   15809    3521   450025   127.8 | 65.718 % |
c |      4772 |   22072    67601 |   17204    4607   665157   144.4 | 67.294 % |
c ==============================================================================
c (current CPU-time: 21.6097 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 |      5741 |   22064    67090 |    6619    5558   802368   144.4 | 67.294 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2361          
c   -- var.elim.:  2000/2361          
c   -- var.elim.:  2361/2361          
c   -- var.elim.:  192/192          
c |      5741 |   21949    66286 |      --    5558       --      -- |     --   | -103/-554
c |      5741 |   21949    66286 |    8779    4574   387102    84.6 | 67.294 % |
c |      5841 |   21949    66286 |    9657    4674   396356    84.8 | 68.149 % |
c |      5991 |   21923    66059 |   10610    4823   419765    87.0 | 68.321 % |
c |      6216 |   21907    65922 |   11663    5030   449599    89.4 | 68.428 % |
c |      6553 |   21907    65922 |   12829    5367   500221    93.2 | 68.427 % |
c |      7059 |   21907    65922 |   14112    5873   616644   105.0 | 68.428 % |
c |      7818 |   21907    65922 |   15523    6632   801118   120.8 | 68.428 % |
c |      8957 |   21817    65168 |   17006    7739   998543   129.0 | 69.010 % |
c |     10665 |   21720    64387 |   18623    9379  1309563   139.6 | 69.633 % |
c |     13227 |   21676    64055 |   20444   11920  1854179   155.6 | 69.910 % |
c ==============================================================================
c (current CPU-time: 33.9778 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 |     14335 |   22526    66363 |    6757   13025  2037607   156.4 | 69.910 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2972          
c   -- var.elim.:  2000/2972          
c   -- var.elim.:  2972/2972          
c   -- var.elim.:  806/806          
c |     14335 |   21705    64626 |      --   13025       --      -- |     --   | -811/-982
c |     14335 |   21705    64626 |    8682   13025  2037607   156.4 | 69.910 % |
c |     14435 |   21705    64626 |    9550   13125  2050185   156.2 | 70.478 % |
c |     14585 |   21705    64626 |   10505   13275  2075574   156.4 | 70.477 % |
c |     14810 |   21705    64626 |   11555   13500  2116988   156.8 | 70.477 % |
c |     15147 |   21705    64626 |   12711   13837  2171598   156.9 | 70.478 % |
c |     15653 |   21705    64626 |   13982   14343  2262744   157.8 | 70.478 % |
c |     16415 |   21705    64626 |   15380   15105  2388632   158.1 | 70.478 % |
c |     17554 |   21672    64348 |   16893   14290  1643535   115.0 | 70.686 % |
c |     19262 |   21642    64133 |   18556   15996  1910783   119.5 | 70.868 % |
c |     21825 |   21553    63361 |   20328   18504  2334081   126.1 | 71.427 % |
c |     25669 |   21411    62211 |   22213   22245  3010817   135.3 | 72.324 % |
c |     31435 |   21311    61382 |   24321   27972  4195136   150.0 | 72.936 % |
c |     40085 |   20959    58736 |   26311   21247  3512986   165.3 | 75.069 % |
c |     53059 |   20632    56432 |   28490   18228  2703874   148.3 | 77.072 % |
c ==============================================================================
c (current CPU-time: 131.192 s)
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     56909 |   22761    62142 |    6828   22078  3501383   158.6 | 77.072 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3816          
c   -- var.elim.:  2000/3816          
c   -- var.elim.:  3000/3816          
c   -- var.elim.:  3816/3816          
c   -- var.elim.:  1000/1475          
c   -- var.elim.:  1475/1475          
c   -- var.elim.:  29/29          
c |     56909 |   20695    58456 |      --   22078       --      -- |     --   | -2052/-3657
c |     56909 |   20695    58456 |    8278   22074  3500167   158.6 | 77.072 % |
c |     57009 |   20602    57722 |    9064   14813  2118570   143.0 | 79.256 % |
c |     57159 |   20576    57526 |    9958   14962  2127409   142.2 | 79.364 % |
c |     57384 |   20485    56863 |   10906   15170  2155234   142.1 | 79.855 % |
c |     57721 |   20485    56863 |   11996   15507  2211008   142.6 | 79.854 % |
c |     58228 |   20485    56863 |   13196   16014  2302666   143.8 | 79.855 % |
c |     58988 |   20485    56863 |   14516   16774  2436341   145.2 | 79.854 % |
c |     60127 |   20392    56195 |   15895   17864  2589822   145.0 | 80.344 % |
c |     61835 |   20307    55541 |   17411   19555  2885655   147.6 | 80.823 % |
c |     64397 |   20307    55541 |   19153   22117  3329651   150.5 | 80.823 % |
c |     68241 |   20261    55179 |   21020   25943  4050735   156.1 | 81.074 % |
c |     74007 |   20247    55065 |   23106   18576  2688945   144.8 | 81.158 % |
c |     82657 |   20116    54039 |   25253   27191  4202362   154.5 | 81.875 % |
c |     95632 |   19989    53023 |   27602   23469  3367510   143.5 | 82.604 % |
c |    115094 |   19837    51774 |   30132   24804  3569328   143.9 | 83.501 % |
c |    144286 |   19673    50525 |   32871   32713  4881383   149.2 | 84.422 % |
c ==============================================================================
c (current CPU-time: 367.382 s)
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    159177 |   20166    51794 |    6049   23133  3268808   141.3 | 84.422 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1803          
c   -- var.elim.:  1803/1803          
c   -- var.elim.:  688/688          
c |    159177 |   19611    49375 |      --   23133       --      -- |     --   | -536/-1736
c |    159177 |   19611    49375 |    7844   13913   959358    69.0 | 84.422 % |
c |    159278 |   19611    49375 |    8628   14014   970231    69.2 | 84.910 % |
c |    159429 |   19611    49375 |    9491   14165   984159    69.5 | 84.910 % |
c |    159655 |   19593    49243 |   10431   14388  1017720    70.7 | 85.018 % |
c |    159994 |   19593    49243 |   11474   14727  1067399    72.5 | 85.018 % |
c |    160500 |   19593    49243 |   12621   15233  1144427    75.1 | 85.017 % |
c |    161260 |   19593    49243 |   13884   15993  1254625    78.4 | 85.018 % |
c |    162399 |   19578    49155 |   15260   17129  1422411    83.0 | 85.101 % |
c |    164107 |   19578    49155 |   16786   18837  1701330    90.3 | 85.101 % |
c |    166669 |   19578    49155 |   18465   21399  2079018    97.2 | 85.101 % |
c |    170513 |   19548    48899 |   20280   25239  2661762   105.5 | 85.268 % |
c |    176279 |   19515    48661 |   22271   19184  2190997   114.2 | 85.458 % |
c |    184932 |   19491    48519 |   24468   27832  3590286   129.0 | 85.565 % |
c |    197906 |   19470    48369 |   26886   24535  3105502   126.6 | 85.684 % |
c |    217368 |   19316    47298 |   29340   25158  2890915   114.9 | 86.565 % |
c |    246560 |   19269    46994 |   32196   33252  4096151   123.2 | 86.827 % |
c ==============================================================================
c (current CPU-time: 577.561 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 |    256442 |   19837    48523 |    5951   19408  1959485   101.0 | 86.827 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1647          
c   -- var.elim.:  1647/1647          
c   -- var.elim.:  725/725          
c |    256442 |   19272    47474 |      --   19408       --      -- |     --   | -565/-1048
c |    256442 |   19272    47474 |    7708   15028  1202386    80.0 | 86.827 % |
c |    256542 |   19272    47474 |    8479   15128  1214185    80.3 | 87.062 % |
c |    256692 |   19272    47474 |    9327   15278  1228580    80.4 | 87.062 % |
c |    256917 |   19272    47474 |   10260   15503  1252016    80.8 | 87.062 % |
c |    257255 |   19272    47474 |   11286   15841  1296798    81.9 | 87.062 % |
c |    257762 |   19272    47474 |   12415   16348  1349645    82.6 | 87.062 % |
c |    258521 |   19272    47474 |   13656   17107  1433762    83.8 | 87.062 % |
c |    259660 |   19272    47474 |   15022   18246  1574619    86.3 | 87.062 % |
c |    261370 |   19245    47306 |   16501   19953  1766450    88.5 | 87.180 % |
c |    263932 |   19245    47306 |   18151   22515  2079207    92.3 | 87.180 % |
c |    267776 |   19245    47306 |   19966   15875  1420910    89.5 | 87.180 % |
c |    273542 |   19192    46951 |   21902   21616  1999484    92.5 | 87.451 % |
c |    282192 |   19155    46705 |   24046   16751  1402205    83.7 | 87.652 % |
c |    295166 |   19131    46560 |   26418   29707  2663557    89.7 | 87.758 % |
c |    314627 |   19131    46560 |   29059   31898  2752195    86.3 | 87.758 % |
c ==============================================================================
c (current CPU-time: 709.231 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 |    328961 |   19590    47733 |    5876   26649  2250114    84.4 | 87.758 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1486          
c   -- var.elim.:  1486/1486          
c   -- var.elim.:  521/521          
c |    328961 |   19083    46167 |      --   26649       --      -- |     --   | -491/-937
c |    328961 |   19083    46167 |    7633   12444   473712    38.1 | 87.758 % |
c |    329061 |   19083    46167 |    8396   12544   481069    38.4 | 88.104 % |
c |    329212 |   19083    46167 |    9236   12695   494198    38.9 | 88.104 % |
c |    329437 |   19083    46167 |   10159   12920   515057    39.9 | 88.104 % |
c |    329774 |   19083    46167 |   11175   13257   548611    41.4 | 88.103 % |
c |    330280 |   19083    46167 |   12293   13763   587410    42.7 | 88.103 % |
c |    331039 |   19083    46167 |   13522   14522   644397    44.4 | 88.103 % |
c |    332181 |   19063    46060 |   14859   15642   744694    47.6 | 88.210 % |
c |    333889 |   19036    45864 |   16322   17349   886302    51.1 | 88.363 % |
c |    336452 |   18938    45240 |   17861   19769  1070819    54.2 | 88.859 % |
c |    340297 |   18938    45240 |   19648   23614  1363396    57.7 | 88.859 % |
c |    346064 |   18878    44877 |   21544   17733  1036861    58.5 | 89.166 % |
c |    354713 |   18244    42843 |   22902   22094  1185192    53.6 | 90.169 % |
c ==============================================================================
c [1mOptimal solution: -30[0m
s OPTIMUM FOUND
v -C450 -C449 -C448 -C447 -C446 C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 C336 -C335 -C334 -C333 -C332 -C331 -C330 C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 C211 -C210 -C209 -C208 -C207 C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 C122 -C121 C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 C78 -C77 -C76 -C75 C74 -C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 -C62 -C61 -C60 -C59 -C58 -C57 -C56 C55 -C54 -C53 -C52 -C51 -C50 -C49 -C48 -C47 -C46 -C45 -C44 -C43 -C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 C34 -C33 -C32 -C31 -C30 -C29 -C28 -C27 -C26 -C25 -C24 -C23 -C22 -C21 -C20 C19 -C18 -C17 -C16 -C15 -C14 -C13 -C12 -C11 -C10 -C9 -C8 -C7 -C6 C5 -C4 -C3 -C2 -C1
c _______________________________________________________________________________
c 
c restarts              : 99
c conflicts             : 359580         (476 /sec)
c decisions             : 569975         (754 /sec)
c propagations          : 28824336       (38132 /sec)
c inspects              : 1136796088     (1503897 /sec)
c CPU time              : 755.9 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 18273
Raw data (stat): 18273 (runsolver) R 18272 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480403213 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 2487 0 0 0 989 9 0 0 25 0 1 0 480403213 12279808 2378 4294967295 134512640 134672761 3221224560 3221222960 134605453 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2998 2378 603 41 0 2957 0
vsize: 11992
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 3473 0 0 0 1981 17 0 0 25 0 1 0 480403213 14028800 2872 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3425 2872 603 41 0 3384 0
vsize: 13700
[startup+30.0003 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 4756 0 0 0 2976 22 0 0 25 0 1 0 480403213 19103744 3928 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4664 3928 603 41 0 4623 0
vsize: 18656
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 6149 0 0 0 3972 25 0 0 25 0 1 0 480403213 23814144 5061 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5814 5061 603 41 0 5773 0
vsize: 23256
[startup+50.0004 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 6208 0 0 0 4972 26 0 0 25 0 1 0 480403213 24076288 5120 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5878 5120 603 41 0 5837 0
vsize: 23512
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 7185 0 0 0 5969 28 0 0 25 0 1 0 480403213 28020736 6097 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6841 6097 603 41 0 6800 0
vsize: 27364
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 7938 0 0 0 6967 31 0 0 25 0 1 0 480403213 31039488 6850 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7578 6850 603 41 0 7537 0
vsize: 30312
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 8820 0 0 0 7965 33 0 0 25 0 1 0 480403213 34619392 7732 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8452 7732 603 41 0 8411 0
vsize: 33808
[startup+90.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 8820 0 0 0 8965 33 0 0 25 0 1 0 480403213 34619392 7732 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8452 7732 603 41 0 8411 0
vsize: 33808
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 8821 0 0 0 9965 33 0 0 25 0 1 0 480403213 34619392 7733 4294967295 134512640 134672761 3221224560 3221223704 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8452 7733 603 41 0 8411 0
vsize: 33808
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 8959 0 0 0 10965 33 0 0 25 0 1 0 480403213 35274752 7871 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8612 7871 603 41 0 8571 0
vsize: 34448
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 9738 0 0 0 11963 36 0 0 25 0 1 0 480403213 38416384 8650 4294967295 134512640 134672761 3221224560 3221223704 134616254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9379 8650 603 41 0 9338 0
vsize: 37516
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 9769 0 0 0 12963 36 0 0 25 0 1 0 480403213 38494208 8681 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9398 8681 603 41 0 9357 0
vsize: 37592
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 13958 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 14957 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 15957 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 16958 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 17958 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 18958 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 19958 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 20958 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 21959 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223600 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10341 0 0 0 22959 41 0 0 25 0 1 0 480403213 39804928 8965 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8965 603 41 0 9677 0
vsize: 38872
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10342 0 0 0 23959 41 0 0 25 0 1 0 480403213 39804928 8966 4294967295 134512640 134672761 3221224560 3221223600 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8966 603 41 0 9677 0
vsize: 38872
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10342 0 0 0 24959 41 0 0 25 0 1 0 480403213 39804928 8966 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8966 603 41 0 9677 0
vsize: 38872
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10342 0 0 0 25959 41 0 0 25 0 1 0 480403213 39804928 8966 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8966 603 41 0 9677 0
vsize: 38872
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10342 0 0 0 26960 41 0 0 25 0 1 0 480403213 39804928 8966 4294967295 134512640 134672761 3221224560 3221223704 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8966 603 41 0 9677 0
vsize: 38872
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10342 0 0 0 27960 41 0 0 25 0 1 0 480403213 39804928 8966 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8966 603 41 0 9677 0
vsize: 38872
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10342 0 0 0 28960 41 0 0 25 0 1 0 480403213 39804928 8966 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9718 8966 603 41 0 9677 0
vsize: 38872
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10542 0 0 0 29959 42 0 0 25 0 1 0 480403213 40177664 9128 4294967295 134512640 134672761 3221224560 3221223600 134612865 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9809 9128 603 41 0 9768 0
vsize: 39236
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10542 0 0 0 30960 42 0 0 25 0 1 0 480403213 40177664 9128 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9809 9128 603 41 0 9768 0
vsize: 39236
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10542 0 0 0 31960 42 0 0 25 0 1 0 480403213 40177664 9128 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9809 9128 603 41 0 9768 0
vsize: 39236
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10542 0 0 0 32960 42 0 0 25 0 1 0 480403213 40177664 9128 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9809 9128 603 41 0 9768 0
vsize: 39236
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10542 0 0 0 33960 42 0 0 25 0 1 0 480403213 40177664 9128 4294967295 134512640 134672761 3221224560 3221223600 134612867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9809 9128 603 41 0 9768 0
vsize: 39236
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 10723 0 0 0 34960 42 0 0 25 0 1 0 480403213 40968192 9309 4294967295 134512640 134672761 3221224560 3221223600 134614191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10002 9309 603 41 0 9961 0
vsize: 40008
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11007 0 0 0 35959 43 0 0 25 0 1 0 480403213 42049536 9583 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10266 9583 603 41 0 10225 0
vsize: 41064
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 36953 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 37953 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 38954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 39954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223696 134614583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 40954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 41953 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 42954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221221876 134646181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 43954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 44954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223600 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 45954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 46954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 47954 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 48955 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 49955 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 50955 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 51955 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 52955 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 53956 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 54956 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 55956 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 11606 0 0 0 56956 49 0 0 25 0 1 0 480403213 42721280 9747 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9747 603 41 0 10389 0
vsize: 41720
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 57952 53 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 58952 53 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 59952 53 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 60952 53 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 61951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18273
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 62951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+640.008 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 63950 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+650.008 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12121 0 0 0 64950 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+660.008 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12155 0 0 0 65951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+670.008 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12155 0 0 0 66951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+680.007 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12155 0 0 0 67951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+690.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12155 0 0 0 68951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+700.008 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12192 0 0 0 69951 54 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223600 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+710.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 18326
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12733 0 0 0 70948 58 0 0 25 0 1 0 480403213 42033152 9594 4294967295 134512640 134672761 3221224560 3221223792 134593638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9594 603 41 0 10221 0
vsize: 41048
[startup+720.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 18328
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12810 0 0 0 71946 59 0 0 25 0 1 0 480403213 42033152 9601 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9601 603 41 0 10221 0
vsize: 41048
[startup+730.009 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 18328
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12810 0 0 0 72947 59 0 0 25 0 1 0 480403213 42033152 9601 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9601 603 41 0 10221 0
vsize: 41048
[startup+740.009 s]
Raw data (loadavg): 1.17 1.03 0.93 2/54 18328
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12810 0 0 0 73947 59 0 0 25 0 1 0 480403213 42033152 9601 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10262 9601 603 41 0 10221 0
vsize: 41048
[startup+750.009 s]
Raw data (loadavg): 1.14 1.03 0.93 2/54 18328
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12810 0 0 0 74947 59 0 0 25 0 1 0 480403213 42033152 9601 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9601 603 41 0 10221 0
vsize: 41048
[startup+756.473 s]
Raw data (loadavg): 1.13 1.03 0.93 1/53 18328
Raw data (stat): 18273 (minisat+) R 18272 10614 10613 0 -1 0 12810 0 0 0 74947 59 0 0 25 0 1 0 480403213 42033152 9601 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10262 9601 603 41 0 10221 0
vsize: 0

Child status: 30
Real time (s): 756.473
CPU time (s): 756.525
CPU user time (s): 755.906
CPU system time (s): 0.618905
CPU usage (%): 100.007
Max. virtual memory (Kb): 41720
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-30
#### END VERIFIER DATA ####